let V be Z_Module; :: thesis: for I being Subset of V

for IQ being Subset of (Z_MQ_VectSp V)

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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (Sum l)

let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp V)

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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (Sum l)

let IQ be Subset of (Z_MQ_VectSp V); :: 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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (Sum l)

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

a * (Sum lq) = (MorphsZQ V) . (Sum l)

let l be Linear_Combination of I; :: thesis: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) implies a * (Sum lq) = (MorphsZQ V) . (Sum l) )

assume AS: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) ) ; :: thesis: a * (Sum lq) = (MorphsZQ V) . (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

.= (MorphsZQ V) . (Sum l) by AS, XThSum1 ; :: thesis: verum

for IQ being Subset of (Z_MQ_VectSp V)

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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (Sum l)

let I be Subset of V; :: thesis: for IQ being Subset of (Z_MQ_VectSp V)

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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (Sum l)

let IQ be Subset of (Z_MQ_VectSp V); :: 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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (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 = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) holds

a * (Sum lq) = (MorphsZQ V) . (Sum l)

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

a * (Sum lq) = (MorphsZQ V) . (Sum l)

let l be Linear_Combination of I; :: thesis: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) implies a * (Sum lq) = (MorphsZQ V) . (Sum l) )

assume AS: ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I & m <> 0 & m = a & l = (a * lq) * (MorphsZQ V) ) ; :: thesis: a * (Sum lq) = (MorphsZQ V) . (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

.= (MorphsZQ V) . (Sum l) by AS, XThSum1 ; :: thesis: verum