theorem :: GFACIRC2:24

for n, k being Nat st k < n holds
for x, y being FinSequence holds ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y)))