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))
now :: thesis: 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;
hence for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ; :: thesis: verum