let x be FinSequence of REAL ; :: thesis: mlt (((len x) |-> 1),x) = x
reconsider y = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92;
mlt (((len x) |-> 1),y) = y by Th31;
hence mlt (((len x) |-> 1),x) = x ; :: thesis: verum