consider i being Nat such that
A3:
k = 1 + i
by A1, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
set o = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y)));
A4:
InnerVertices (k -BitSubtracterStr (x,y)) c= InnerVertices (n -BitSubtracterStr (x,y))
by A2, Th8;
A5:
BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) in InnerVertices (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y))))
by A3, FACIRC_1:21;
A6:
k -BitSubtracterStr (x,y) = (i -BitSubtracterStr (x,y)) +* (BitSubtracterWithBorrowStr ((x . (i + 1)),(y . (i + 1)),(i -BitBorrowOutput (x,y))))
by A3, 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 A5;
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 A6, 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 A5, A6, CIRCCOMB:15;
hence
ex b1 being Element of InnerVertices (n -BitSubtracterStr (x,y)) ex i being Element of NAT st
( k = i + 1 & b1 = BitSubtracterOutput ((x . k),(y . k),(i -BitBorrowOutput (x,y))) )
by A3, A4; verum