let V be Z_Module; :: thesis: for I being Subset of V
for IQ being Subset of () st V is Mult-cancelable & IQ = () .: I & I is linearly-independent holds
IQ is linearly-independent

let I be Subset of V; :: thesis: for IQ being Subset of () st V is Mult-cancelable & IQ = () .: I & I is linearly-independent holds
IQ is linearly-independent

let IQ be Subset of (); :: thesis: ( V is Mult-cancelable & IQ = () .: I & I is linearly-independent implies IQ is linearly-independent )
assume AS: ( V is Mult-cancelable & IQ = () .: I & I is linearly-independent ) ; :: thesis:
assume not IQ is linearly-independent ; :: thesis: contradiction
then consider lq being Linear_Combination of IQ such that
P1: ( Sum lq = 0. () & Carrier lq <> {} ) by VECTSP_7:def 1;
consider m being Element of INT.Ring, a being Element of F_Rat, l being Linear_Combination of I such that
P2: ( m <> 0. INT.Ring & m = a & l = (a * lq) * () & () " (Carrier lq) = Carrier l ) by ;
a * (Sum lq) = 0. () by ;
then X2: (MorphsZQ V) . (Sum l) = 0. () by ;
X3: (MorphsZQ V) . (0. V) = 0. () by ;
MorphsZQ V is one-to-one by ;
then P3: Sum l = 0. V by ;
H6: Carrier lq c= IQ by VECTSP_6:def 4;
IQ c= rng () by ;
then H2: Carrier lq = () .: () by ;
Carrier l <> {} by H2, P1;
hence contradiction by AS, P3, VECTSP_7:def 1; :: thesis: verum