A8:
for n being Nat holds S1[n]
fromNAT_1:sch 2(A2, A3); defpred S2[ Nat] means (uInt. n)+(uInt. $1)=uInt.(n + $1); A9:
S2[ 0 ]
byA1; A10:
for m being Nat st S2[m] holds S2[m + 1]
A1: uInt.0=0_NobyDef1; defpred S1[ Nat] means for n, m being Nat st n + m = $1 holds (uInt. n)*(uInt. m)==uInt.(n * m); A2:
for k being Nat st ( for n being Nat st n < k holds S1[n] ) holds S1[k]