consider f, h being ManySortedSet of NAT such that
A1: ( f . 0 = F₁() & h . 0 = F₂() ) 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₃(S,x,n) & h . (n + 1) = F₄(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₁[S,x,n] holds
S₁[F₃(S,x,n),F₄(x,n),n + 1] ;
A4: ex S being non empty ManySortedSign ex x being set st
( S = f . 0 & x = h . 0 & S₁[S,x, 0 ] ) by A1;
for n being Nat ex S being non empty ManySortedSign st
( S = f . n & S₁[S,h . n,n] ) from CIRCCMB2:sch 2(A4, A2, A3);
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₅() & 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) = F₃(S,x,n) & h . (n + 1) = F₄(x,n) ) ) )
take f ; :: thesis: ex 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) = F₃(S,x,n) & h . (n + 1) = F₄(x,n) ) ) )
take h ; :: thesis: ( 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) = F₃(S,x,n) & h . (n + 1) = F₄(x,n) ) ) )
thus ( 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) = F₃(S,x,n) & h . (n + 1) = F₄(x,n) ) ) ) by A1, A2, A5; :: thesis: verum