A5: 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 A3;
defpred S₃[ object , object , Nat] means ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st
( S = $1 & A = $2 );
consider f, g, h being ManySortedSet of NAT such that
A6: ( f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₆() ) and
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 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();
A8: 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] ;
A9: 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 A6;
A10: 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(A9, A7, A8, A5);
defpred S₄[ object , object , object , Nat] means S₃[$1,$2,$4];
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 . 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]

proof

let n be Nat; :: thesis: 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]
let S be non empty ManySortedSign ; :: thesis: 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]
let A be non-empty MSAlgebra over S; :: thesis: 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]
let x be set ; :: thesis: ( S = f . n & A = g . n & x = h . n & S₄[S,A,x,n] implies S₄[F₄(S,x,n),F₅(S,A,x,n),F₇(x,n),n + 1] )
assume that
S = f . n and
A = g . n and
x = h . n and
A12: S₃[S,A,n] ; :: thesis: S₄[F₄(S,x,n),F₅(S,A,x,n),F₇(x,n),n + 1]
reconsider S = S as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A12;
reconsider A = A as strict gate`2=den Boolean Circuit of S by A12;
reconsider S1 = F<sub>4</sub>(S,x,n) as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A1;
F<sub>5</sub>(S,A,x,n) is strict gate`2=den Boolean Circuit of S1 by A4;
hence S₄[F₄(S,x,n),F₅(S,A,x,n),F₇(x,n),n + 1] ; :: thesis: verum

end;

A13: 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 A6;
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(A13, A7, A11, A5);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A14: S = f . F₈() and
A15: A = g . F₈() and
A16: S₃[S,A,F₈()] ;
consider f1, h1 being ManySortedSet of NAT such that
A17: F₂() = f1 . F₈() and
A18: f1 . 0 = F₁() and
A19: h1 . 0 = F₆() and
A20: 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 A2;
A21: 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;
A22: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S₁[S,x, 0 ] ) by A18;
A23: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S₁[S,h1 . n,n] ) from CIRCCMB2:sch 2(A22, A20, A21);

A24: 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 A25: S₅[n] ; :: thesis: S₅[n + 1]
ex S being non empty ManySortedSign st S = f1 . n by A23;
then A26: h1 . (n + 1) = F₇((h1 . n),n) by A20;
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n ) by A10;
hence S₅[n + 1] by A7, A25, A26; :: thesis: verum

end;

A27: S₅[ 0 ] by A6, A19;
A28: for i being Nat holds S₅[i] from NAT_1:sch 2(A27, A24);
defpred S₆[ Nat] means f1 . $1 = f . $1;
for i being object st i in NAT holds
h1 . i = h . i by A28;
then A29: h1 = h by PBOOLE:3;

A30: 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
A31: S = f . n and
A32: A = g . n by A10;
assume S₆[n] ; :: thesis: S₆[n + 1]
then f1 . (n + 1) = F₄(S,(h1 . n),n) by A20, A31
.= f . (n + 1) by A7, A29, A31, A32 ;
hence S₆[n + 1] ; :: thesis: verum

end;

A33: S₆[ 0 ] by A6, A18;
A34: for i being Nat holds S₆[i] from NAT_1:sch 2(A33, A30);
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 strict gate`2=den Boolean Circuit of F₂() by A17, A14, A16;
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 A6, A7, A17, A34, A15; :: thesis: verum