consider i being Nat such that
A2: k = 1 + i by A1, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
set o = BitSubtracterOutput (x . k),(y . k),(i -BitBorrowOutput x,y);
A3: InnerVertices (k -BitSubtracterStr x,y) c= InnerVertices (n -BitSubtracterStr x,y) by A1, Th8;
A4: BitSubtracterOutput (x . k),(y . k),(i -BitBorrowOutput x,y) in InnerVertices (BitSubtracterWithBorrowStr (x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput x,y)) by A2, FACIRC_1:21;
A5: k -BitSubtracterStr x,y = (i -BitSubtracterStr x,y) +* (BitSubtracterWithBorrowStr (x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput x,y)) by A2, Th7;
reconsider o = BitSubtracterOutput (x . k),(y . k),(i -BitBorrowOutput x,y) as Element of (BitSubtracterWithBorrowStr (x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput x,y)) by A4;
the carrier of (BitSubtracterWithBorrowStr (x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput x,y)) \/ the carrier of (i -BitSubtracterStr x,y) = the carrier of (k -BitSubtracterStr x,y) by A5, CIRCCOMB:def 2;
then o in the carrier of (k -BitSubtracterStr x,y) by XBOOLE_0:def 3;
then o in InnerVertices (k -BitSubtracterStr x,y) by A4, A5, CIRCCOMB:19;
hence ex b₁ being Element of InnerVertices (n -BitSubtracterStr x,y) ex i being Element of NAT st
( k = i + 1 & b₁ = BitSubtracterOutput (x . k),(y . k),(i -BitBorrowOutput x,y) ) by A2, A3; :: thesis: verum