deffunc H₁( non empty ManySortedSign , set , set ) -> ManySortedSign = $1 +* F₂($2,$3);
A2: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for x being set
for n being Nat holds
( H₁(S,x,n) is unsplit & H₁(S,x,n) is gate`1=arity & H<sub>1</sub>(S,x,n) is gate`2isBoolean & not H₁(S,x,n) is void & not H₁(S,x,n) is empty & H₁(S,x,n) is strict ) ;
thus ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F₅() & f . 0 = F₁() & h . 0 = F₃() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = H₁(S,x,n) & h . (n + 1) = F₄(x,n) ) ) ) from CIRCCMB2:sch 7(A1, A2); :: thesis: verum