let F, F1, F2 be FinSequence of COMPLEX ; :: thesis: ( F = multcomplex .: F1,F2 implies F = multcomplex .: F2,F1 )
A1: dom multcomplex = [:COMPLEX ,COMPLEX :] by FUNCT_2:def 1;
then A2: [:(rng F2),(rng F1):] c= dom multcomplex by ZFMISC_1:119;
[:(rng F1),(rng F2):] c= dom multcomplex by A1, ZFMISC_1:119;
then A3: dom (multcomplex .: F1,F2) = (dom F1) /\ (dom F2) by FUNCOP_1:84
.= dom (multcomplex .: F2,F1) by A2, FUNCOP_1:84 ;
assume A4: F = multcomplex .: F1,F2 ; :: thesis: F = multcomplex .: F2,F1
for z being set st z in dom (multcomplex .: F2,F1) holds
F . z = multcomplex . (F2 . z),(F1 . z)

proof

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

end;

hence F = multcomplex .: F2,F1 by A4, A3, FUNCOP_1:27; :: thesis: verum