theorem Lm1: :: E_TRANS1:6

for n being Nat
for f being Element of the carrier of (Polynom-Ring F_Rat) holds n * f = (In (n,F_Rat)) * f