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 ;
( z in [:(FQ x),(FQ x):] implies (addcomplex || (FQ x)) . z in FQ x )
assume A2:
z in [:(FQ x),(FQ x):]
;
(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;
verum
end;
hence
addcomplex || (FQ x) is BinOp of (FQ x)
by A1, FUNCT_2:3; verum