let n, k be Element of NAT ; ( k < n implies for x, y being FinSequence holds ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (x,y))) )
assume A1:
k < n
; for x, y being FinSequence holds ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (x,y)))
let x, y be FinSequence; ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (x,y)))
A2:
k + 1 >= 1
by NAT_1:11;
k + 1 <= n
by A1, NAT_1:13;
then
ex i being Element of NAT st
( k + 1 = i + 1 & ((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(i -BitBorrowOutput (x,y))) )
by A2, Def4;
hence
((k + 1),n) -BitSubtracterOutput (x,y) = BitSubtracterOutput ((x . (k + 1)),(y . (k + 1)),(k -BitBorrowOutput (x,y)))
; verum