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

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

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

let lq be Linear_Combination of IQ; :: thesis: ( V is Mult-cancelable & IQ = () .: I implies ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * () & () " (Carrier lq) = Carrier l ) )

assume AS: ( V is Mult-cancelable & IQ = () .: I ) ; :: thesis: ex m being Element of INT.Ring ex a being Element of F_Rat ex l being Linear_Combination of I st
( m <> 0. INT.Ring & m = a & l = (a * lq) * () & () " (Carrier lq) = Carrier l )

consider m being Integer, a being Element of F_Rat such that
X3: ( m <> 0 & m = a & rng (a * lq) c= INT ) by ThEQRZMV3A;
reconsider mm = m as Element of INT.Ring by INT_1:def 2;
P81: rng ((a * lq) * ()) c= rng (a * lq) by RELAT_1:26;
dom ((a * lq) * ()) = the carrier of V by FUNCT_2:def 1;
then (a * lq) * () is Function of the carrier of V,INT by ;
then reconsider l = (a * lq) * () as Element of Funcs ( the carrier of V,INT) by FUNCT_2:8;
set T = { v where v is Element of V : l . v <> 0 } ;
set F = MorphsZQ V;
B2: now :: thesis: for v being object st v in { v where v is Element of V : l . v <> 0 } holds
v in the carrier of V
let v be object ; :: thesis: ( v in { v where v is Element of V : l . v <> 0 } implies v in the carrier of V )
assume v in { v where v is Element of V : l . v <> 0 } ; :: thesis: v in the carrier of V
then ex v1 being Element of V st
( v1 = v & l . v1 <> 0 ) ;
hence v in the carrier of V ; :: thesis: verum
end;
R1: { v where v is Element of V : l . v <> 0 } c= () " (Carrier lq)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of V : l . v <> 0 } or x in () " (Carrier lq) )
assume x in { v where v is Element of V : l . v <> 0 } ; :: thesis: x in () " (Carrier lq)
then consider v being Element of V such that
R11: ( x = v & l . v <> 0 ) ;
RRR: dom () = the carrier of V by FUNCT_2:def 1;
V1: l . v = (a * lq) . (() . v) by
.= a * (lq . (() . v)) by VECTSP_6:def 9 ;
lq . (() . v) <> 0. F_Rat by ;
then (MorphsZQ V) . v in Carrier lq ;
hence x in () " (Carrier lq) by ; :: thesis: verum
end;
MorphsZQ V is one-to-one by ;
then (MorphsZQ V) " (Carrier lq) = (() ") .: (Carrier lq) by FUNCT_1:85;
then reconsider T = { v where v is Element of V : l . v <> 0 } as finite Subset of V by ;
for v being Element of V st not v in T holds
l . v = 0. INT.Ring ;
then reconsider l = l as Linear_Combination of V by VECTSP_6:def 1;
(MorphsZQ V) " (Carrier lq) c= T
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in () " (Carrier lq) or x in T )
assume S21: x in () " (Carrier lq) ; :: thesis: x in T
then ( x in the carrier of V & () . x in Carrier lq ) by FUNCT_2:38;
then consider w being Element of () such that
R11: ( (MorphsZQ V) . x = w & lq . w <> 0. F_Rat ) ;
reconsider v = x as Element of V by S21;
RRR: dom () = the carrier of V by FUNCT_2:def 1;
RR1: l . v = (a * lq) . (() . v) by
.= a * (lq . w) by ;
reconsider a1 = a, d1 = lq . w as Rational ;
l . v <> 0
proof
assume l . v = 0 ; :: thesis: contradiction
then a1 * d1 = 0 by RR1;
hence contradiction by R11, X3; :: thesis: verum
end;
hence x in T ; :: thesis: verum
end;
then A9: (MorphsZQ V) " (Carrier lq) = T by R1;
A7: T = Carrier l ;
AA1: (MorphsZQ V) " (Carrier lq) c= () " (() .: I) by ;
dom () = the carrier of V by FUNCT_2:def 1;
then ( MorphsZQ V is one-to-one & I c= dom () ) by ;
then T c= I by ;
then reconsider l1 = l as Linear_Combination of I by ;
take mm ; :: thesis: ex a being Element of F_Rat ex l being Linear_Combination of I st
( mm <> 0. INT.Ring & mm = a & l = (a * lq) * () & () " (Carrier lq) = Carrier l )

take a ; :: thesis: ex l being Linear_Combination of I st
( mm <> 0. INT.Ring & mm = a & l = (a * lq) * () & () " (Carrier lq) = Carrier l )

take l1 ; :: thesis: ( mm <> 0. INT.Ring & mm = a & l1 = (a * lq) * () & () " (Carrier lq) = Carrier l1 )
thus ( mm <> 0. INT.Ring & mm = a & l1 = (a * lq) * () & () " (Carrier lq) = Carrier l1 ) by A9, X3; :: thesis: verum