let F be FinSequence of REAL ; :: thesis: ( F = mlt F1,F2 iff F = multreal .: F1,F2 )
A1: dom (mlt F1,F2) = (dom F1) /\ (dom F2) by VALUED_1:def 4;
reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm4;
dom multreal = [:REAL ,REAL :] by FUNCT_2:def 1;
then [:(rng F3),(rng F4):] c= dom multreal by ZFMISC_1:119;
then A2: dom (multreal .: F1,F2) = (dom F1) /\ (dom F2) by FUNCOP_1:84;
thus ( F = mlt F1,F2 implies F = multreal .: F1,F2 ) :: thesis: ( F = multreal .: F1,F2 implies F = mlt F1,F2 )

proof

assume A3: F = mlt F1,F2 ; :: thesis: F = multreal .: F1,F2
for z being set st z in dom (multreal .: F1,F2) holds
F . z = multreal . (F1 . z),(F2 . z)

proof

let z be set ; :: thesis: ( z in dom (multreal .: F1,F2) implies F . z = multreal . (F1 . z),(F2 . z) )
assume z in dom (multreal .: F1,F2) ; :: thesis: F . z = multreal . (F1 . z),(F2 . z)
thus F . z = (F1 . z) * (F2 . z) by A3, VALUED_1:5
.= multreal . (F1 . z),(F2 . z) by BINOP_2:def 11 ; :: thesis: verum

end;

hence F = multreal .: F1,F2 by A1, A2, A3, FUNCOP_1:27; :: thesis: verum

end;

assume A4: F = multreal .: F1,F2 ; :: thesis: F = mlt F1,F2

now

let c be set ; :: thesis: ( c in dom F implies F . c = (F1 . c) * (F2 . c) )
assume c in dom F ; :: thesis: F . c = (F1 . c) * (F2 . c)
hence F . c = multreal . (F1 . c),(F2 . c) by A4, FUNCOP_1:28
.= (F1 . c) * (F2 . c) by BINOP_2:def 11 ;
:: thesis: verum

end;

hence F = mlt F1,F2 by A2, A4, VALUED_1:def 4; :: thesis: verum