consider i being Nat such that
A3: k = 1 + i by A1, NAT_1:10;
reconsider n9 = n, k9 = k, i = i as Element of NAT by ORDINAL1:def 13;
set o = BitAdderOutput (x . k),(y . k),(i -BitMajorityOutput x,y);
A4: InnerVertices (k9 -BitAdderStr x,y) c= InnerVertices (n9 -BitAdderStr x,y) by A2, Th14;
A5: BitAdderOutput (x . k),(y . k),(i -BitMajorityOutput x,y) in InnerVertices (BitAdderWithOverflowStr (x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput x,y)) by A3, FACIRC_1:90;
A6: k -BitAdderStr x,y = (i -BitAdderStr x,y) +* (BitAdderWithOverflowStr (x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput x,y)) by A3, Th13;
reconsider o = BitAdderOutput (x . k),(y . k),(i -BitMajorityOutput x,y) as Element of (BitAdderWithOverflowStr (x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput x,y)) by A5;
the carrier of (BitAdderWithOverflowStr (x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput x,y)) \/ the carrier of (i -BitAdderStr x,y) = the carrier of (k -BitAdderStr x,y) by A6, CIRCCOMB:def 2;
then o in the carrier of (k -BitAdderStr x,y) by XBOOLE_0:def 3;
then o in InnerVertices (k -BitAdderStr x,y) by A5, A6, CIRCCOMB:19;
hence ex b₁ being Element of InnerVertices (n -BitAdderStr x,y) ex i being Element of NAT st
( k = i + 1 & b₁ = BitAdderOutput (x . k),(y . k),(i -BitMajorityOutput x,y) ) by A3, A4; :: thesis: verum