theorem Th28: :: EUCLID_5:28

for f1, f2 being FinSequence of REAL st len f1 = 3 & len f2 = 3 holds
mlt (f1,f2) = <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*>