let IT1, IT2 be Function; ( dom IT1 = NAT & IT1 . 0 = x . 1 & ( for n being Nat holds IT1 . (n + 1) = f . ((IT1 . n),(x . (n + 2))) ) & dom IT2 = NAT & IT2 . 0 = x . 1 & ( for n being Nat holds IT2 . (n + 1) = f . ((IT2 . n),(x . (n + 2))) ) implies IT1 = IT2 )
assume A2:
( dom IT1 = NAT & IT1 . 0 = x . 1 & ( for n being Nat holds IT1 . (n + 1) = f . ((IT1 . n),(x . (n + 2))) ) )
; ( not dom IT2 = NAT or not IT2 . 0 = x . 1 or ex n being Nat st not IT2 . (n + 1) = f . ((IT2 . n),(x . (n + 2))) or IT1 = IT2 )
assume A3:
( dom IT2 = NAT & IT2 . 0 = x . 1 & ( for n being Nat holds IT2 . (n + 1) = f . ((IT2 . n),(x . (n + 2))) ) )
; IT1 = IT2
deffunc H1( Nat, set ) -> set = f . ($2,(x . ($1 + 2)));
A4:
dom IT1 = NAT
by A2;
A5:
IT1 . 0 = x . 1
by A2;
A6:
for n being Nat holds IT1 . (n + 1) = H1(n,IT1 . n)
by A2;
A7:
dom IT2 = NAT
by A3;
A8:
IT2 . 0 = x . 1
by A3;
A9:
for n being Nat holds IT2 . (n + 1) = H1(n,IT2 . n)
by A3;
thus
IT1 = IT2
from NAT_1:sch 15(A4, A5, A6, A7, A8, A9); verum