let R be Ring; :: thesis: for V being RightMod of
for v1, v2 being Vector of st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
let V be RightMod of ; :: thesis: for v1, v2 being Vector of st v1 <> v2 holds
Sum {v1,v2} = v1 + v2
let v1, v2 be Vector of ; :: thesis: ( v1 <> v2 implies Sum {v1,v2} = v1 + v2 )
assume v1 <> v2 ; :: thesis: Sum {v1,v2} = v1 + v2
then A1: <*v1,v2*> is one-to-one by FINSEQ_3:103;
( rng <*v1,v2*> = {v1,v2} & Sum <*v1,v2*> = v1 + v2 ) by FINSEQ_2:147, RLVECT_1:62;
hence Sum {v1,v2} = v1 + v2 by A1, Def3; :: thesis: verum