set ad = addcomplex || G_INT_SET;
[:G_INT_SET,G_INT_SET:] c= [:COMPLEX,COMPLEX:] by ZFMISC_1:96;
then [:G_INT_SET,G_INT_SET:] c= dom addcomplex by FUNCT_2:def 1;
then A1: dom (addcomplex || G_INT_SET) = [:G_INT_SET,G_INT_SET:] by RELAT_1:62;
for z being object st z in [:G_INT_SET,G_INT_SET:] holds
(addcomplex || G_INT_SET) . z in G_INT_SET

proof

let z be object ; :: thesis: ( z in [:G_INT_SET,G_INT_SET:] implies (addcomplex || G_INT_SET) . z in G_INT_SET )
assume A2: z in [:G_INT_SET,G_INT_SET:] ; :: thesis: (addcomplex || G_INT_SET) . z in G_INT_SET
consider x, y being object such that
A3: ( x in G_INT_SET & y in G_INT_SET & z = [x,y] ) by A2, ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as G_INTEG by Th2, A3;
(addcomplex || G_INT_SET) . z = addcomplex . (x1,y1) by A2, A3, FUNCT_1:49
.= x1 + y1 by BINOP_2:def 3 ;
hence (addcomplex || G_INT_SET) . z in G_INT_SET ; :: thesis: verum

end;

hence addcomplex || G_INT_SET is BinOp of G_INT_SET by A1, FUNCT_2:3; :: thesis: verum