set mu = multcomplex || REAL;
[:REAL,REAL:] c= [:COMPLEX,COMPLEX:] by NUMBERS:11, ZFMISC_1:96;
then A1: [:REAL,REAL:] c= dom multcomplex by FUNCT_2:def 1;
then A2: dom (multcomplex || REAL) = [:REAL,REAL:] by RELAT_1:62;
A3: dom multreal = [:REAL,REAL:] by FUNCT_2:def 1;
for z being object st z in dom (multcomplex || REAL) holds
(multcomplex || REAL) . z = multreal . z

proof

let z be object ; :: thesis: ( z in dom (multcomplex || REAL) implies (multcomplex || REAL) . z = multreal . z )
assume A4: z in dom (multcomplex || REAL) ; :: thesis: (multcomplex || REAL) . z = multreal . z
then consider x, y being object such that
A5: ( x in REAL & y in REAL & z = [x,y] ) by A2, ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Real by A5;
thus (multcomplex || REAL) . z = multcomplex . (x1,y1) by A4, A5, A2, FUNCT_1:49
.= x1 * y1 by BINOP_2:def 5
.= multreal . (x1,y1) by BINOP_2:def 11
.= multreal . z by A5 ; :: thesis: verum

end;

hence multcomplex || REAL = multreal by A1, A3, RELAT_1:62; :: thesis: verum