let n, k be Nat; :: thesis: ( k < n implies for x, y being FinSequence holds (k + 1),n -BitGFA0AdderOutput x,y = GFA0AdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput x,y) )
assume A1: k < n ; :: thesis: for x, y being FinSequence holds (k + 1),n -BitGFA0AdderOutput x,y = GFA0AdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput x,y)
let x, y be FinSequence; :: thesis: (k + 1),n -BitGFA0AdderOutput x,y = GFA0AdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput 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 -BitGFA0AdderOutput x,y = GFA0AdderOutput (x . (k + 1)),(y . (k + 1)),(i -BitGFA0CarryOutput x,y) ) by A2, Def4;
hence (k + 1),n -BitGFA0AdderOutput x,y = GFA0AdderOutput (x . (k + 1)),(y . (k + 1)),(k -BitGFA0CarryOutput x,y) ; :: thesis: verum