let V be torsion-free Z_Module; :: thesis: ( ( for v being Vector of (Z_MQ_VectSp V) holds v is Vector of (DivisibleMod V) ) & ( for v being Vector of (DivisibleMod V) holds v is Vector of (Z_MQ_VectSp V) ) & 0. (DivisibleMod V) = 0. (Z_MQ_VectSp V) )
A1: Z_MQ_VectSp V = ModuleStr(# (Class (EQRZM V)),(addCoset V),(zeroCoset V),(lmultCoset V) #) by ZMODUL04:def 5;
thus for v being Vector of (Z_MQ_VectSp V) holds v is Vector of (DivisibleMod V) by A1, defDivisibleMod; :: thesis: ( ( for v being Vector of (DivisibleMod V) holds v is Vector of (Z_MQ_VectSp V) ) & 0. (DivisibleMod V) = 0. (Z_MQ_VectSp V) )
thus for v being Vector of (DivisibleMod V) holds v is Vector of (Z_MQ_VectSp V) by A1, defDivisibleMod; :: thesis: 0. (DivisibleMod V) = 0. (Z_MQ_VectSp V)
thus 0. (DivisibleMod V) = 0. (Z_MQ_VectSp V) by A1, defDivisibleMod; :: thesis: verum