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:95;
( rng <*v1,v2,v3*> = {v1,v2,v3} & Sum <*v1,v2,v3*> = (v1 + v2) + v3 ) by FINSEQ_2:128, RLVECT_1:46;
hence Sum {v1,v2,v3} = (v1 + v2) + v3 by A1, Def2; :: thesis: verum