theorem :: ZMODUL08:22

for V being torsion-free Z_Module
for vv being Vector of (EMbedding V) ex v being Vector of V st (MorphsZQ V) . v = vv