let R be Ring; :: thesis: for V being RightMod of R
for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
let V be RightMod of R; :: thesis: for v1, v2, v3 being Vector of V st v1 <> v2 & v2 <> v3 & v1 <> v3 holds
Sum {v1,v2,v3} = (v1 + v2) + v3
let v1, v2, v3 be Vector 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, Def1; :: thesis: verum