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