A3:
for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

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

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

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

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 holds

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

A6: 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_{5}(S,x,n),F_{6}(S,A,x,n),F_{7}(x,n),n + 1]
;

A7: 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_{5}(S,x,n),F_{6}(S,A,x,n),F_{7}(x,n),n + 1]
;

A8: 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 A4;

A9: 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(A8, A5, A7, A3);

A10: 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 A4;

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(A10, A5, A6, A3);

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

A11: S = f . F_{8}()
and

A12: A = g . F_{8}()
;

consider f1, h1 being ManySortedSet of NAT such that

A13: F_{2}() = f1 . F_{8}()
and

A14: f1 . 0 = F_{1}()
and

A15: h1 . 0 = F_{4}()
and

A16: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f1 . n & x = h1 . n holds

( f1 . (n + 1) = F_{5}(S,x,n) & h1 . (n + 1) = F_{7}(x,n) )
by A1;

A17: for n being Nat

for S being non empty ManySortedSign

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

S_{1}[F_{5}(S,x,n),F_{7}(x,n),n + 1]
;

defpred S_{3}[ Nat] means h1 . $1 = h . $1;

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

( S = f1 . 0 & x = h1 . 0 & S_{1}[S,x, 0 ] )
by A14;

A19: for n being Nat ex S being non empty ManySortedSign st

( S = f1 . n & S_{1}[S,h1 . n,n] )
from CIRCCMB2:sch 2(A18, A16, A17);

_{3}[ 0 ]
by A4, A15;

A24: for i being Nat holds S_{3}[i]
from NAT_1:sch 2(A23, A20);

defpred S_{4}[ Nat] means f1 . $1 = f . $1;

for i being object st i in NAT holds

h1 . i = h . i by A24;

then A25: h1 = h by PBOOLE:3;

_{4}[ 0 ]
by A4, A14;

A30: for i being Nat holds S_{4}[i]
from NAT_1:sch 2(A29, A26);

then for i being object st i in NAT holds

f1 . i = f . i ;

then f1 = f by PBOOLE:3;

then reconsider A = A as non-empty MSAlgebra over F_{2}() by A13, A11;

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

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

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

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

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

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

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

thus ( F_{2}() = f . F_{8}() & A = g . F_{8}() & f . 0 = F_{1}() & g . 0 = F_{3}() & h . 0 = F_{4}() & ( 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_{5}(S,x,n) & g . (n + 1) = F_{6}(S,A,x,n) & h . (n + 1) = F_{7}(x,n) ) ) )
by A4, A5, A13, A30, A12; :: 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

A4: ( f . 0 = 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 holds

( f . (n + 1) = F

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

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

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

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

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

A11: S = f . F

A12: A = g . F

consider f1, h1 being ManySortedSet of NAT such that

A13: F

A14: f1 . 0 = F

A15: h1 . 0 = F

A16: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f1 . n & x = h1 . n holds

( f1 . (n + 1) = F

A17: for n being Nat

for S being non empty ManySortedSign

for x being set st S = f1 . n & x = h1 . n & S

S

defpred S

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

( S = f1 . 0 & x = h1 . 0 & S

A19: for n being Nat ex S being non empty ManySortedSign st

( S = f1 . n & S

A20: now :: thesis: for n being Nat st S_{3}[n] holds

S_{3}[n + 1]

A23:
SS

let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

assume A21: S_{3}[n]
; :: thesis: S_{3}[n + 1]

ex S being non empty ManySortedSign st S = f1 . n by A19;

then A22: h1 . (n + 1) = F_{7}((h1 . n),n)
by A16;

ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . n & A = g . n ) by A9;

hence S_{3}[n + 1]
by A5, A21, A22; :: thesis: verum

end;assume A21: S

ex S being non empty ManySortedSign st S = f1 . n by A19;

then A22: h1 . (n + 1) = F

ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st

( S = f . n & A = g . n ) by A9;

hence S

A24: for i being Nat holds S

defpred S

for i being object st i in NAT holds

h1 . i = h . i by A24;

then A25: h1 = h by PBOOLE:3;

A26: now :: thesis: for n being Nat st S_{4}[n] holds

S_{4}[n + 1]

A29:
SS

let n be Nat; :: thesis: ( S_{4}[n] implies S_{4}[n + 1] )

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

A27: S = f . n and

A28: A = g . n by A9;

assume S_{4}[n]
; :: thesis: S_{4}[n + 1]

then f1 . (n + 1) = F_{5}(S,(h1 . n),n)
by A16, A27

.= f . (n + 1) by A5, A25, A27, A28 ;

hence S_{4}[n + 1]
; :: thesis: verum

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

A27: S = f . n and

A28: A = g . n by A9;

assume S

then f1 . (n + 1) = F

.= f . (n + 1) by A5, A25, A27, A28 ;

hence S

A30: for i being Nat holds S

then for i being object st i in NAT holds

f1 . i = f . i ;

then f1 = f by PBOOLE:3;

then reconsider A = A as non-empty MSAlgebra over F

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

( 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

( 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

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