let V be free finite-rank Z_Module; :: thesis: for r being non zero Element of F_Rat holds rank (EMbedding (r,V)) = rank V
let r be non zero Element of F_Rat; :: thesis: rank (EMbedding (r,V)) = rank V
thus rank (EMbedding (r,V)) = rank (EMbedding V) by ThRankrEM1
.= rank V by ThRankEM ; :: thesis: verum