let F be real-valued FinSequence; :: thesis: mlt (<*> REAL ),F = <*> REAL
F is FinSequence of REAL by Lm4;
hence mlt (<*> REAL ),F = <*> REAL by FINSEQ_2:87; :: thesis: verum