ByInduction​(AngouriMath.​Entity.​Variable,​AngouriMath.​Entity.​Set,​AngouriMath.​Entity.​Number.​Integer,​AngouriMath.​Entity,​System.​Boolean)

forall x in S : sum(f, k, a, x) = g by induction from the least member of
S: the statement at that member evaluates to true, and the
statement at x + 1, with the sum to x + 1 unfolded to the sum to x plus f(x + 1) and that sum then replaced by g -- the hypothesis -- holds
at every member. A product unfolds with a factor. Only the shape with one sum or
product, standing alone on a side of the equation, is read; a statement that fails at
the least member is false.