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_{4}() . n & A = F_{6}() . n & x = F_{8}() . n holds

( F_{4}() . (n + 1) = F_{1}(S,x,n) & F_{6}() . (n + 1) = F_{2}(S,A,x,n) & F_{8}() . (n + 1) = F_{3}(x,n) )
by A3;

set f1 = F_{4}();

set g1 = F_{6}();

set h1 = F_{8}();

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_{4}() . n & A = F_{6}() . n & x = F_{8}() . n & S_{2}[S,A,x,n] holds

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

A8: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F_{2}(S,A,x,n) is non-empty MSAlgebra over F_{1}(S,x,n)
by A5;

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

( S = F_{4}() . 0 & A = F_{6}() . 0 & x = F_{8}() . 0 & S_{2}[S,A,x, 0 ] )
by A1;

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

( S = F_{4}() . n & A = F_{6}() . n & S_{2}[S,A,F_{8}() . n,n] )
from CIRCCMB2:sch 13(A9, A6, A7, A8);

set f2 = F_{5}();

set g2 = F_{7}();

set h2 = F_{9}();

A11: 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_{5}() . n & A = F_{7}() . n & x = F_{9}() . n & S_{2}[S,A,x,n] holds

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

defpred S_{3}[ Nat] means F_{8}() . $1 = F_{9}() . $1;

A12: 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_{5}() . n & A = F_{7}() . n & x = F_{9}() . n holds

( F_{5}() . (n + 1) = F_{1}(S,x,n) & F_{7}() . (n + 1) = F_{2}(S,A,x,n) & F_{9}() . (n + 1) = F_{3}(x,n) )
by A4;

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

( S = F_{5}() . 0 & A = F_{7}() . 0 & x = F_{9}() . 0 & S_{2}[S,A,x, 0 ] )
by A1, A2;

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

( S = F_{5}() . n & A = F_{7}() . n & S_{2}[S,A,F_{9}() . n,n] )
from CIRCCMB2:sch 13(A13, A12, A11, A8);

_{3}[ 0 ]
by A2;

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

then A19: for i being object st i in NAT holds

F_{8}() . i = F_{9}() . i
;

defpred S_{4}[ Nat] means ( F_{4}() . $1 = F_{5}() . $1 & F_{6}() . $1 = F_{7}() . $1 );

A20: F_{8}() = F_{9}()
by A19, PBOOLE:3;

_{4}[ 0 ]
by A2;

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

then ( ( for i being object st i in NAT holds

F_{4}() . i = F_{5}() . i ) & ( for i being object st i in NAT holds

F_{6}() . i = F_{7}() . i ) )
;

hence ( F_{4}() = F_{5}() & F_{6}() = F_{7}() & F_{8}() = F_{9}() )
by A19, PBOOLE:3; :: thesis: verum

for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set st S = F

( F

set f1 = F

set g1 = F

set h1 = F

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

S

A8: for S being non empty ManySortedSign

for A being non-empty MSAlgebra over S

for x being set

for n being Nat holds F

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

( S = F

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

( S = F

set f2 = F

set g2 = F

set h2 = F

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

S

defpred S

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

( F

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

( S = F

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

( S = F

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

S_{3}[n + 1]

A18:
SS

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

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

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

( S = F_{4}() . n & A = F_{6}() . n )
by A10;

then A17: F_{8}() . (n + 1) = F_{3}((F_{8}() . n),n)
by A3;

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

( S = F_{5}() . n & A = F_{7}() . n )
by A14;

hence S_{3}[n + 1]
by A4, A16, A17; :: thesis: verum

end;assume A16: S

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

( S = F

then A17: F

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

( S = F

hence S

for i being Nat holds S

then A19: for i being object st i in NAT holds

F

defpred S

A20: F

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

S_{4}[n + 1]

A25:
SS

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

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

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

A23: ( S = F_{4}() . n & A = F_{6}() . n )
by A10;

A24: F_{6}() . (n + 1) =
F_{2}(S,A,(F_{8}() . n),n)
by A3, A23

.= F_{7}() . (n + 1)
by A4, A20, A22, A23
;

F_{4}() . (n + 1) =
F_{1}(S,(F_{8}() . n),n)
by A3, A23

.= F_{5}() . (n + 1)
by A4, A20, A22, A23
;

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

end;assume A22: S

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

A23: ( S = F

A24: F

.= F

F

.= F

hence S

for i being Nat holds S

then ( ( for i being object st i in NAT holds

F

F

hence ( F