reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;
let F be FinSequence of COMPLEX ; ( 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) )
( F = multcomplex .: (F1,F2) implies F = mlt (F1,F2) )
assume A4:
F = multcomplex .: (F1,F2)
; F = mlt (F1,F2)
hence
F = mlt (F1,F2)
by A1, A4, VALUED_1:def 4; verum