theorem Th67: :: ANPROJ_8:83

for a being Real
for p being FinSequence of 1 -tuples_on REAL st len p = 3 holds
M2F (a * p) = a * (M2F p)