defpred S2[ non empty ManySortedSign , object ] means ( $1 is unsplit & $1 is gate`1=arity & $1 is gate`2isBoolean & not $1 is void & $1 is strict );
defpred S3[ non empty ManySortedSign , object , object ] means S2[$1,$2];
consider S being non empty ManySortedSign , f, h being ManySortedSet of NAT such that
A3: ( S = f . F5() & f . 0 = F1() & h . 0 = F3() ) and
A4: 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) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) from CIRCCMB2:sch 4();
 A5: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n & S3[S,x,n] holds
S3[F2(S,x,n),F4(x,n),n + 1] by A2;
A6: ex S being non empty ManySortedSign ex x being set st
( S = f . 0 & x = h . 0 & S3[S,x, 0 ] ) by A1, A3;
for n being Nat ex S being non empty ManySortedSign st
( S = f . n & S3[S,h . n,n] ) from CIRCCMB2:sch 2(A6, A4, A5);
 then ex S being non empty ManySortedSign st
( S = f . F5() & S2[S,F5()] ) ;
then reconsider S = S as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A3;
take S ; :: thesis: ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( 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) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
take f ; :: thesis: ex h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( 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) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
take h ; :: thesis: ( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( 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) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
thus ( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( 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) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) by A3, A4; :: thesis: verum