let V be Z_Module; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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 S_{1}[ 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 & S_{1}[x,y] )

A5: for x being object st x in the carrier of (Z_MQ_VectSp V) holds

S_{1}[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

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 ; :: thesis: ( 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

IQ0 c= Carrier lq

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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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 S

( 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 & S

proof

consider lq being Function of the carrier of (Z_MQ_VectSp V),RAT such that
let x be object ; :: thesis: ( x in the carrier of (Z_MQ_VectSp V) implies ex y being object st

( y in RAT & S_{1}[x,y] ) )

assume x in the carrier of (Z_MQ_VectSp V) ; :: thesis: ex y being object st

( y in RAT & S_{1}[x,y] )

then reconsider x = x as Element of (Z_MQ_VectSp V) ;

end;( y in RAT & S

assume x in the carrier of (Z_MQ_VectSp V) ; :: thesis: ex y being object st

( y in RAT & S

then reconsider x = x as Element of (Z_MQ_VectSp V) ;

per cases
( x in IQ0 or not x in IQ0 )
;

end;

suppose A3:
x in IQ0
; :: thesis: ex y being object st

( y in RAT & S_{1}[x,y] )

( y in RAT & S

then consider v being object such that

A4: ( v in the carrier of V & v in I0 & x = (MorphsZQ V) . v ) by FUNCT_2:64;

reconsider v = v as Element of V by A4;

l . v in RAT by NUMBERS:14, TARSKI:def 3;

hence ex y being object st

( y in RAT & S_{1}[x,y] )
by A3, A4; :: thesis: verum

end;A4: ( v in the carrier of V & v in I0 & x = (MorphsZQ V) . v ) by FUNCT_2:64;

reconsider v = v as Element of V by A4;

l . v in RAT by NUMBERS:14, TARSKI:def 3;

hence ex y being object st

( y in RAT & S

A5: for x being object st x in the carrier of (Z_MQ_VectSp V) holds

S

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

proof

then reconsider lq = lq as Linear_Combination of IQ by K2, VECTSP_6:def 4, XBOOLE_1:1;
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 (Z_MQ_VectSp V) such that

A9: x = z and

A10: lq . z <> 0. F_Rat by A7;

thus contradiction by A5, A8, A9, A10; :: thesis: verum

end;assume that

A7: x in Carrier lq and

A8: not x in IQ0 ; :: thesis: contradiction

consider z being Element of (Z_MQ_VectSp V) such that

A9: x = z and

A10: lq . z <> 0. F_Rat by A7;

thus contradiction by A5, A8, A9, A10; :: thesis: verum

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 ; :: thesis: ( 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

proof

hence U1:
l = lq * (MorphsZQ V)
by FUNCT_1:2, A12, A13; :: thesis: Carrier lq = (MorphsZQ V) .: (Carrier l)
let x be object ; :: thesis: ( x in dom l implies l . x = (lq * (MorphsZQ V)) . x )

assume x in dom l ; :: thesis: l . x = (lq * (MorphsZQ V)) . x

then reconsider v = x as Element of V ;

reconsider w = (MorphsZQ V) . v as Element of (Z_MQ_VectSp V) ;

end;assume x in dom l ; :: thesis: l . x = (lq * (MorphsZQ V)) . x

then reconsider v = x as Element of V ;

reconsider w = (MorphsZQ V) . v as Element of (Z_MQ_VectSp V) ;

per cases
( v in I0 or not v in I0 )
;

end;

suppose
v in I0
; :: thesis: l . x = (lq * (MorphsZQ V)) . x

then
w in IQ0
by FUNCT_2:35;

then consider v0 being Element of V such that

A16: ( v0 in I0 & w = (MorphsZQ V) . v0 & lq . w = l . v0 ) by A5;

v0 = v by A16, FUNCT_2:19, F1;

hence l . x = (lq * (MorphsZQ V)) . x by A13, A16, FUNCT_1:12; :: thesis: verum

end;then consider v0 being Element of V such that

A16: ( v0 in I0 & w = (MorphsZQ V) . v0 & lq . w = l . v0 ) by A5;

v0 = v by A16, FUNCT_2:19, F1;

hence l . x = (lq * (MorphsZQ V)) . x by A13, A16, FUNCT_1:12; :: thesis: verum

suppose A18:
not v in I0
; :: thesis: l . x = (lq * (MorphsZQ V)) . x

then A19:
l . v = 0. F_Rat
;

not w in IQ0

hence l . x = (lq * (MorphsZQ V)) . x by A13, A19, FUNCT_1:12; :: thesis: verum

end;not w in IQ0

proof

then
lq . w = 0. F_Rat
by A5;
assume
w in IQ0
; :: thesis: contradiction

then consider v0 being Element of V such that

A16: ( v0 in I0 & w = (MorphsZQ V) . v0 & lq . w = l . v0 ) by A5;

thus contradiction by A16, A18, F1, FUNCT_2:19; :: thesis: verum

end;then consider v0 being Element of V such that

A16: ( v0 in I0 & w = (MorphsZQ V) . v0 & lq . w = l . v0 ) by A5;

thus contradiction by A16, A18, F1, FUNCT_2:19; :: thesis: verum

hence l . x = (lq * (MorphsZQ V)) . x by A13, A19, FUNCT_1:12; :: thesis: verum

IQ0 c= Carrier lq

proof

hence
Carrier lq = (MorphsZQ V) .: (Carrier l)
by A11; :: thesis: verum
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 = (MorphsZQ V) . v ) by FUNCT_2:64;

reconsider v = v as Element of V by A4;

x = (MorphsZQ V) . v by A4;

then reconsider y = x as Element of (Z_MQ_VectSp V) ;

X1: lq . y = l . v by A4, A13, U1, FUNCT_1:12;

l . v <> 0 by ZMODUL02:8, A4;

hence x in Carrier lq by X1; :: thesis: verum

end;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 = (MorphsZQ V) . v ) by FUNCT_2:64;

reconsider v = v as Element of V by A4;

x = (MorphsZQ V) . v by A4;

then reconsider y = x as Element of (Z_MQ_VectSp V) ;

X1: lq . y = l . v by A4, A13, U1, FUNCT_1:12;

l . v <> 0 by ZMODUL02:8, A4;

hence x in Carrier lq by X1; :: thesis: verum