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

proof

let n be Element of 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, Th49
.= (n *^ m) +^ (1 *^ m) by ORDINAL2:56
.= (n +^ 1) *^ m by ORDINAL3:54
.= (succ n) *^ m by ORDINAL2:48
.= (n + 1) *^ m by NAT_1:39 ; :: thesis: verum

end;

A3: S₁[ 0 ] by ORDINAL2:52;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A1);
hence n * m = n *^ m ; :: thesis: verum