let V be Z_Module; for I being Subset of V
for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
let I be Subset of V; for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
let l be Linear_Combination of I; for IQ being Subset of (Z_MQ_VectSp V) st V is Mult-cancelable & IQ = (MorphsZQ V) .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
let IQ be Subset of (Z_MQ_VectSp V); ( V is Mult-cancelable & IQ = (MorphsZQ V) .: I implies ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) ) )
assume AS0:
( V is Mult-cancelable & IQ = (MorphsZQ V) .: I )
; ex lq being Linear_Combination of IQ st
( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
reconsider I0 = Carrier l as finite Subset of V ;
K2:
( (MorphsZQ V) .: I0 c= IQ & (MorphsZQ V) .: I0 is finite )
by AS0, RELAT_1:123, VECTSP_6:def 4;
reconsider IQ0 = (MorphsZQ V) .: I0 as finite Subset of (Z_MQ_VectSp V) ;
defpred S1[ object , object ] means ( ( $1 in IQ0 & ex v being Element of V st
( v in I0 & $1 = (MorphsZQ V) . v & $2 = l . v ) ) or ( not $1 in IQ0 & $2 = 0. F_Rat ) );
A2:
for x being object st x in the carrier of (Z_MQ_VectSp V) holds
ex y being object st
( y in RAT & S1[x,y] )
consider lq being Function of the carrier of (Z_MQ_VectSp V),RAT such that
A5:
for x being object st x in the carrier of (Z_MQ_VectSp V) holds
S1[x,lq . x]
from FUNCT_2:sch 1(A2);
A6:
for x being Element of (Z_MQ_VectSp V) st not x in IQ0 holds
lq . x = 0. F_Rat
by A5;
lq is Element of Funcs ( the carrier of (Z_MQ_VectSp V),RAT)
by FUNCT_2:8;
then reconsider lq = lq as Linear_Combination of Z_MQ_VectSp V by A6, VECTSP_6:def 1;
A11:
Carrier lq c= IQ0
then reconsider lq = lq as Linear_Combination of IQ by K2, VECTSP_6:def 4, XBOOLE_1:1;
A12:
dom l = the carrier of V
by FUNCT_2:def 1;
A13:
dom (lq * (MorphsZQ V)) = the carrier of V
by FUNCT_2:def 1;
take
lq
; ( l = lq * (MorphsZQ V) & Carrier lq = (MorphsZQ V) .: (Carrier l) )
F1:
MorphsZQ V is one-to-one
by defMorph, AS0;
for x being object st x in dom l holds
l . x = (lq * (MorphsZQ V)) . x
hence U1:
l = lq * (MorphsZQ V)
by FUNCT_1:2, A12, A13; Carrier lq = (MorphsZQ V) .: (Carrier l)
IQ0 c= Carrier lq
hence
Carrier lq = (MorphsZQ V) .: (Carrier l)
by A11; verum