let V be free Z_Module; :: thesis: for I being Subset of V
for IQ being Subset of ()
for l being Linear_Combination of I
for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = () .: I holds
Class ((),[(Sum l),i]) in Lin IQ

let I be Subset of V; :: thesis: for IQ being Subset of ()
for l being Linear_Combination of I
for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = () .: I holds
Class ((),[(Sum l),i]) in Lin IQ

let IQ be Subset of (); :: thesis: for l being Linear_Combination of I
for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = () .: I holds
Class ((),[(Sum l),i]) in Lin IQ

let l be Linear_Combination of I; :: thesis: for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = () .: I holds
Class ((),[(Sum l),i]) in Lin IQ

let i be Element of INT.Ring; :: thesis: ( i <> 0. INT.Ring & IQ = () .: I implies Class ((),[(Sum l),i]) in Lin IQ )
assume AS: ( i <> 0. INT.Ring & IQ = () .: I ) ; :: thesis: Class ((),[(Sum l),i]) in Lin IQ
Z0: Z_MQ_VectSp V = ModuleStr(# (Class ()),(),(),() #) by defZMQVSp;
consider lq being Linear_Combination of IQ such that
P1: ( l = lq * () & Carrier lq = () .: () ) by ;
P2: Sum lq = () . (Sum l) by ;
reconsider a = 1 / i as Element of F_Rat by RAT_1:def 2;
P3: (MorphsZQ V) . (Sum l) = Class ((),[(Sum l),()]) by defMorph;
a * (() . (Sum l)) = Class ((),[(() * (Sum l)),(i * ())]) by
.= Class ((),[(Sum l),i]) by VECTSP_1:def 17 ;
hence Class ((),[(Sum l),i]) in Lin IQ by ; :: thesis: verum