let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; for v1, v2 being Element of V st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
let v1, v2 be Element of V; ( v1 <> v2 implies Sum {v1,v2} = v1 + v2 )
assume
v1 <> v2
; Sum {v1,v2} = v1 + v2
then A1:
<*v1,v2*> is one-to-one
by FINSEQ_3:94;
( rng <*v1,v2*> = {v1,v2} & Sum <*v1,v2*> = v1 + v2 )
by FINSEQ_2:127, RLVECT_1:45;
hence
Sum {v1,v2} = v1 + v2
by A1, Def2; verum