let i be Element of NAT ; :: thesis: for j being Element of NAT holds [*] . <*i,j*> = i * j
defpred S2[ Element of NAT ] means [*] . <*i,$1*> = i * $1;
A1: now
let j be Element of NAT ; :: thesis: ( S2[j] implies S2[j + 1] )
assume S2[j] ; :: thesis: S2[j + 1]
then [*] . <*i,(j + 1)*> = ((1,2)->(1,?,2) [+]) . <*i,j,(i * j)*> by Th85
.= [+] . <*i,(i * j)*> by Th87
.= (i * 1) + (i * j) by Th89
.= i * (j + 1) ;
hence S2[j + 1] ; :: thesis: verum
end;
reconsider ii = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:98;
[*] . <*i,0*> = (1 const 0) . ii by Th83
.= i * 0 by FUNCOP_1:7 ;
then A2: S2[ 0 ] ;
thus for i being Element of NAT holds S2[i] from NAT_1:sch 1(A2, A1); :: thesis: verum