let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( len f > 0 implies (exp_R1 (#) ('F' f)) `| REAL = - (exp_R1 (#) (Eval (~ (^ f)))) )
assume A1: len f > 0 ; :: thesis: (exp_R1 (#) ('F' f)) `| REAL = - (exp_R1 (#) (Eval (~ (^ f))))
reconsider t = exp_R1 (#) ('F' f) as Function of REAL,REAL ;
set e1 = exp_R1 ;
set fhw = 'F' f;
A2: ((- 1) (#) (exp_R1 (#) ('F' f))) + (1 (#) (exp_R1 (#) ('F' f))) = t (#) ((- 1) + 1) by TOPREALC:2
.= REAL --> 0 by Lm35 ;
dom (Eval (~ (^ f))) = REAL by FUNCT_2:def 1;
then (dom (exp_R ^)) /\ (dom (Eval (~ (^ f)))) = REAL by Lm23A;
then dom (exp_R1 (#) (Eval (~ (^ f)))) = REAL by VALUED_1:def 4;
then A4: dom (- (exp_R1 (#) (Eval (~ (^ f))))) = REAL by VALUED_1:def 5;
(exp_R1 (#) ('F' f)) `| REAL = (exp_R1 (#) ('F' f)) `|
.= ((exp_R1 `|) (#) ('F' f)) + (exp_R1 (#) (('F' f) `|)) by POLYDIFF:16
.= ((- exp_R1) (#) ('F' f)) + (exp_R1 (#) (('F' f) - (Eval (~ (^ f))))) by Lm28, A1, Lm34
.= ((- exp_R1) (#) ('F' f)) + ((exp_R1 (#) ('F' f)) - (exp_R1 (#) (Eval (~ (^ f))))) by RFUNCT_1:15
.= ((((- 1) (#) exp_R1) (#) ('F' f)) + (exp_R1 (#) ('F' f))) - (exp_R1 (#) (Eval (~ (^ f)))) by RFUNCT_1:23
.= ((((- 1) (#) exp_R1) (#) ('F' f)) + ((1 (#) exp_R1) (#) ('F' f))) - (exp_R1 (#) (Eval (~ (^ f)))) by RFUNCT_1:21
.= (((- 1) (#) (exp_R1 (#) ('F' f))) + ((1 (#) exp_R1) (#) ('F' f))) - (exp_R1 (#) (Eval (~ (^ f)))) by RFUNCT_1:12
.= (- (exp_R1 (#) (Eval (~ (^ f))))) + (REAL --> 0) by A2, RFUNCT_1:12
.= - (exp_R1 (#) (Eval (~ (^ f)))) by A4, POLYDIFF:6 ;
hence (exp_R1 (#) ('F' f)) `| REAL = - (exp_R1 (#) (Eval (~ (^ f)))) ; :: thesis: verum