let i, j be Element of NAT ; :: thesis: [+] . <*i,j*> = i + j
reconsider q = <*i*> as Element of 1 -tuples_on NAT by FINSEQ_2:151;
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 r = <*i,j,(i + j)*> as Element of 3 -tuples_on NAT by FINSEQ_2:124;
assume S₂[j] ; :: thesis: S₂[j + 1]
then [+] . <*i,(j + 1)*> = (3 succ 3) . r by Th85
.= (r /. 3) + 1 by Def10
.= (i + j) + 1 by FINSEQ_4:27
.= i + (j + 1) ;
hence S₂[j + 1] ; :: thesis: verum

end;

[+] . <*i,0 *> = (1 proj 1) . q by Th83
.= q . 1 by Th42
.= i + 0 by FINSEQ_1:57 ;
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