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:110;
mlt ((len x) |-> 1),y = y by Th31;
hence mlt ((len x) |-> 1),x = x ; :: thesis: verum