reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;
let F be FinSequence of COMPLEX ; :: thesis: ( F = mlt (F1,F2) iff F = multcomplex .: (F1,F2) )
dom multcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1;
then [:(rng F3),(rng F4):] c= dom multcomplex by ZFMISC_1:96;
then A1: dom (multcomplex .: (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 = multcomplex .: (F1,F2) ) :: thesis: ( F = multcomplex .: (F1,F2) implies F = mlt (F1,F2) )

proof

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

proof

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

end;

hence F = multcomplex .: (F1,F2) by A1, A2, A3, FUNCOP_1:21; :: thesis: verum

end;

assume A4: F = multcomplex .: (F1,F2) ; :: thesis: F = mlt (F1,F2)

now :: thesis: for c being object st c in dom F holds
F . c = (F1 . c) * (F2 . c)

let c be object ; :: 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 = multcomplex . ((F1 . c),(F2 . c)) by A4, FUNCOP_1:22
.= (F1 . c) * (F2 . c) by BINOP_2:def 5 ;
:: thesis: verum

end;

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