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₆(S,A,x,n) is non-empty MSAlgebra over F₅(S,x,n) by A2;
consider f, g, h being ManySortedSet of NAT such that
A4: ( f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₄() ) 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₅(S,x,n) & g . (n + 1) = F₆(S,A,x,n) & h . (n + 1) = F₇(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₂[S,A,x,n] holds
S₂[F₅(S,x,n),F₆(S,A,x,n),F₇(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₂[S,A,x,n] holds
S₂[F₅(S,x,n),F₆(S,A,x,n),F₇(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₂[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₂[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₂[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₂[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₈() and
A12: A = g . F₈() ;
consider f1, h1 being ManySortedSet of NAT such that
A13: F₂() = f1 . F₈() and
A14: f1 . 0 = F₁() and
A15: h1 . 0 = F₄() 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₅(S,x,n) & h1 . (n + 1) = F₇(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₁[S,x,n] holds
S₁[F₅(S,x,n),F₇(x,n),n + 1] ;
defpred S₃[ 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₁[S,x, 0 ] ) by A14;
A19: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S₁[S,h1 . n,n] ) from CIRCCMB2:sch 2(A18, A16, A17);

A20: now :: thesis: for n being Nat st S₃[n] holds
S₃[n + 1]

let n be Nat; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume A21: S₃[n] ; :: thesis: S₃[n + 1]
ex S being non empty ManySortedSign st S = f1 . n by A19;
then A22: h1 . (n + 1) = F₇((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₃[n + 1] by A5, A21, A22; :: thesis: verum

end;

A23: S₃[ 0 ] by A4, A15;
A24: for i being Nat holds S₃[i] from NAT_1:sch 2(A23, A20);
defpred S₄[ 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;

A26: now :: thesis: for n being Nat st S₄[n] holds
S₄[n + 1]

let n be Nat; :: thesis: ( S₄[n] implies S₄[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₄[n] ; :: thesis: S₄[n + 1]
then f1 . (n + 1) = F₅(S,(h1 . n),n) by A16, A27
.= f . (n + 1) by A5, A25, A27, A28 ;
hence S₄[n + 1] ; :: thesis: verum

end;

A29: S₄[ 0 ] by A4, A14;
A30: for i being Nat holds S₄[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₂() by A13, A11;
take A ; :: thesis: ex f, g, h being ManySortedSet of NAT st
( F₂() = f . F₈() & A = g . F₈() & f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₄() & ( 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₅(S,x,n) & g . (n + 1) = F₆(S,A,x,n) & h . (n + 1) = F₇(x,n) ) ) )
take f ; :: thesis: ex g, h being ManySortedSet of NAT st
( F₂() = f . F₈() & A = g . F₈() & f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₄() & ( 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₅(S,x,n) & g . (n + 1) = F₆(S,A,x,n) & h . (n + 1) = F₇(x,n) ) ) )
take g ; :: thesis: ex h being ManySortedSet of NAT st
( F₂() = f . F₈() & A = g . F₈() & f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₄() & ( 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₅(S,x,n) & g . (n + 1) = F₆(S,A,x,n) & h . (n + 1) = F₇(x,n) ) ) )
take h ; :: thesis: ( F₂() = f . F₈() & A = g . F₈() & f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₄() & ( 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₅(S,x,n) & g . (n + 1) = F₆(S,A,x,n) & h . (n + 1) = F₇(x,n) ) ) )
thus ( F₂() = f . F₈() & A = g . F₈() & f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₄() & ( 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₅(S,x,n) & g . (n + 1) = F₆(S,A,x,n) & h . (n + 1) = F₇(x,n) ) ) ) by A4, A5, A13, A30, A12; :: thesis: verum