let R be Ring; :: thesis: for V being LeftMod of R
for A being finite Subset of V
for l, l0 being Linear_Combination of V st l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 holds
Sum (l * ()) = Sum (l0 * ())

let V be LeftMod of R; :: thesis: for A being finite Subset of V
for l, l0 being Linear_Combination of V st l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 holds
Sum (l * ()) = Sum (l0 * ())

let A be finite Subset of V; :: thesis: for l, l0 being Linear_Combination of V st l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 holds
Sum (l * ()) = Sum (l0 * ())

let l, l0 be Linear_Combination of V; :: thesis: ( l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 implies Sum (l * ()) = Sum (l0 * ()) )
assume A1: ( l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 ) ; :: thesis: Sum (l * ()) = Sum (l0 * ())
dom l0 = the carrier of V by FUNCT_2:def 1;
then dom (l0 | (Carrier l0)) = Carrier l0 by RELAT_1:62;
then A2: rng () c= dom (l0 | (Carrier l0)) by A1;
then l * () = (l0 | (Carrier l0)) * () by ;
hence Sum (l * ()) = Sum (l0 * ()) by ; :: thesis: verum