for r being Real
for fr being Element of F_Real
for p being FinSequence of REAL
for fp being FinSequence of F_Real st r = fr & p = fp holds
r * p = fr * fp