let V be free finite-rank Z_Module; :: thesis: for r being non zero Element of F_Rat holds rank (EMbedding (r,V)) = rank (EMbedding V)
let r be non zero Element of F_Rat; :: thesis: rank (EMbedding (r,V)) = rank (EMbedding V)
consider T being linear-transformation of (EMbedding V),(EMbedding (r,V)) such that
A1: ( ( for v being Element of (Z_MQ_VectSp V) st v in EMbedding V holds
T . v = r * v ) & T is bijective ) by rSB03A;
thus rank (EMbedding (r,V)) = rank (EMbedding V) by A1, ZMODUL06:51; :: thesis: verum