theorem :: ZMODUL08:36
for V being free finite-rank Z_Module
for r being non zero Element of F_Rat holds rank (EMbedding (r,V)) = rank V