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 * (canFS A)) = Sum (l0 * (canFS A))
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 * (canFS A)) = Sum (l0 * (canFS A))
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 * (canFS A)) = Sum (l0 * (canFS A))
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 * (canFS A)) = Sum (l0 * (canFS A)) )
assume A1: ( l | (Carrier l0) = l0 | (Carrier l0) & Carrier l0 c= Carrier l & A c= Carrier l0 ) ; :: thesis: Sum (l * (canFS A)) = Sum (l0 * (canFS A))
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 (canFS A) c= dom (l0 | (Carrier l0)) by A1;
then l * (canFS A) = (l0 | (Carrier l0)) * (canFS A) by A1, RELAT_1:165;
hence Sum (l * (canFS A)) = Sum (l0 * (canFS A)) by A2, RELAT_1:165; :: thesis: verum