theorem LMThGM23: :: ZMODLAT2:66

for n being Nat
for r being FinSequence of F_Rat st len r = n holds
ex K being Integer ex Kr being FinSequence of INT.Ring st
( K <> 0 & len Kr = n & ( for i being Nat st i in dom Kr holds
Kr . i = K * (r /. i) ) )