( 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:3;
assume i = n + 1 ; :: thesis: contradiction
hence contradiction by A1, NAT_1:13; :: thesis: verum

end;

hence for b₁ being Integer st i in Seg n & i = n + 1 holds
( b₁ = (SDSub_Add_Data (DigA x,i),k) + (SDSub_Add_Carry (DigA x,(i -' 1)),k) iff b₁ = SDSub_Add_Carry (DigA x,(i -' 1)),k ) ; :: thesis: verum