set mult = multcomplex || (FQ x);
set theCFComplex = the carrier of F_Complex;
A0: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
[:(FQ x),(FQ x):] c= [:COMPLEX,COMPLEX:] by A0;
then [:(FQ x),(FQ x):] c= dom multcomplex by FUNCT_2:def 1;
then A1: dom (multcomplex || (FQ x)) = [:(FQ x),(FQ x):] by RELAT_1:62;
for z being object st z in [:(FQ x),(FQ x):] holds
(multcomplex || (FQ x)) . z in FQ x

proof

let z be object ; :: thesis: ( z in [:(FQ x),(FQ x):] implies (multcomplex || (FQ x)) . z in FQ x )
assume A2: z in [:(FQ x),(FQ x):] ; :: thesis: (multcomplex || (FQ x)) . z in FQ x
consider x1, y1 being object such that
A3: ( x1 in FQ x & y1 in FQ x & z = [x1,y1] ) by A2, ZFMISC_1:def 2;
reconsider x2 = x1, y2 = y1 as Element of the carrier of F_Complex by A3;
(multcomplex || (FQ x)) . z = multcomplex . (x2,y2) by A2, A3, FUNCT_1:49
.= x2 * y2 by BINOP_2:def 5 ;
hence (multcomplex || (FQ x)) . z in FQ x by A3, Lm47; :: thesis: verum

end;

hence multcomplex || (FQ x) is BinOp of (FQ x) by A1, FUNCT_2:3; :: thesis: verum