theorem :: ZMODUL05:4

for V being free finite-rank Z_Module holds rank V = rank ((Omega). V)