theorem :: FACIRC_2:15

for n, k being Element of NAT st k < n holds
for x, y being FinSequence holds ((k + 1),n) -BitAdderOutput (x,y) = BitAdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitMajorityOutput (x,y)))