let m, n be Nat; :: thesis: n * m = n *^ m
defpred S₁[ Nat] means $1 * m = $1 *^ m;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
thus (n + 1) * m = (n * m) + (1 * m)
.= (n *^ m) +^ m by A2, Th35
.= (n *^ m) +^ (1 *^ m) by ORDINAL2:39
.= (n +^ 1) *^ m by ORDINAL3:46
.= (succ (Segm n)) *^ m by ORDINAL2:31
.= (Segm (n + 1)) *^ m by NAT_1:38
.= (n + 1) *^ m ; :: thesis: verum

end;

A3: S₁[ 0 ] by ORDINAL2:35;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence n * m = n *^ m ; :: thesis: verum