defpred S_{2}[ 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 S_{3}[ non empty ManySortedSign , object , object ] means S_{2}[$1,$2];

consider S being non empty ManySortedSign , f, h being ManySortedSet of NAT such that

A3: ( S = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{3}() )
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) = F_{2}(S,x,n) & h . (n + 1) = F_{4}(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 & S_{3}[S,x,n] holds

S_{3}[F_{2}(S,x,n),F_{4}(x,n),n + 1]
by A2;

A6: ex S being non empty ManySortedSign ex x being set st

( S = f . 0 & x = h . 0 & S_{3}[S,x, 0 ] )
by A1, A3;

for n being Nat ex S being non empty ManySortedSign st

( S = f . n & S_{3}[S,h . n,n] )
from CIRCCMB2:sch 2(A6, A4, A5);

then ex S being non empty ManySortedSign st

( S = f . F_{5}() & S_{2}[S,F_{5}()] )
;

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 . 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) = F_{2}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )

take f ; :: thesis: ex 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) = F_{2}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )

take h ; :: thesis: ( 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) = F_{2}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )

thus ( 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) = F_{2}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )
by A3, A4; :: thesis: verum

defpred S

consider S being non empty ManySortedSign , f, h being ManySortedSet of NAT such that

A3: ( S = f . F

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) = F

A5: for n being Nat

for S being non empty ManySortedSign

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

S

A6: ex S being non empty ManySortedSign ex x being set st

( S = f . 0 & x = h . 0 & S

for n being Nat ex S being non empty ManySortedSign st

( S = f . n & S

then ex S being non empty ManySortedSign st

( S = f . F

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 . F

for S being non empty ManySortedSign

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

( f . (n + 1) = F

take f ; :: thesis: ex 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) = F

take h ; :: thesis: ( S = f . F

for S being non empty ManySortedSign

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

( f . (n + 1) = F

thus ( S = f . F

for S being non empty ManySortedSign

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

( f . (n + 1) = F