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 = F4() . n & A = F6() . n & x = F8() . n holds
( F4() . (n + 1) = F1(S,x,n) & F6() . (n + 1) = F2(S,A,x,n) & F8() . (n + 1) = F3(x,n) ) by A3;
set f1 = F4();
set g1 = F6();
set h1 = F8();
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 = F4() . n & A = F6() . n & x = F8() . n & S2[S,A,x,n] holds
S2[F1(S,x,n),F2(S,A,x,n),F3(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 F2(S,A,x,n) is non-empty MSAlgebra over F1(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 = F4() . 0 & A = F6() . 0 & x = F8() . 0 & S2[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 = F4() . n & A = F6() . n & S2[S,A,F8() . n,n] ) from CIRCCMB2:sch 13(A9, A6, A7, A8);
 set f2 = F5();
set g2 = F7();
set h2 = F9();
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 = F5() . n & A = F7() . n & x = F9() . n & S2[S,A,x,n] holds
S2[F1(S,x,n),F2(S,A,x,n),F3(x,n),n + 1] ;
defpred S3[ Nat] means F8() . $1 = F9() . $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 = F5() . n & A = F7() . n & x = F9() . n holds
( F5() . (n + 1) = F1(S,x,n) & F7() . (n + 1) = F2(S,A,x,n) & F9() . (n + 1) = F3(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 = F5() . 0 & A = F7() . 0 & x = F9() . 0 & S2[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 = F5() . n & A = F7() . n & S2[S,A,F9() . n,n] ) from CIRCCMB2:sch 13(A13, A12, A11, A8);
A15: 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 A16: S3[n] ; :: thesis: S3[n + 1]
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F4() . n & A = F6() . n ) by A10;
then A17: F8() . (n + 1) = F3((F8() . n),n) by A3;
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F5() . n & A = F7() . n ) by A14;
hence S3[n + 1] by A4, A16, A17; :: thesis: verum
end;
A18: S3[ 0 ] by A2;
for i being Nat holds S3[i] from NAT_1:sch 2(A18, A15);
 then A19: for i being object st i in NAT holds
F8() . i = F9() . i ;
defpred S4[ Nat] means ( F4() . $1 = F5() . $1 & F6() . $1 = F7() . $1 );
A20: F8() = F9() by A19, PBOOLE:3;
A21: now :: thesis: for n being Nat st S4[n] holds
S4[n + 1]
let n be Nat; :: thesis: ( S4[n] implies S4[n + 1] )
assume A22: S4[n] ; :: thesis: S4[n + 1]
consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A23: ( S = F4() . n & A = F6() . n ) by A10;
A24: F6() . (n + 1) = F2(S,A,(F8() . n),n) by A3, A23
.= F7() . (n + 1) by A4, A20, A22, A23 ;
F4() . (n + 1) = F1(S,(F8() . n),n) by A3, A23
.= F5() . (n + 1) by A4, A20, A22, A23 ;
hence S4[n + 1] by A24; :: thesis: verum
end;
A25: S4[ 0 ] by A2;
for i being Nat holds S4[i] from NAT_1:sch 2(A25, A21);
 then ( ( for i being object st i in NAT holds
F4() . i = F5() . i ) & ( for i being object st i in NAT holds
F6() . i = F7() . i ) ) ;
hence ( F4() = F5() & F6() = F7() & F8() = F9() ) by A19, PBOOLE:3; :: thesis: verum