theorem Th35: :: MATRPROB:35

for e1, e2 being FinSequence of REAL
for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)