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