let i be Element of NAT ; :: thesis: ( [pred] . <*0*> = 0 & [pred] . <*(i + 1)*> = i )
0 -tuples_on NAT = {{}} by Th5;
then A1: {} in 0 -tuples_on NAT by TARSKI:def 1;
defpred S2[ Nat] means [pred] . <*($1 + 1)*> = $1;
reconsider p0 = <*0,0*> as Element of 2 -tuples_on NAT by FINSEQ_2:101;
A2: arity (0 const 0) = 0 by Th31;
A3: arity (2 proj 1) = 2 by Th36;
A4: now :: thesis: for i being Nat st S2[i] holds
S2[i + 1]
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
reconsider p0 = <*(i1 + 1),i1*> as Element of 2 -tuples_on NAT by FINSEQ_2:101;
assume S2[i] ; :: thesis: S2[i + 1]
then [pred] . <*((i + 1) + 1)*> = (2 proj 1) . p0 by A2, A3, Th81
.= <*(i + 1),i*> . 1 by Th37
.= i + 1 by FINSEQ_1:44 ;
hence S2[i + 1] ; :: thesis: verum
end;
thus [pred] . <*0*> = (0 const 0) . {} by A2, Th79
.= 0 by A1, FUNCOP_1:7 ; :: thesis: [pred] . <*(i + 1)*> = i
then [pred] . <*(0 + 1)*> = (2 proj 1) . p0 by A2, A3, Th81
.= <*0,0*> . 1 by Th37
.= 0 by FINSEQ_1:44 ;
then A5: S2[ 0 ] ;
for i being Nat holds S2[i] from NAT_1:sch 2(A5, A4);
 hence [pred] . <*(i + 1)*> = i ; :: thesis: verum