theorem :: GFACIRC2:10

for n, k being Nat st k < n holds
for x, y being FinSequence holds ((k + 1),n) -BitGFA0AdderOutput (x,y) = GFA0AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput (x,y)))