( i in Seg n implies not i = n + 1 )
_{1} being Integer st i in Seg n & i = n + 1 holds

( b_{1} = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) iff b_{1} = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) )
; :: thesis: verum

proof

hence
for b
assume
i in Seg n
; :: thesis: not i = n + 1

then A1: i <= n by FINSEQ_1:1;

assume i = n + 1 ; :: thesis: contradiction

hence contradiction by A1, NAT_1:13; :: thesis: verum

end;then A1: i <= n by FINSEQ_1:1;

assume i = n + 1 ; :: thesis: contradiction

hence contradiction by A1, NAT_1:13; :: thesis: verum

( b