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