let i, j be Nat; :: thesis: [+] . <*i,j*> = i + j
reconsider i = i, j = j as Element of NAT by ORDINAL1:def 12;
reconsider q = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:131;
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;
reconsider r = <*i,jj,(i + jj)*> as Element of 3 -tuples_on NAT by FINSEQ_2:104;
assume S2[j] ; :: thesis: S2[j + 1]
then [+] . <*i,(jj + 1)*> = (3 succ 3) . r by Th80
.= (r . 3) + 1 by Def7
.= i + (j + 1) ;
hence S2[j + 1] ; :: thesis: verum
end;
[+] . <*i,0*> = (1 proj 1) . q by Th78
.= q . 1 by Th37
.= i + 0 ;
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