let n, k be Element of NAT ; :: thesis: ( k < n implies for x, y being FinSequence holds (k + 1),n -BitAdderOutput x,y = BitAdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput x,y) )
assume A1: k < n ; :: thesis: for x, y being FinSequence holds (k + 1),n -BitAdderOutput x,y = BitAdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput x,y)
let x, y be FinSequence; :: thesis: (k + 1),n -BitAdderOutput x,y = BitAdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput 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 -BitAdderOutput x,y = BitAdderOutput (x . (k + 1)),(y . (k + 1)),(i -BitMajorityOutput x,y) ) by A2, Def6;
hence (k + 1),n -BitAdderOutput x,y = BitAdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput x,y) ; :: thesis: verum