deffunc H₁( set , set ) -> set = (union { (Compound (s,$2)) where s is ofAtomicFormula Element of S : s is operational } ) \/ $2;
let IT1, IT2 be Function; :: thesis: ( dom IT1 = NAT & IT1 . 0 = AtomicTermsOf S & ( for n being Nat holds IT1 . (n + 1) = (union { (Compound (s,(IT1 . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (IT1 . n) ) & dom IT2 = NAT & IT2 . 0 = AtomicTermsOf S & ( for n being Nat holds IT2 . (n + 1) = (union { (Compound (s,(IT2 . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (IT2 . n) ) implies IT1 = IT2 )
assume A1: ( dom IT1 = NAT & IT1 . 0 = AtomicTermsOf S & ( for n being Nat holds IT1 . (n + 1) = H₁(n,IT1 . n) ) ) ; :: thesis: ( not dom IT2 = NAT or not IT2 . 0 = AtomicTermsOf S or ex n being Nat st not IT2 . (n + 1) = (union { (Compound (s,(IT2 . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (IT2 . n) or IT1 = IT2 )
A2: dom IT1 = NAT by A1;
A3: IT1 . 0 = AtomicTermsOf S by A1;
A4: for n being Nat holds IT1 . (n + 1) = H₁(n,IT1 . n) by A1;
assume A5: ( dom IT2 = NAT & IT2 . 0 = AtomicTermsOf S & ( for n being Nat holds IT2 . (n + 1) = H₁(n,IT2 . n) ) ) ; :: thesis: IT1 = IT2
A6: dom IT2 = NAT by A5;
A7: IT2 . 0 = AtomicTermsOf S by A5;
A8: for n being Nat holds IT2 . (n + 1) = H₁(n,IT2 . n) by A5;
thus IT1 = IT2 from NAT_1:sch 15(A2, A3, A4, A6, A7, A8); :: thesis: verum