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

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 st S = f1 . n by A10;
then A17: h1 . (n + 1) = F₇((h1 . n),n) by A6;
ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of S st
( S = f . n & A = g . n ) by A14;
hence S₃[n + 1] by A4, A16, A17; :: thesis: verum

end;

X: for i being Nat holds S₃[i] from NAT_1:sch 2(A7, A15);
for i being set st i in NAT holds
h1 . i = h . i by X;
then A18: h1 = h by PBOOLE:3;
defpred S₄[ Nat] means f1 . $1 = f . $1;
A19: S₄[ 0 ] by A3, A5;

A20: now

let n be Nat; :: thesis: ( S₄[n] implies S₄[n + 1] )
assume A21: S₄[n] ; :: thesis: S₄[n + 1]
consider S being non empty ManySortedSign , A being non-empty MSAlgebra of S such that
A22: ( S = f . n & A = g . n ) by A14;
f1 . (n + 1) = S +* F₄((h1 . n),n) by A6, A21, A22
.= f . (n + 1) by A4, A18, A22 ;
hence S₄[n + 1] ; :: thesis: verum

end;

A23: for i being Nat holds S₄[i] from NAT_1:sch 2(A19, A20);
for i being set st i in NAT holds
f1 . i = f . i by A23;
then A24: f1 = f by PBOOLE:3;
defpred S₅[ set , set , 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 ) );
defpred S₆[ set , set , set , Nat] means S₅[$1,$2,$4];
A25: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of S ex x being set st
( S = f . 0 & A = g . 0 & x = h . 0 & S₆[S,A,x, 0 ] ) by A3;
A26: 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 = 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 of 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 of 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 of 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 A27: ( S = f . n & A = g . n & x = h . n & S₅[S,A,n] & 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 A3, A27, 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 A' = 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 +* A' 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;

for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra of S st
( S = f . n & A = g . n & S₆[S,A,h . n,n] ) from CIRCCMB2:sch 13(A25, A4, A26, A13);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra of S such that
A30: ( S = f . F₈() & A = g . F₈() & S₅[S,A,F₈()] ) ;
reconsider A = A as strict gate`2=den Boolean Circuit of F₂() by A3, A5, A24, A30;
take A ; :: thesis: ex f, g, h being ManySortedSet of 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 of S
for x being set
for A2 being non-empty MSAlgebra of 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 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 of S
for x being set
for A2 being non-empty MSAlgebra of 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 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 of S
for x being set
for A2 being non-empty MSAlgebra of 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 of S
for x being set
for A2 being non-empty MSAlgebra of 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 A3, A5, A23, A30; :: thesis: for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra of S
for x being set
for A2 being non-empty MSAlgebra of 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 of S
for x being set
for A2 being non-empty MSAlgebra of 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 of S
for x being set
for A2 being non-empty MSAlgebra of 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 of S; :: thesis: for x being set
for A2 being non-empty MSAlgebra of 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 of 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 of 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 A31: ( 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 A4, A31; :: thesis: verum