consider i being Nat such that
A1: k = 1 + i by X1, NAT_1:10;
reconsider n9 = n, k9 = k, i = i as Element of NAT by ORDINAL1:def 12;
set o = BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y)));
A2: InnerVertices (k9 -BitAdderStr (x,y)) c= InnerVertices (n9 -BitAdderStr (x,y)) by X2, Th13;
A3: BitAdderOutput ((x . k),(y . k),(i -BitMajorityOutput (x,y))) in InnerVertices (BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y)))) by A1, FACIRC_1:90;
A4: k -BitAdderStr (x,y) = (i -BitAdderStr (x,y)) +* (BitAdderWithOverflowStr ((x . (i + 1)),(y . (i + 1)),(i -BitMajorityOutput (x,y)))) by A1, Th12;
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 A3;
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 A4, 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 A3, A4, CIRCCOMB:15;
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 A1, A2; :: thesis: verum