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