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 ; :: thesis: ( 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:] ; :: thesis: (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 ; :: thesis: 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; :: thesis: verum