let n, k be Element of NAT ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ((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))) ; :: thesis: verum