let n, k be Nat; :: thesis: ( k < n implies for x, y being FinSequence holds ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y))) )
assume A1: k < n ; :: thesis: for x, y being FinSequence holds ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y)))
let x, y be FinSequence; :: thesis: ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y)))
A2: k + 1 >= 1 by NAT_1:11;
k + 1 <= n by A1, NAT_1:13;
then ex i being Nat st
( k + 1 = i + 1 & ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(i -BitGFA1CarryOutput (x,y))) ) by A2, Def8;
hence ((k + 1),n) -BitGFA1AdderOutput (x,y) = GFA1AdderOutput ((x . (k + 1)),(y . (k + 1)),(k -BitGFA1CarryOutput (x,y))) ; :: thesis: verum