theorem Th32: :: MATRPROB:32

for x being FinSequence of REAL holds mlt (((len x) |-> 1),x) = x