let i, j be Element of NAT ; :: thesis: [^] . <*i,j*> = i |^ j
defpred S₂[ Element of NAT ] means [^] . <*i,$1*> = i |^ $1;

A1: now

let j be Element of NAT ; :: thesis: ( S₂[j] implies S₂[j + 1] )
reconsider ij = i |^ j as Element of NAT ;
assume S₂[j] ; :: thesis: S₂[j + 1]
then [^] . <*i,(j + 1)*> = ((1,2)->(1,?,2) [*]) . <*i,j,ij*> by Th85
.= [*] . <*i,ij*> by Th87
.= i * ij by Th90
.= i |^ (j + 1) by NEWTON:11 ;
hence S₂[j + 1] ; :: thesis: verum

end;

reconsider ii = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:151;
[^] . <*i,0*> = (1 const 1) . ii by Th83
.= 1 by FUNCOP_1:13
.= i |^ 0 by NEWTON:9 ;
then A2: S₂[ 0 ] ;
for j being Element of NAT holds S₂[j] from NAT_1:sch 1(A2, A1);
hence [^] . <*i,j*> = i |^ j ; :: thesis: verum