let i, j be Nat; :: thesis: [^] . <*i,j*> = i |^ j
defpred S2[ Nat] means [^] . <*i,$1*> = i |^ $1;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
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;
reconsider ij = i |^ jj as Element of NAT ;
assume S2[j] ; :: thesis: S2[j + 1]
then [^] . <*i,(jj + 1)*> = ((1,2)->(1,?,2) [*]) . <*i,jj,ij*> by Th80
.= [*] . <*i,ij*> by Th82
.= i * ij by Th85
.= i |^ (j + 1) by NEWTON:6 ;
hence S2[j + 1] ; :: thesis: verum
end;
reconsider ii = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:131;
[^] . <*i,0*> = (1 const 1) . ii by Th78
.= i |^ 0 by NEWTON:4 ;
then A2: S2[ 0 ] ;
for j being Nat holds S2[j] from NAT_1:sch 2(A2, A1);
 hence [^] . <*i,j*> = i |^ j ; :: thesis: verum