let p be prime Element of INT.Ring; :: thesis: for V being Z_Module
for I being Subset of V
for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

let V be Z_Module; :: thesis: for I being Subset of V
for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

let I be Subset of V; :: thesis: for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

let lq be Linear_Combination of Z_MQ_VectSp (V,p); :: thesis: ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

set ZQ = Z_MQ_VectSp (V,p);
per cases ( I is empty or not I is empty ) ;
suppose A1: I is empty ; :: thesis: ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

set l = the Linear_Combination of I;
take the Linear_Combination of I ; :: thesis: for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & the Linear_Combination of I . w = lq . (ZMtoMQV (V,p,v)) )

thus for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & the Linear_Combination of I . w = lq . (ZMtoMQV (V,p,v)) ) by A1; :: thesis: verum
end;
suppose A2: not I is empty ; :: thesis: ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

set X = { (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } ;
now :: thesis: for x being object st x in { (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } holds
x in the carrier of (Z_MQ_VectSp (V,p))
let x be object ; :: thesis: ( x in { (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } implies x in the carrier of (Z_MQ_VectSp (V,p)) )
assume x in { (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V,p))
then consider v being Vector of V such that
A3: ( x = ZMtoMQV (V,p,v) & v in I ) ;
thus x in the carrier of (Z_MQ_VectSp (V,p)) by A3; :: thesis: verum
end;
then reconsider X = { (ZMtoMQV (V,p,v)) where v is Vector of V : v in I } as Subset of (Z_MQ_VectSp (V,p)) by TARSKI:def 3;
consider v0 being object such that
A4: v0 in I by ;
reconsider v0 = v0 as Vector of V by A4;
ZMtoMQV (V,p,v0) in X by A4;
then reconsider X = X as non empty Subset of (Z_MQ_VectSp (V,p)) ;
defpred S1[ Element of X, Element of V] means ( \$2 in \$1 & \$2 in I );
A5: for x being Element of X ex v being Element of V st S1[x,v]
proof
let x be Element of X; :: thesis: ex v being Element of V st S1[x,v]
x in X ;
then consider v being Vector of V such that
A6: ( x = ZMtoMQV (V,p,v) & v in I ) ;
thus ex v being Element of V st S1[x,v] by ; :: thesis: verum
end;
consider F being Function of X, the carrier of V such that
A7: for x being Element of X holds S1[x,F . x] from
A8: now :: thesis: for y being object st y in rng F holds
y in I
let y be object ; :: thesis: ( y in rng F implies y in I )
assume y in rng F ; :: thesis: y in I
then consider x being object such that
A9: ( x in X & F . x = y ) by FUNCT_2:11;
reconsider x = x as Element of X by A9;
thus y in I by A9, A7; :: thesis: verum
end;
then A10: rng F c= I ;
defpred S2[ Element of V, Element of (GF p)] means ( ( \$1 in rng F implies \$2 = lq . (ZMtoMQV (V,p,\$1)) ) & ( not \$1 in rng F implies \$2 = 0 ) );
A11: for v being Element of V ex y being Element of (GF p) st S2[v,y]
proof
let v be Element of V; :: thesis: ex y being Element of (GF p) st S2[v,y]
per cases ( v in rng F or not v in rng F ) ;
suppose A12: v in rng F ; :: thesis: ex y being Element of (GF p) st S2[v,y]
reconsider y = lq . (ZMtoMQV (V,p,v)) as Element of (GF p) ;
take y ; :: thesis: S2[v,y]
thus S2[v,y] by A12; :: thesis: verum
end;
suppose A13: not v in rng F ; :: thesis: ex y being Element of (GF p) st S2[v,y]
0. (GF p) is Element of (GF p) ;
then reconsider F0 = 0 as Element of (GF p) by EC_PF_1:11;
take F0 ; :: thesis: S2[v,F0]
thus S2[v,F0] by A13; :: thesis: verum
end;
end;
end;
A14: Segm p c= INT by NUMBERS:17;
consider f being Function of the carrier of V,(GF p) such that
A15: for v being Element of V holds S2[v,f . v] from A16: for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) )
proof
let v be Vector of V; :: thesis: ( v in I implies ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) ) )

assume v in I ; :: thesis: ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) )

then A17: ZMtoMQV (V,p,v) in X ;
then A18: F . (ZMtoMQV (V,p,v)) in rng F by FUNCT_2:4;
reconsider w = F . (ZMtoMQV (V,p,v)) as Element of V by ;
take w ; :: thesis: ( w in I & w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) )
A19: f . w = lq . (ZMtoMQV (V,p,w)) by ;
thus w in I by ; :: thesis: ( w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) )
thus w in ZMtoMQV (V,p,v) by ; :: thesis: f . w = lq . (ZMtoMQV (V,p,v))
thus f . w = lq . (ZMtoMQV (V,p,v)) by ; :: thesis: verum
end;
reconsider l = f as Function of the carrier of V,INT by ;
reconsider l = l 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 } ;
A20: 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;
A21: now :: thesis: for x being object st x in { v where v is Element of V : l . v <> 0 } holds
x in rng F
let x be object ; :: thesis: ( x in { v where v is Element of V : l . v <> 0 } implies x in rng F )
assume x in { v where v is Element of V : l . v <> 0 } ; :: thesis: x in rng F
then consider v being Element of V such that
A22: ( x = v & l . v <> 0 ) ;
thus x in rng F by ; :: thesis: verum
end;
then A23: { v where v is Element of V : l . v <> 0 } c= rng F ;
now :: thesis: for x being object st x in F " { v where v is Element of V : l . v <> 0 } holds
x in Carrier lq
let x be object ; :: thesis: ( x in F " { v where v is Element of V : l . v <> 0 } implies x in Carrier lq )
assume A24: x in F " { v where v is Element of V : l . v <> 0 } ; :: thesis: x in Carrier lq
then A25: ( x in X & F . x in { v where v is Element of V : l . v <> 0 } ) by FUNCT_2:38;
then consider v being Element of V such that
A26: ( F . x = v & l . v <> 0 ) ;
A27: S2[v,f . v] by A15;
lq . (ZMtoMQV (V,p,v)) <> 0. (GF p) by ;
then A28: ZMtoMQV (V,p,v) in Carrier lq ;
reconsider w = x as Element of X by A24;
A29: ( F . w in w & F . w in I ) by A7;
consider v1 being Vector of V such that
A30: ( w = ZMtoMQV (V,p,v1) & v1 in I ) by A25;
v in ZMtoMQV (V,p,v) by ZMODUL01:58;
then (ZMtoMQV (V,p,v)) /\ (ZMtoMQV (V,p,v1)) <> {} by ;
hence x in Carrier lq by ; :: thesis: verum
end;
then F " { v where v is Element of V : l . v <> 0 } c= Carrier lq ;
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;
T = Carrier l ;
then reconsider l = l as Linear_Combination of I by ;
take l ; :: thesis: for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

now :: thesis: for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )
let v be Vector of V; :: thesis: ( v in I implies ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) ) )

assume v in I ; :: thesis: ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )

then ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & f . w = lq . (ZMtoMQV (V,p,v)) ) by A16;
hence ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) ) ; :: thesis: verum
end;
hence for v being Vector of V st v in I holds
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) ) ; :: thesis: verum
end;
end;