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

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