let V be Z_Module; for I being Subset of V
for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: 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) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
let I be Subset of V; for IQ being Subset of (Z_MQ_VectSp V)
for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: 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) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
let IQ be Subset of (Z_MQ_VectSp V); for lq being Linear_Combination of IQ st V is Mult-cancelable & IQ = (MorphsZQ V) .: 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) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
let lq be Linear_Combination of IQ; ( V is Mult-cancelable & IQ = (MorphsZQ V) .: 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) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l ) )
assume AS:
( V is Mult-cancelable & IQ = (MorphsZQ V) .: I )
; 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) * (MorphsZQ V) & (MorphsZQ V) " (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) * (MorphsZQ V)) c= rng (a * lq)
by RELAT_1:26;
dom ((a * lq) * (MorphsZQ V)) = the carrier of V
by FUNCT_2:def 1;
then
(a * lq) * (MorphsZQ V) is Function of the carrier of V,INT
by P81, X3, FUNCT_2:2, XBOOLE_1:1;
then reconsider l = (a * lq) * (MorphsZQ V) 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;
R1:
{ v where v is Element of V : l . v <> 0 } c= (MorphsZQ V) " (Carrier lq)
MorphsZQ V is one-to-one
by AS, defMorph;
then
(MorphsZQ V) " (Carrier lq) = ((MorphsZQ V) ") .: (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 B2, R1, TARSKI:def 3;
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
then A9:
(MorphsZQ V) " (Carrier lq) = T
by R1;
A7:
T = Carrier l
;
AA1:
(MorphsZQ V) " (Carrier lq) c= (MorphsZQ V) " ((MorphsZQ V) .: I)
by AS, RELAT_1:143, VECTSP_6:def 4;
dom (MorphsZQ V) = the carrier of V
by FUNCT_2:def 1;
then
( MorphsZQ V is one-to-one & I c= dom (MorphsZQ V) )
by AS, defMorph;
then
T c= I
by A9, AA1, FUNCT_1:94;
then reconsider l1 = l as Linear_Combination of I by A7, VECTSP_6:def 4;
take
mm
; ex a being Element of F_Rat ex l being Linear_Combination of I st
( mm <> 0. INT.Ring & mm = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
take
a
; ex l being Linear_Combination of I st
( mm <> 0. INT.Ring & mm = a & l = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l )
take
l1
; ( mm <> 0. INT.Ring & mm = a & l1 = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l1 )
thus
( mm <> 0. INT.Ring & mm = a & l1 = (a * lq) * (MorphsZQ V) & (MorphsZQ V) " (Carrier lq) = Carrier l1 )
by A9, X3; verum