A2:
for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F_{5}(S,A,x,n) is non-empty MSAlgebra over F_{4}(S,x,n)
by A1;

consider f, g, h being ManySortedSet of NAT such that

A3: ( f . 0 = F_{1}() & g . 0 = F_{2}() & h . 0 = F_{3}() )
and

A4: for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) )
from CIRCCMB2:sch 12();

A5: for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

S_{2}[F_{4}(S,x,n),F_{5}(S,A,x,n),F_{6}(x,n),n + 1]
;

A6: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st

( S = f . 0 & A = g . 0 & x = h . 0 & S_{2}[S,A,x, 0 ] )
by A3;

for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

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

then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that

A7: ( S = f . F_{7}() & A = g . F_{7}() )
;

take S ; :: thesis: ex A being non-empty MSAlgebra over S ex f, g, h being ManySortedSet of NAT st

( S = f . F_{7}() & A = g . F_{7}() & f . 0 = F_{1}() & g . 0 = F_{2}() & h . 0 = F_{3}() & ( for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

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

( S = f . F_{7}() & A = g . F_{7}() & f . 0 = F_{1}() & g . 0 = F_{2}() & h . 0 = F_{3}() & ( for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

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

( S = f . F_{7}() & A = g . F_{7}() & f . 0 = F_{1}() & g . 0 = F_{2}() & h . 0 = F_{3}() & ( for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

take g ; :: thesis: ex h being ManySortedSet of NAT st

( S = f . F_{7}() & A = g . F_{7}() & f . 0 = F_{1}() & g . 0 = F_{2}() & h . 0 = F_{3}() & ( for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

take h ; :: thesis: ( S = f . F_{7}() & A = g . F_{7}() & f . 0 = F_{1}() & g . 0 = F_{2}() & h . 0 = F_{3}() & ( for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )

thus ( S = f . F_{7}() & A = g . F_{7}() & f . 0 = F_{1}() & g . 0 = F_{2}() & h . 0 = F_{3}() & ( for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F_{4}(S,x,n) & g . (n + 1) = F_{5}(S,A,x,n) & h . (n + 1) = F_{6}(x,n) ) ) )
by A3, A4, A7; :: thesis: verum

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

consider f, g, h being ManySortedSet of NAT such that

A3: ( f . 0 = F

A4: for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

A5: for n being Nat

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

S

A6: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st

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

for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . n & A = g . n & S

then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that

A7: ( S = f . F

take S ; :: thesis: ex A being non-empty MSAlgebra over S ex f, g, h being ManySortedSet of NAT st

( S = f . F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

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

( S = f . F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

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

( S = f . F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

take g ; :: thesis: ex h being ManySortedSet of NAT st

( S = f . F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

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

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F

thus ( S = f . F

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

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

( f . (n + 1) = F