let IT1, IT2 be Function; :: thesis: ( 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 C1: ( dom IT1 = NAT & IT1 . 0 = x . 1 & ( for n being Nat holds IT1 . (n + 1) = f . ((IT1 . n),(x . (n + 2))) ) ) ; :: thesis: ( 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 C2: ( dom IT2 = NAT & IT2 . 0 = x . 1 & ( for n being Nat holds IT2 . (n + 1) = f . ((IT2 . n),(x . (n + 2))) ) ) ; :: thesis: IT1 = IT2
deffunc H₁( Nat, set ) -> set = f . ($2,(x . ($1 + 2)));
B1: dom IT1 = NAT by C1;
B2: IT1 . 0 = x . 1 by C1;
B3: for n being Nat holds IT1 . (n + 1) = H₁(n,IT1 . n) by C1;
B4: dom IT2 = NAT by C2;
B5: IT2 . 0 = x . 1 by C2;
B6: for n being Nat holds IT2 . (n + 1) = H₁(n,IT2 . n) by C2;
thus IT1 = IT2 from NAT_1:sch 15(B1, B2, B3, B4, B5, B6); :: thesis: verum