deffunc H_{1}( non empty ManySortedSign , set , set ) -> ManySortedSign = $1 +* F_{2}($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_{1}(S,x,n) is unsplit & H_{1}(S,x,n) is gate`1=arity & H_{1}(S,x,n) is gate`2isBoolean & not H_{1}(S,x,n) is void & not H_{1}(S,x,n) is empty & H_{1}(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_{5}() & f . 0 = F_{1}() & h . 0 = F_{3}() & ( 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_{1}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )
from CIRCCMB2:sch 7(A1, A2); :: thesis: verum

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

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

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n holds

( f . (n + 1) = H