A1: (dom exp_R) \ (exp_R " {0}) = REAL by FUNCT_2:def 1, Lm23A;
A2: dom (exp_R / exp_R) = (dom exp_R) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def 1
.= REAL /\ ((dom exp_R) \ (exp_R " {0})) by FUNCT_2:def 1
.= REAL by A1 ;
reconsider f = exp_R / exp_R as Function of REAL,REAL by A2, FUNCT_2:def 1;
reconsider g = REAL --> 1 as Function of REAL,REAL by XREAL_0:def 1, FUNCOP_1:45;
for x being object st x in REAL holds
f . x = g . x

proof

let x be object ; :: thesis: ( x in REAL implies f . x = g . x )
assume A3: x in REAL ; :: thesis: f . x = g . x
then A4: exp_R . x <> 0 by SIN_COS:54;
reconsider r = exp_R . x as Real ;
(exp_R / exp_R) . x = r * (r ") by A2, A3, RFUNCT_1:def 1
.= 1 by A4, XCMPLX_0:def 7
.= (REAL --> 1) . x by A3, FUNCOP_1:7 ;
hence f . x = g . x ; :: thesis: verum

end;

hence exp_R / exp_R = REAL --> 1 by FUNCT_2:12; :: thesis: verum