let f, g be nonpair-yielding FinSequence; :: thesis:
deffunc H₁( Nat) -> non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign = $1 -BitAdderStr f,g;
deffunc H₂( set , Nat) -> ManySortedSign = BitAdderWithOverflowStr (f . ($2 + 1)),(g . ($2 + 1)),$1;
deffunc H₃( Nat) -> Element of InnerVertices ($1 -BitAdderStr f,g) = $1 -BitMajorityOutput f,g;
consider h being ManySortedSet of such that
A1: for n being Element of NAT holds h . n = H₃(n) from PBOOLE:sch 5();
deffunc H₄( Nat) -> set = h . $1;
deffunc H₅( set , Nat) -> Element of InnerVertices (MajorityStr (f . ($2 + 1)),(g . ($2 + 1)),$1) = MajorityOutput (f . ($2 + 1)),(g . ($2 + 1)),$1;
set k = (0 -tuples_on BOOLEAN ) --> FALSE ;
A2: 0 -BitAdderStr f,g = 1GateCircStr <*> ,((0 -tuples_on BOOLEAN ) --> FALSE ) by Th8;
then A3: InnerVertices H₁( 0 ) is Relation by FACIRC_1:38;
A4: not InputVertices H₁( 0 ) is with_pair by A2, FACIRC_1:39;
H₄( 0 ) = 0 -BitMajorityOutput f,g by A1;
then A5: h . 0 in InnerVertices H₁( 0 ) ;
A6: for n being Nat
for x being set holds InnerVertices H₂(x,n) is Relation by FACIRC_1:88;

A7: now

let n be Nat; :: thesis:
let x be set ; :: thesis:
assume A8: x = H₄(n) ; :: thesis:
X: n in NAT by ORDINAL1:def 13;
H₄(n) = n -BitMajorityOutput f,g by A1, X;
then ( x <> [<*(f . (n + 1)),(g . (n + 1))*>,'&' ] & x <> [<*(f . (n + 1)),(g . (n + 1))*>,'xor' ] ) by A8, Th26, X;
hence InputVertices H₂(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by Th23; :: thesis:

end;

A9: for n being Nat
for x being set st x = h . n holds
not (InputVertices H₂(x,n)) \ {x} is with_pair

let n be Nat; :: thesis:
let x be set ; :: thesis:
assume A10: x = H₄(n) ; :: thesis:
A11: InputVertices H₂(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7, A10;
thus not (InputVertices H₂(x,n)) \ {x} is with_pair :: thesis:

let a be pair set ; :: according to FACIRC_1:def 2 :: thesis:
assume a in (InputVertices H₂(x,n)) \ {x} ; :: thesis:
then ( a in InputVertices H₂(x,n) & not a in {x} ) by XBOOLE_0:def 5;
then ( ( a = f . (n + 1) or a = g . (n + 1) or a = x ) & not a in {x} ) by A11, ENUMSET1:def 1;
hence contradiction by TARSKI:def 1; :: thesis:

end;

A12: now

let n be Nat; :: thesis:
let S be non empty ManySortedSign ; :: thesis:
let x be set ; :: thesis:
X: n in NAT by ORDINAL1:def 13;
assume A13: ( S = H₁(n) & x = h . n ) ; :: thesis:
then A14: ( x = n -BitMajorityOutput f,g & H₄(n + 1) = (n + 1) -BitMajorityOutput f,g ) by A1, X;
hence H₁(n + 1) = S +* H₂(x,n) by A13, Th13, X; :: thesis:
thus h . (n + 1) = H₅(x,n) by A14, Th13, X; :: thesis:
InputVertices H₂(x,n) = {(f . (n + 1)),(g . (n + 1)),x} by A7, A13;
hence x in InputVertices H₂(x,n) by ENUMSET1:def 1; :: thesis:
A15: InnerVertices H₂(x,n) = ({[<*(f . (n + 1)),(g . (n + 1))*>,'xor' ],(2GatesCircOutput (f . (n + 1)),(g . (n + 1)),x,'xor' )} \/ {[<*(f . (n + 1)),(g . (n + 1))*>,'&' ],[<*(g . (n + 1)),x*>,'&' ],[<*x,(f . (n + 1))*>,'&' ]}) \/ {(MajorityOutput (f . (n + 1)),(g . (n + 1)),x)} by Th24;
H₅(x,n) in {H₅(x,n)} by TARSKI:def 1;
hence H₅(x,n) in InnerVertices H₂(x,n) by A15, XBOOLE_0:def 3; :: thesis:

end;