theorem :: ZMODUL07:18

for A being finite Subset of Rat-Module ex n being Integer st
( n <> 0 & ( for s being Element of Rat-Module st s in Lin A holds
ex m being Integer st s = m / n ) )