deffunc H1( non empty ManySortedSign , set , set ) -> ManySortedSign = \$1 +* F4(\$2,\$3);
consider f1, h1 being ManySortedSet of NAT such that
A3: F2() = f1 . F8() and
A4: f1 . 0 = F1() and
A5: h1 . 0 = F6() and
A6: 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) = H1(S,x,n) & h1 . (n + 1) = F7(x,n) ) by A1;
defpred S3[ object , object , Nat] means ( \$3 <> 0 implies 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 ) );
deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over \$1, set , set ) -> MSAlgebra over \$1 +* F4(\$3,\$4) = \$2 +* (MSAlg (F5(\$3,\$4),F4(\$3,\$4)));
A7: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds H2(S,A,x,n) is non-empty MSAlgebra over H1(S,x,n) ;
A8: 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[H1(S,x,n),F7(x,n),n + 1] ;
consider f, g, h being ManySortedSet of NAT such that
A9: ( f . 0 = F1() & g . 0 = F3() & h . 0 = F6() ) and
A10: 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) = H1(S,x,n) & g . (n + 1) = H2(S,A,x,n) & h . (n + 1) = F7(x,n) ) from 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 & S2[S,A,x,n] holds
S2[H1(S,x,n),H2(S,A,x,n),F7(x,n),n + 1] ;
A12: 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 A9;
A13: 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 defpred S4[ Nat] means h1 . \$1 = h . \$1;
A14: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S1[S,x, 0 ] ) by A4;
A15: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) from
A16: 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 A17: S4[n] ; :: thesis: S4[n + 1]
ex S being non empty ManySortedSign st S = f1 . n by A15;
then A18: h1 . (n + 1) = F7((h1 . n),n) by A6;
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n ) by A13;
hence S4[n + 1] by ; :: thesis: verum
end;
A19: S4[ 0 ] by A9, A5;
A20: for i being Nat holds S4[i] from defpred S5[ Nat] means f1 . \$1 = f . \$1;
for i being object st i in NAT holds
h1 . i = h . i by A20;
then A21: h1 = h by PBOOLE:3;
A22: now :: thesis: for n being Nat st S5[n] holds
S5[n + 1]
let n be Nat; :: thesis: ( S5[n] implies S5[n + 1] )
consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A23: S = f . n and
A24: A = g . n by A13;
assume S5[n] ; :: thesis: S5[n + 1]
then f1 . (n + 1) = S +* F4((h1 . n),n) by
.= f . (n + 1) by A10, A21, A23, A24 ;
hence S5[n + 1] ; :: thesis: verum
end;
defpred S6[ object , object , object , Nat] means S3[\$1,\$2,\$4];
A25: 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 & S6[S,A,x,n] holds
S6[H1(S,x,n),H2(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 & S6[S,A,x,n] holds
S6[H1(S,x,n),H2(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 & S6[S,A,x,n] holds
S6[H1(S,x,n),H2(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 & S6[S,A,x,n] holds
S6[H1(S,x,n),H2(S,A,x,n),F7(x,n),n + 1]

let x be set ; :: thesis: ( S = f . n & A = g . n & x = h . n & S6[S,A,x,n] implies S6[H1(S,x,n),H2(S,A,x,n),F7(x,n),n + 1] )
assume that
A26: ( S = f . n & A = g . n ) and
x = h . n and
A27: S3[S,A,n] and
n + 1 <> 0 ; :: thesis: 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 = H1(S,x,n) & A = H2(S,A,x,n) )

per cases ( n = 0 or n <> 0 ) ;
suppose A28: n = 0 ; :: thesis: 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 = H1(S,x,n) & A = H2(S,A,x,n) )

reconsider A2 = F5(x,0) as strict gate`2=den Boolean Circuit of F4(x,0) by A2;
F3() +* (MSAlg (F5(x,0),F4(x,0))) = F3() +* A2 by Def1;
hence 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 = H1(S,x,n) & A = H2(S,A,x,n) ) by A9, A26, A28; :: thesis: verum
end;
suppose A29: n <> 0 ; :: thesis: 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 = H1(S,x,n) & A = H2(S,A,x,n) )

then reconsider S = S as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A27;
reconsider A = A as strict gate`2=den Boolean Circuit of S by ;
reconsider A9 = F5(x,n) as strict gate`2=den Boolean Circuit of F4(x,n) by A2;
A +* (MSAlg (F5(x,n),F4(x,n))) = A +* A9 by Def1;
hence 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 = H1(S,x,n) & A = H2(S,A,x,n) ) ; :: thesis: verum
end;
end;
end;
A30: 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 & S6[S,A,x, 0 ] ) by 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 & S6[S,A,h . n,n] ) from then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A31: S = f . F8() and
A32: A = g . F8() and
A33: S3[S,A,F8()] ;
A34: S5[ 0 ] by A9, A4;
A35: for i being Nat holds S5[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 A9, A3, A31, A32, A33;
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 A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & 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 A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & 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 A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & 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 A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) ) )

thus ( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() ) by A9, A3, A35, A32; :: thesis: for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )

let n be Nat; :: thesis: for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )

let S be non empty ManySortedSign ; :: thesis: for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )

let A1 be non-empty MSAlgebra over S; :: thesis: for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )

let x be set ; :: thesis: for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )

let A2 be non-empty MSAlgebra over F4(x,n); :: thesis: ( S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) implies ( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) )
assume A36: ( S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) ) ; :: thesis: ( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )
A2 = MSAlg (A2,F4(x,n)) by Def1;
hence ( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) by ; :: thesis: verum