A6: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for x being set st S = F₄() . n & A = F₆() . n & x = F₈() . n holds
( F₄() . (n + 1) = F₁(S,x,n) & F₆() . (n + 1) = F₂(S,A,x,n) & F₈() . (n + 1) = F₃(x,n) ) by A3;
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 of S
for x being set st S = F₄() . n & A = F₆() . n & x = F₈() . n & S₂[S,A,x,n] holds
S₂[F₁(S,x,n),F₂(S,A,x,n),F₃(x,n),n + 1] ;
A8: for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for x being set
for n being Nat holds F₂(S,A,x,n) is non-empty MSAlgebra of F₁(S,x,n) by A5;
A9: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of S ex x being set st
( S = F₄() . 0 & A = F₆() . 0 & x = F₈() . 0 & S₂[S,A,x, 0 ] ) by A1;
A10: for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of S st
( S = F₄() . n & A = F₆() . n & S₂[S,A,F₈() . n,n] ) from CIRCCMB2:sch 13(A9, A6, A7, A8);
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 of S
for x being set st S = F₅() . n & A = F₇() . n & x = F₉() . n & S₂[S,A,x,n] holds
S₂[F₁(S,x,n),F₂(S,A,x,n),F₃(x,n),n + 1] ;
defpred S₃[ Nat] means F₈() . $1 = F₉() . $1;
A12: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra of S
for x being set st S = F₅() . n & A = F₇() . n & x = F₉() . n holds
( F₅() . (n + 1) = F₁(S,x,n) & F₇() . (n + 1) = F₂(S,A,x,n) & F₉() . (n + 1) = F₃(x,n) ) by A4;
A13: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of S ex x being set st
( S = F₅() . 0 & A = F₇() . 0 & x = F₉() . 0 & S₂[S,A,x, 0 ] ) by A1, A2;
A14: for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of S st
( S = F₅() . n & A = F₇() . n & S₂[S,A,F₉() . n,n] ) from CIRCCMB2:sch 13(A13, A12, A11, A8);

A15: now

let n be Nat; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume A16: S₃[n] ; :: thesis: S₃[n + 1]
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of S st
( S = F₄() . n & A = F₆() . n ) by A10;
then A17: F₈() . (n + 1) = F₃((F₈() . n),n) by A3;
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of S st
( S = F₅() . n & A = F₇() . n ) by A14;
hence S₃[n + 1] by A4, A16, A17; :: thesis: verum

end;

A18: S₃[ 0 ] by A2;
for i being Nat holds S₃[i] from NAT_1:sch 2(A18, A15);
then A19: for i being set st i in NAT holds
F₈() . i = F₉() . i ;
defpred S₄[ Nat] means ( F₄() . $1 = F₅() . $1 & F₆() . $1 = F₇() . $1 );
A20: F₈() = F₉() by A19, PBOOLE:3;

A21: now

let n be Nat; :: thesis: ( S₄[n] implies S₄[n + 1] )
assume A22: S₄[n] ; :: thesis: S₄[n + 1]
consider S being non empty ManySortedSign , A being non-empty MSAlgebra of S such that
A23: ( S = F₄() . n & A = F₆() . n ) by A10;
A24: F₆() . (n + 1) = F₂(S,A,(F₈() . n),n) by A3, A23
.= F₇() . (n + 1) by A4, A20, A22, A23 ;
F₄() . (n + 1) = F₁(S,(F₈() . n),n) by A3, A23
.= F₅() . (n + 1) by A4, A20, A22, A23 ;
hence S₄[n + 1] by A24; :: thesis: verum

end;

A25: S₄[ 0 ] by A2;
for i being Nat holds S₄[i] from NAT_1:sch 2(A25, A21);
then ( ( for i being set st i in NAT holds
F₄() . i = F₅() . i ) & ( for i being set st i in NAT holds
F₆() . i = F₇() . i ) ) ;
hence ( F₄() = F₅() & F₆() = F₇() & F₈() = F₉() ) by A19, PBOOLE:3; :: thesis: verum