set mult = multcomplex || 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 multcomplex
by FUNCT_2:def 1;
then A1:
dom (multcomplex || 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
(multcomplex || G_INT_SET) . z in G_INT_SET
proof
let z be
object ;
( z in [:G_INT_SET,G_INT_SET:] implies (multcomplex || G_INT_SET) . z in G_INT_SET )
assume A2:
z in [:G_INT_SET,G_INT_SET:]
;
(multcomplex || 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;
(multcomplex || G_INT_SET) . z =
multcomplex . (
x1,
y1)
by A2, A3, FUNCT_1:49
.=
x1 * y1
by BINOP_2:def 5
;
hence
(multcomplex || G_INT_SET) . z in G_INT_SET
;
verum
end;
hence
multcomplex || G_INT_SET is BinOp of G_INT_SET
by A1, FUNCT_2:3; verum