( i in Seg n implies not i = n + 1 )
proof
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;
hence for b1 being Integer st i in Seg n & i = n + 1 holds
( b1 = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) iff b1 = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) ) ; :: thesis: verum