let p be prime Element of INT.Ring; :: thesis: for V being free Z_Module

for I being Basis 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

l . v = lq . (ZMtoMQV (V,p,v))

let V be free Z_Module; :: thesis: for I being Basis 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

l . v = lq . (ZMtoMQV (V,p,v))

let I be Basis 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

l . v = 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

l . v = lq . (ZMtoMQV (V,p,v))

consider l being Linear_Combination of I such that

A1: 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)) ) by Th23;

take l ; :: thesis: for v being Vector of V st v in I holds

l . v = lq . (ZMtoMQV (V,p,v))

l . v = lq . (ZMtoMQV (V,p,v)) ; :: thesis: verum

for I being Basis 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

l . v = lq . (ZMtoMQV (V,p,v))

let V be free Z_Module; :: thesis: for I being Basis 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

l . v = lq . (ZMtoMQV (V,p,v))

let I be Basis 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

l . v = 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

l . v = lq . (ZMtoMQV (V,p,v))

consider l being Linear_Combination of I such that

A1: 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)) ) by Th23;

take l ; :: thesis: for v being Vector of V st v in I holds

l . v = lq . (ZMtoMQV (V,p,v))

now :: thesis: for v being Vector of V st v in I holds

l . v = lq . (ZMtoMQV (V,p,v))

hence
for v being Vector of V st v in I holds l . v = lq . (ZMtoMQV (V,p,v))

let v be Vector of V; :: thesis: ( v in I implies l . v = lq . (ZMtoMQV (V,p,v)) )

assume A2: v in I ; :: thesis: l . v = lq . (ZMtoMQV (V,p,v))

then consider w being Vector of V such that

A3: ( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) ) by A1;

ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v) by A3, ZMODUL01:67;

hence l . v = lq . (ZMtoMQV (V,p,v)) by A2, A3, Th21; :: thesis: verum

end;assume A2: v in I ; :: thesis: l . v = lq . (ZMtoMQV (V,p,v))

then consider w being Vector of V such that

A3: ( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) ) by A1;

ZMtoMQV (V,p,w) = ZMtoMQV (V,p,v) by A3, ZMODUL01:67;

hence l . v = lq . (ZMtoMQV (V,p,v)) by A2, A3, Th21; :: thesis: verum

l . v = lq . (ZMtoMQV (V,p,v)) ; :: thesis: verum