let V be Z_Module; :: thesis: for I being Subset of V
for l being Linear_Combination of I
for IQ being Subset of () st V is Mult-cancelable & IQ = () .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * () & Carrier lq = () .: () )

let I be Subset of V; :: thesis: for l being Linear_Combination of I
for IQ being Subset of () st V is Mult-cancelable & IQ = () .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * () & Carrier lq = () .: () )

let l be Linear_Combination of I; :: thesis: for IQ being Subset of () st V is Mult-cancelable & IQ = () .: I holds
ex lq being Linear_Combination of IQ st
( l = lq * () & Carrier lq = () .: () )

let IQ be Subset of (); :: thesis: ( V is Mult-cancelable & IQ = () .: I implies ex lq being Linear_Combination of IQ st
( l = lq * () & Carrier lq = () .: () ) )

assume AS0: ( V is Mult-cancelable & IQ = () .: I ) ; :: thesis: ex lq being Linear_Combination of IQ st
( l = lq * () & Carrier lq = () .: () )

reconsider I0 = Carrier l as finite Subset of V ;
K2: ( (MorphsZQ V) .: I0 c= IQ & () .: I0 is finite ) by ;
reconsider IQ0 = () .: I0 as finite Subset of () ;
defpred S1[ object , object ] means ( ( \$1 in IQ0 & ex v being Element of V st
( v in I0 & \$1 = () . v & \$2 = l . v ) ) or ( not \$1 in IQ0 & \$2 = 0. F_Rat ) );
A2: for x being object st x in the carrier of () holds
ex y being object st
( y in RAT & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of () implies ex y being object st
( y in RAT & S1[x,y] ) )

assume x in the carrier of () ; :: thesis: ex y being object st
( y in RAT & S1[x,y] )

then reconsider x = x as Element of () ;
per cases ( x in IQ0 or not x in IQ0 ) ;
suppose A3: x in IQ0 ; :: thesis: ex y being object st
( y in RAT & S1[x,y] )

then consider v being object such that
A4: ( v in the carrier of V & v in I0 & x = () . v ) by FUNCT_2:64;
reconsider v = v as Element of V by A4;
l . v in RAT by ;
hence ex y being object st
( y in RAT & S1[x,y] ) by A3, A4; :: thesis: verum
end;
suppose not x in IQ0 ; :: thesis: ex y being object st
( y in RAT & S1[x,y] )

hence ex y being object st
( y in RAT & S1[x,y] ) ; :: thesis: verum
end;
end;
end;
consider lq being Function of the carrier of (),RAT such that
A5: for x being object st x in the carrier of () holds
S1[x,lq . x] from A6: for x being Element of () st not x in IQ0 holds
lq . x = 0. F_Rat by A5;
lq is Element of Funcs ( the carrier of (),RAT) by FUNCT_2:8;
then reconsider lq = lq as Linear_Combination of Z_MQ_VectSp V by ;
A11: Carrier lq c= IQ0
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier lq or x in IQ0 )
assume that
A7: x in Carrier lq and
A8: not x in IQ0 ; :: thesis: contradiction
consider z being Element of () such that
A9: x = z and
A10: lq . z <> 0. F_Rat by A7;
thus contradiction by A5, A8, A9, A10; :: thesis: verum
end;
then reconsider lq = lq as Linear_Combination of IQ by ;
A12: dom l = the carrier of V by FUNCT_2:def 1;
A13: dom (lq * ()) = the carrier of V by FUNCT_2:def 1;
take lq ; :: thesis: ( l = lq * () & Carrier lq = () .: () )
F1: MorphsZQ V is one-to-one by ;
for x being object st x in dom l holds
l . x = (lq * ()) . x
proof
let x be object ; :: thesis: ( x in dom l implies l . x = (lq * ()) . x )
assume x in dom l ; :: thesis: l . x = (lq * ()) . x
then reconsider v = x as Element of V ;
reconsider w = () . v as Element of () ;
per cases ( v in I0 or not v in I0 ) ;
suppose v in I0 ; :: thesis: l . x = (lq * ()) . x
then w in IQ0 by FUNCT_2:35;
then consider v0 being Element of V such that
A16: ( v0 in I0 & w = () . v0 & lq . w = l . v0 ) by A5;
v0 = v by ;
hence l . x = (lq * ()) . x by ; :: thesis: verum
end;
suppose A18: not v in I0 ; :: thesis: l . x = (lq * ()) . x
then A19: l . v = 0. F_Rat ;
not w in IQ0
proof
assume w in IQ0 ; :: thesis: contradiction
then consider v0 being Element of V such that
A16: ( v0 in I0 & w = () . v0 & lq . w = l . v0 ) by A5;
thus contradiction by A16, A18, F1, FUNCT_2:19; :: thesis: verum
end;
then lq . w = 0. F_Rat by A5;
hence l . x = (lq * ()) . x by ; :: thesis: verum
end;
end;
end;
hence U1: l = lq * () by ; :: thesis: Carrier lq = () .: ()
IQ0 c= Carrier lq
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in IQ0 or x in Carrier lq )
assume x in IQ0 ; :: thesis: x in Carrier lq
then consider v being object such that
A4: ( v in the carrier of V & v in I0 & x = () . v ) by FUNCT_2:64;
reconsider v = v as Element of V by A4;
x = () . v by A4;
then reconsider y = x as Element of () ;
X1: lq . y = l . v by ;
l . v <> 0 by ;
hence x in Carrier lq by X1; :: thesis: verum
end;
hence Carrier lq = () .: () by A11; :: thesis: verum