A3: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n) by A2;
consider f, g, h being ManySortedSet of NAT such that
A4: ( f . 0 = F1() & g . 0 = F3() & h . 0 = F4() ) 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) from 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 & S2[S,A,x,n] holds
S2[F5(S,x,n),F6(S,A,x,n),F7(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 & S2[S,A,x,n] holds
S2[F5(S,x,n),F6(S,A,x,n),F7(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 & S2[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 & S2[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 & S2[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 & S2[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 . F8() and
A12: A = g . F8() ;
consider f1, h1 being ManySortedSet of NAT such that
A13: F2() = f1 . F8() and
A14: f1 . 0 = F1() and
A15: h1 . 0 = F4() 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) = F5(S,x,n) & h1 . (n + 1) = F7(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 & S1[S,x,n] holds
S1[F5(S,x,n),F7(x,n),n + 1] ;
defpred S3[ Nat] means h1 . \$1 = h . \$1;
A18: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S1[S,x, 0 ] ) by A14;
A19: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) from
A20: now :: thesis: for n being Nat st S3[n] holds
S3[n + 1]
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
assume A21: S3[n] ; :: thesis: S3[n + 1]
ex S being non empty ManySortedSign st S = f1 . n by A19;
then A22: h1 . (n + 1) = F7((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 S3[n + 1] by A5, A21, A22; :: thesis: verum
end;
A23: S3[ 0 ] by ;
A24: for i being Nat holds S3[i] from defpred S4[ 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 S4[n] holds
S4[n + 1]
let n be Nat; :: thesis: ( S4[n] implies S4[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 S4[n] ; :: thesis: S4[n + 1]
then f1 . (n + 1) = F5(S,(h1 . n),n) by
.= f . (n + 1) by A5, A25, A27, A28 ;
hence S4[n + 1] ; :: thesis: verum
end;
A29: S4[ 0 ] by ;
A30: for i being Nat holds S4[i] from 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 F2() by ;
take A ; :: thesis: ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )

take f ; :: thesis: ex g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )

take g ; :: thesis: ex h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )

take h ; :: thesis: ( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )

thus ( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( 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) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) by A4, A5, A13, A30, A12; :: thesis: verum