let V be Z_Module; :: thesis: for I being Subset of V
for IQ being Subset of ()
for lq being Linear_Combination of IQ
for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = () .: I & m <> 0 & m = a & l = (a * lq) * () holds
a * (Sum lq) = () . (Sum l)

let I be Subset of V; :: thesis: for IQ being Subset of ()
for lq being Linear_Combination of IQ
for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = () .: I & m <> 0 & m = a & l = (a * lq) * () holds
a * (Sum lq) = () . (Sum l)

let IQ be Subset of (); :: thesis: for lq being Linear_Combination of IQ
for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = () .: I & m <> 0 & m = a & l = (a * lq) * () holds
a * (Sum lq) = () . (Sum l)

let lq be Linear_Combination of IQ; :: thesis: for m being Integer
for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = () .: I & m <> 0 & m = a & l = (a * lq) * () holds
a * (Sum lq) = () . (Sum l)

let m be Integer; :: thesis: for a being Element of F_Rat
for l being Linear_Combination of I st V is Mult-cancelable & IQ = () .: I & m <> 0 & m = a & l = (a * lq) * () holds
a * (Sum lq) = () . (Sum l)

let a be Element of F_Rat; :: thesis: for l being Linear_Combination of I st V is Mult-cancelable & IQ = () .: I & m <> 0 & m = a & l = (a * lq) * () holds
a * (Sum lq) = () . (Sum l)

let l be Linear_Combination of I; :: thesis: ( V is Mult-cancelable & IQ = () .: I & m <> 0 & m = a & l = (a * lq) * () implies a * (Sum lq) = () . (Sum l) )
assume AS: ( V is Mult-cancelable & IQ = () .: I & m <> 0 & m = a & l = (a * lq) * () ) ; :: thesis: a * (Sum lq) = () . (Sum l)
reconsider lqa = a * lq as Linear_Combination of IQ by VECTSP_6:31;
thus a * (Sum lq) = Sum lqa by VECTSP_6:45
.= () . (Sum l) by ; :: thesis: verum