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

proof

let z be object ; :: thesis: ( z in [:(FQ x),(FQ x):] implies (addcomplex || (FQ x)) . z in FQ x )
assume A2: z in [:(FQ x),(FQ x):] ; :: thesis: (addcomplex || (FQ x)) . z in FQ x
consider a, b being object such that
A3: a in FQ x and
A4: b in FQ x and
A5: z = [a,b] by A2, ZFMISC_1:def 2;
reconsider x1 = a, y1 = b as Element of the carrier of F_Complex by A3, A4;
(addcomplex || (FQ x)) . z = addcomplex . (a,b) by A2, A5, FUNCT_1:49
.= x1 + y1 by BINOP_2:def 3 ;
hence (addcomplex || (FQ x)) . z in FQ x by A3, A4, Lm46; :: thesis: verum

end;

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