let i be Element of NAT ; :: thesis: ( [pred] . <*0*> = 0 & [pred] . <*(i + 1)*> = i )
0 -tuples_on NAT = {{}} by Th8;
then A1: {} in 0 -tuples_on NAT by TARSKI:def 1;
defpred S2[ Element of 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 Th35;
A3: arity (2 proj 1) = 2 by Th41;
A4: now
let i be Element of NAT ; :: thesis: ( S2[i] implies S2[i + 1] )
reconsider p0 = <*(i + 1),i*> 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, Th86
.= <*(i + 1),i*> . 1 by Th42
.= i + 1 by FINSEQ_1:44 ;
hence S2[i + 1] ; :: thesis: verum
end;
thus [pred] . <*0*> = (0 const 0) . {} by A2, Th84
.= 0 by A1, FUNCOP_1:7 ; :: thesis: [pred] . <*(i + 1)*> = i
then [pred] . <*(0 + 1)*> = (2 proj 1) . p0 by A2, A3, Th86
.= <*0,0*> . 1 by Th42
.= 0 by FINSEQ_1:44 ;
then A5: S2[ 0 ] ;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A5, A4);
 hence [pred] . <*(i + 1)*> = i ; :: thesis: verum