reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2;
let F be FinSequence of REAL ; ( F = mlt (F1,F2) iff F = multreal .: (F1,F2) )
dom multreal = [:REAL,REAL:]
by FUNCT_2:def 1;
then
[:(rng F3),(rng F4):] c= dom multreal
by ZFMISC_1:96;
then A1:
dom (multreal .: (F1,F2)) = (dom F1) /\ (dom F2)
by FUNCOP_1:69;
A2:
dom (mlt (F1,F2)) = (dom F1) /\ (dom F2)
by VALUED_1:def 4;
thus
( F = mlt (F1,F2) implies F = multreal .: (F1,F2) )
( F = multreal .: (F1,F2) implies F = mlt (F1,F2) )
assume A4:
F = multreal .: (F1,F2)
; F = mlt (F1,F2)
hence
F = mlt (F1,F2)
by A1, A4, VALUED_1:def 4; verum