let i, j be Nat; :: thesis: [*] . <*i,j*> = i * j
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
defpred S2[ Nat] means [*] . <*i,$1*> = i * $1;
A1: now :: thesis: for j being Nat st S2[j] holds
S2[j + 1]
let j be Nat; :: thesis: ( S2[j] implies S2[j + 1] )
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
assume S2[j] ; :: thesis: S2[j + 1]
then [*] . <*i1,(jj + 1)*> = ((1,2)->(1,?,2) [+]) . <*i,jj,(i * jj)*> by Th80
.= [+] . <*i1,(i1 * jj)*> by Th82
.= (i * 1) + (i * jj) by Th84
.= i * (j + 1) ;
hence S2[j + 1] ; :: thesis: verum
end;
reconsider ii = <*i1*> as Element of 1 -tuples_on NAT by FINSEQ_2:98;
[*] . <*i,0*> = (1 const 0) . ii by Th78
.= i * 0 ;
then A2: S2[ 0 ] ;
for i being Nat holds S2[i] from NAT_1:sch 2(A2, A1);
 hence [*] . <*i,j*> = i * j ; :: thesis: verum