reconsider N = F1() as Element of NAT by ORDINAL1:def 12;
defpred S1[ Nat] means ex n being Nat st P1[$1,n];
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
given n being Nat such that A3: P1[k,n] ; :: thesis: S1[k + 1]
reconsider F = F2((k + 1),n) as Element of NAT by ORDINAL1:def 12;
take F ; :: thesis: P1[k + 1,F]
thus P1[k + 1,F] by A1, A3; :: thesis: verum
end;
P1[ 0 ,N] by A1;
then A4: S1[ 0 ] ;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A4, A2); :: thesis: for k, n, m being Nat st P1[k,n] & P1[k,m] holds
n = m
defpred S2[ Nat] means for n, m being Nat st P1[$1,n] & P1[$1,m] holds
n = m;
A5: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A6: for n, m being Nat st P1[k,n] & P1[k,m] holds
n = m ; :: thesis: S2[k + 1]
let n, m be Nat; :: thesis: ( P1[k + 1,n] & P1[k + 1,m] implies n = m )
assume ( P1[k + 1,n] & P1[k + 1,m] ) ; :: thesis: n = m
then ( ex l, u being Nat st
( k + 1 = l + 1 & P1[l,u] & n = F2((k + 1),u) ) & ex v, w being Nat st
( k + 1 = v + 1 & P1[v,w] & m = F2((k + 1),w) ) ) by A1;
hence n = m by A6; :: thesis: verum
end;
A7: S2[ 0 ]
proof
let n, m be Nat; :: thesis: ( P1[ 0 ,n] & P1[ 0 ,m] implies n = m )
assume that
A8: P1[ 0 ,n] and
A9: P1[ 0 ,m] ; :: thesis: n = m
for m, l being Nat holds
( not 0 = m + 1 or not P1[m,l] or not n = F2(0,l) ) ;
then ( ( for n, l being Nat holds
( not 0 = n + 1 or not P1[n,l] or not m = F2(0,l) ) ) & n = F1() ) by A1, A8;
hence n = m by A1, A9; :: thesis: verum
end;
thus for k being Nat holds S2[k] from NAT_1:sch 2(A7, A5); :: thesis: verum