consider f, h being ManySortedSet of NAT such that

A1: ( f . 0 = F_{1}() & h . 0 = F_{2}() )
and

A2: 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_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) )
from CIRCCMB2:sch 1();

A3: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f . n & x = h . n & S_{1}[S,x,n] holds

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

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

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

for n being Nat ex S being non empty ManySortedSign st

( S = f . n & S_{1}[S,h . n,n] )
from CIRCCMB2:sch 2(A4, A2, A3);

then consider S being non empty ManySortedSign such that

A5: S = f . F_{5}()
;

take S ; :: thesis: ex f, h being ManySortedSet of NAT st

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

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

thus ( S = f . F_{5}() & f . 0 = F_{1}() & h . 0 = F_{2}() & ( 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_{3}(S,x,n) & h . (n + 1) = F_{4}(x,n) ) ) )
by A1, A2, A5; :: thesis: verum

A1: ( f . 0 = F

A2: 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

A3: for n being Nat

for S being non empty ManySortedSign

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

S

A4: 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 consider S being non empty ManySortedSign such that

A5: S = f . F

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