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

for IQ being Subset of (Z_MQ_VectSp V)

for l being Linear_Combination of I

for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(Sum l),i]) in Lin IQ

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

for l being Linear_Combination of I

for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(Sum l),i]) in Lin IQ

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

for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(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 = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(Sum l),i]) in Lin IQ

let i be Element of INT.Ring; :: thesis: ( i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I implies Class ((EQRZM V),[(Sum l),i]) in Lin IQ )

assume AS: ( i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I ) ; :: thesis: Class ((EQRZM V),[(Sum l),i]) in Lin IQ

Z0: Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) by defZMQVSp;

consider lq being Linear_Combination of IQ such that

P1: ( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) ) by ThEQRZMV4, AS;

P2: Sum lq = (MorphsZQ V) . (Sum l) by AS, P1, XThSum1;

reconsider a = 1 / i as Element of F_Rat by RAT_1:def 2;

P3: (MorphsZQ V) . (Sum l) = Class ((EQRZM V),[(Sum l),(1. INT.Ring)]) by defMorph;

a * ((MorphsZQ V) . (Sum l)) = Class ((EQRZM V),[((1. INT.Ring) * (Sum l)),(i * (1. INT.Ring))]) by AS, P3, Z0, DeflmultCoset

.= Class ((EQRZM V),[(Sum l),i]) by VECTSP_1:def 17 ;

hence Class ((EQRZM V),[(Sum l),i]) in Lin IQ by P2, VECTSP_4:21, VECTSP_7:7; :: thesis: verum

for IQ being Subset of (Z_MQ_VectSp V)

for l being Linear_Combination of I

for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(Sum l),i]) in Lin IQ

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

for l being Linear_Combination of I

for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(Sum l),i]) in Lin IQ

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

for i being Element of INT.Ring st i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(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 = (MorphsZQ V) .: I holds

Class ((EQRZM V),[(Sum l),i]) in Lin IQ

let i be Element of INT.Ring; :: thesis: ( i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I implies Class ((EQRZM V),[(Sum l),i]) in Lin IQ )

assume AS: ( i <> 0. INT.Ring & IQ = (MorphsZQ V) .: I ) ; :: thesis: Class ((EQRZM V),[(Sum l),i]) in Lin IQ

Z0: Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) by defZMQVSp;

consider lq being Linear_Combination of IQ such that

P1: ( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) ) by ThEQRZMV4, AS;

P2: Sum lq = (MorphsZQ V) . (Sum l) by AS, P1, XThSum1;

reconsider a = 1 / i as Element of F_Rat by RAT_1:def 2;

P3: (MorphsZQ V) . (Sum l) = Class ((EQRZM V),[(Sum l),(1. INT.Ring)]) by defMorph;

a * ((MorphsZQ V) . (Sum l)) = Class ((EQRZM V),[((1. INT.Ring) * (Sum l)),(i * (1. INT.Ring))]) by AS, P3, Z0, DeflmultCoset

.= Class ((EQRZM V),[(Sum l),i]) by VECTSP_1:def 17 ;

hence Class ((EQRZM V),[(Sum l),i]) in Lin IQ by P2, VECTSP_4:21, VECTSP_7:7; :: thesis: verum