A0:
INT = the carrier of INT.Ring
by INT_3:def 3;
set scmult = multcomplex | [:INT,G_INT_SET:];
[:INT,G_INT_SET:] c= [:COMPLEX,COMPLEX:]
by NUMBERS:16, ZFMISC_1:96;
then
[:INT,G_INT_SET:] c= dom multcomplex
by FUNCT_2:def 1;
then A1:
dom (multcomplex | [:INT,G_INT_SET:]) = [:INT,G_INT_SET:]
by RELAT_1:62;
for z being object st z in [:INT,G_INT_SET:] holds
(multcomplex | [:INT,G_INT_SET:]) . z in G_INT_SET
proof
let z be
object ;
( z in [:INT,G_INT_SET:] implies (multcomplex | [:INT,G_INT_SET:]) . z in G_INT_SET )
assume A2:
z in [:INT,G_INT_SET:]
;
(multcomplex | [:INT,G_INT_SET:]) . z in G_INT_SET
consider x,
y being
object such that A3:
(
x in INT &
y in G_INT_SET &
z = [x,y] )
by A2, ZFMISC_1:def 2;
reconsider x1 =
x as
Element of
INT by A3;
reconsider y1 =
y as
G_INTEG by Th2, A3;
(multcomplex | [:INT,G_INT_SET:]) . z =
multcomplex . (
x1,
y1)
by A2, A3, FUNCT_1:49
.=
x1 * y1
by BINOP_2:def 5
;
hence
(multcomplex | [:INT,G_INT_SET:]) . z in G_INT_SET
;
verum
end;
hence
multcomplex | [: the carrier of INT.Ring,G_INT_SET:] is Function of [: the carrier of INT.Ring,G_INT_SET:],G_INT_SET
by A1, FUNCT_2:3, A0; verum