theorem RL5Th30: :: ZMODUL05:3

for V being Z_Module
for A being finite linearly-independent Subset of V holds card A = rank (Lin A)