reconsider g = exp_R1 as differentiable Function of REAL,REAL ;
reconsider f1 = exp_R as differentiable Function of REAL,REAL ;
A1: REAL --> 1 = f1 (#) g by Lm26, RFUNCT_1:31;
reconsider h = REAL --> 1 as constant Function of REAL,REAL by XREAL_0:def 1, FUNCOP_1:45;
reconsider f1dg = f1 (#) (g `|) as Function of REAL,REAL ;
A2: REAL --> 0 = (f1 (#) g) `| by A1, POLYDIFF:11
.= (g (#) (f1 `|)) + (f1 (#) (g `|)) by POLYDIFF:16 ;
A3: (REAL --> 0) - (g (#) (f1 `|)) = (- (g (#) (f1 `|))) + ((dom (- (g (#) (f1 `|)))) --> 0) by FUNCT_2:def 1
.= - (g (#) (f1 `|)) by POLYDIFF:6 ;
A4: - (g (#) f1) = (f1 (#) (g `|)) + ((g (#) (f1 `|)) - (g (#) (f1 `|))) by INTEGRA8:32, RFUNCT_1:8, A2, A3
.= (f1 (#) (g `|)) + (REAL --> 0) by Lm27
.= f1dg + ((dom f1dg) --> 0) by FUNCT_2:def 1
.= (g `|) (#) f1 by POLYDIFF:6 ;
A5: dom (- g) = REAL by Lm23A, VALUED_1:def 5;
- g = 1 (#) (- g) by RFUNCT_1:21
.= (- g) (#) (f1 / f1) by A5, Lm26, POLYDIFF:5
.= ((- g) (#) f1) / f1 by RFUNCT_1:36
.= ((g `|) (#) f1) / f1 by A4, VALUED_2:25
.= (g `|) (#) (REAL --> 1) by Lm26, RFUNCT_1:36
.= ((dom (g `|)) --> 1) (#) (g `|) by FUNCT_2:def 1
.= 1 (#) (g `|) by POLYDIFF:5
.= g `| by RFUNCT_1:21 ;
hence exp_R1 `| = - exp_R1 ; :: thesis: verum