deffunc H₁( set , set ) -> set = (union { (Compound (s,$2)) where s is ofAtomicFormula Element of S : s is operational } ) \/ $2;
ex f being Function st
( dom f = NAT & f . 0 = AtomicTermsOf S & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 11();
hence ex b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = AtomicTermsOf S & ( for n being Nat holds b₁ . (n + 1) = (union { (Compound (s,(b₁ . n))) where s is ofAtomicFormula Element of S : s is operational } ) \/ (b₁ . n) ) ) ; :: thesis: verum