deffunc H₁( non empty ManySortedSign , set , set ) -> ManySortedSign = $1 +* F₄($2,$3);
consider f1, h1 being ManySortedSet of NAT such that
A3: F₂() = f1 . F₈() and
A4: f1 . 0 = F₁() and
A5: h1 . 0 = F₆() 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) = H₁(S,x,n) & h1 . (n + 1) = F₇(x,n) ) by A1;
defpred S₃[ 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 H₂( non empty ManySortedSign , non-empty MSAlgebra over $1, set , set ) -> MSAlgebra over $1 +* F₄($3,$4) = $2 +* (MSAlg (F₅($3,$4),F₄($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 H₂(S,A,x,n) is non-empty MSAlgebra over H₁(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 & S₁[S,x,n] holds
S₁[H₁(S,x,n),F₇(x,n),n + 1] ;
consider f, g, h being ManySortedSet of NAT such that
A9: ( f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₆() ) 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) = H₁(S,x,n) & g . (n + 1) = H₂(S,A,x,n) & h . (n + 1) = F₇(x,n) ) from CIRCCMB2:sch 12();
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₂[H₁(S,x,n),H₂(S,A,x,n),F₇(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 & S₂[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 & S₂[S,A,h . n,n] ) from CIRCCMB2:sch 13(A12, A10, A11, A7);
defpred S₄[ Nat] means h1 . $1 = h . $1;
A14: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S₁[S,x, 0 ] ) by A4;
A15: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S₁[S,h1 . n,n] ) from CIRCCMB2:sch 2(A14, A6, A8);

A16: 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 A17: S₄[n] ; :: thesis: S₄[n + 1]
ex S being non empty ManySortedSign st S = f1 . n by A15;
then A18: h1 . (n + 1) = F₇((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 S₄[n + 1] by A10, A17, A18; :: thesis: verum

end;

A19: S₄[ 0 ] by A9, A5;
A20: for i being Nat holds S₄[i] from NAT_1:sch 2(A19, A16);
defpred S₅[ 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 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
A23: S = f . n and
A24: A = g . n by A13;
assume S₅[n] ; :: thesis: S₅[n + 1]
then f1 . (n + 1) = S +* F₄((h1 . n),n) by A6, A23
.= f . (n + 1) by A10, A21, A23, A24 ;
hence S₅[n + 1] ; :: thesis: verum

end;

defpred S₆[ object , object , object , Nat] means S₃[$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 & S₆[S,A,x,n] holds
S₆[H₁(S,x,n),H₂(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₆[H₁(S,x,n),H₂(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₆[H₁(S,x,n),H₂(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₆[H₁(S,x,n),H₂(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₆[H₁(S,x,n),H₂(S,A,x,n),F₇(x,n),n + 1] )
assume that
A26: ( S = f . n & A = g . n ) and
x = h . n and
A27: S₃[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 = H₁(S,x,n) & A = H₂(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 = H₁(S,x,n) & A = H₂(S,A,x,n) )

reconsider A2 = F₅(x,0) as strict gate`2=den Boolean Circuit of F<sub>4</sub>(x,0) by A2;
F<sub>3</sub>() +* (MSAlg (F<sub>5</sub>(x,0),F<sub>4</sub>(x,0))) = F<sub>3</sub>() +* 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 = H₁(S,x,n) & A = H₂(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 = H₁(S,x,n) & A = H₂(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 A27, A29;
reconsider A9 = F<sub>5</sub>(x,n) as strict gate`2=den Boolean Circuit of F₄(x,n) by A2;
A +* (MSAlg (F₅(x,n),F₄(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 = H₁(S,x,n) & A = H₂(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 & S₆[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 & S₆[S,A,h . n,n] ) from CIRCCMB2:sch 13(A30, A10, A25, A7);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A31: S = f . F₈() and
A32: A = g . F₈() and
A33: S₃[S,A,F₈()] ;
A34: S₅[ 0 ] by A9, A4;
A35: for i being Nat holds S₅[i] from NAT_1:sch 2(A34, A22);
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 A9, A3, A31, A32, A33;
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 A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F₄(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) holds
( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & 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 A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F₄(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) holds
( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & 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 A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F₄(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) holds
( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & 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 A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F₄(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) holds
( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F₇(x,n) ) ) )
thus ( F₂() = f . F₈() & A = g . F₈() & f . 0 = F₁() & g . 0 = F₃() & h . 0 = F₆() ) 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 F₄(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) holds
( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F₇(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 F₄(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) holds
( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F₇(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 F₄(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) holds
( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F₇(x,n) )
let A1 be non-empty MSAlgebra over S; :: thesis: for x being set
for A2 being non-empty MSAlgebra over F₄(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) holds
( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F₇(x,n) )
let x be set ; :: thesis: for A2 being non-empty MSAlgebra over F₄(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) holds
( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F₇(x,n) )
let A2 be non-empty MSAlgebra over F₄(x,n); :: thesis: ( S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) implies ( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F₇(x,n) ) )
assume A36: ( S = f . n & A1 = g . n & x = h . n & A2 = F₅(x,n) ) ; :: thesis: ( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F₇(x,n) )
A2 = MSAlg (A2,F₄(x,n)) by Def1;
hence ( f . (n + 1) = S +* F₄(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F₇(x,n) ) by A10, A36; :: thesis: verum