let i be Element of NAT ; :: thesis: ( [pred] . <*0 *> = 0 & [pred] . <*(i + 1)*> = i )
A1: arity (0 const 0 ) = 0 by Th35;
0 -tuples_on NAT = {{} } by Th8;
then A2: {} in 0 -tuples_on NAT by TARSKI:def 1;
thus A3: [pred] . <*0 *> = (0 const 0 ) . {} by A1, Th84
.= 0 by A2, FUNCOP_1:13 ; :: thesis: [pred] . <*(i + 1)*> = i
A4: arity (2 proj 1) = 2 by Th41;
reconsider p0 = <*0 ,0 *> as Element of 2 -tuples_on NAT by FINSEQ_2:121;
defpred S2[ Element of NAT ] means [pred] . <*($1 + 1)*> = $1;
A5: S2[ 0 ]
proof
thus [pred] . <*(0 + 1)*> = (2 proj 1) . p0 by A1, A3, A4, Th86
.= <*0 ,0 *> . 1 by Th42
.= 0 by FINSEQ_1:61 ; :: thesis: verum
end;
A6: now
let i be Element of NAT ; :: thesis: ( S2[i] implies S2[i + 1] )
assume A7: S2[i] ; :: thesis: S2[i + 1]
reconsider p0 = <*(i + 1),i*> as Element of 2 -tuples_on NAT by FINSEQ_2:121;
[pred] . <*((i + 1) + 1)*> = (2 proj 1) . p0 by A1, A4, A7, Th86
.= <*(i + 1),i*> . 1 by Th42
.= i + 1 by FINSEQ_1:61 ;
hence S2[i + 1] ; :: thesis: verum
end;
for i being Element of NAT holds S2[i] from NAT_1:sch 1(A5, A6);
 hence [pred] . <*(i + 1)*> = i ; :: thesis: verum