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

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
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:

end;