A5: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F5(S,A,x,n) is non-empty MSAlgebra over F4(S,x,n) by A3;
defpred S3[ 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 = F1() & g . 0 = F3() & h . 0 = F6() ) 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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) from 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 & S2[S,A,x,n] holds
S2[F4(S,x,n),F5(S,A,x,n),F7(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 & S2[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 & S2[S,A,h . n,n] ) from CIRCCMB2:sch 13(A9, A7, A8, A5);
defpred S4[ object , object , object , Nat] means S3[\$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 & S4[S,A,x,n] holds
S4[F4(S,x,n),F5(S,A,x,n),F7(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 & S4[S,A,x,n] holds
S4[F4(S,x,n),F5(S,A,x,n),F7(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 & S4[S,A,x,n] holds
S4[F4(S,x,n),F5(S,A,x,n),F7(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 & S4[S,A,x,n] holds
S4[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1]

let x be set ; :: thesis: ( S = f . n & A = g . n & x = h . n & S4[S,A,x,n] implies S4[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1] )
assume that
S = f . n and
A = g . n and
x = h . n and
A12: S3[S,A,n] ; :: thesis: S4[F4(S,x,n),F5(S,A,x,n),F7(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 = F4(S,x,n) as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A1;
F5(S,A,x,n) is strict gate`2=den Boolean Circuit of S1 by A4;
hence S4[F4(S,x,n),F5(S,A,x,n),F7(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 & S4[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 & S4[S,A,h . n,n] ) from then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A14: S = f . F8() and
A15: A = g . F8() and
A16: S3[S,A,F8()] ;
consider f1, h1 being
ManySortedSet of NAT such that
A17: F2() = f1 . F8() and
A18: f1 . 0 = F1() and
A19: h1 . 0 = F6() 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) = F4(S,x,n) & h1 . (n + 1) = F7(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 & S1[S,x,n] holds
S1[F4(S,x,n),F7(x,n),n + 1] ;
defpred S5[ Nat] means h1 . \$1 = h . \$1;
A22: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S1[S,x, 0 ] ) by A18;
A23: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) from
A24: now :: thesis: for n being Nat st S5[n] holds
S5[n + 1]
let n be Nat; :: thesis: ( S5[n] implies S5[n + 1] )
assume A25: S5[n] ; :: thesis: S5[n + 1]
ex S being non empty ManySortedSign st S = f1 . n by A23;
then A26: h1 . (n + 1) = F7((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 S5[n + 1] by A7, A25, A26; :: thesis: verum
end;
A27: S5[ 0 ] by ;
A28: for i being Nat holds S5[i] from defpred S6[ 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 S6[n] holds
S6[n + 1]
let n be Nat; :: thesis: ( S6[n] implies S6[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 S6[n] ; :: thesis: S6[n + 1]
then f1 . (n + 1) = F4(S,(h1 . n),n) by
.= f . (n + 1) by A7, A29, A31, A32 ;
hence S6[n + 1] ; :: thesis: verum
end;
A33: S6[ 0 ] by ;
A34: for i being Nat holds S6[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 strict gate`2=den Boolean Circuit of 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 = F6() & ( 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) = F4(S,x,n) & g . (n + 1) = F5(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 = F6() & ( 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) = F4(S,x,n) & g . (n + 1) = F5(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 = F6() & ( 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) = F4(S,x,n) & g . (n + 1) = F5(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 = F6() & ( 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) = F4(S,x,n) & g . (n + 1) = F5(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 = F6() & ( 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) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) by A6, A7, A17, A34, A15; :: thesis: verum