set DR = Der1 F_Real;
let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: ( len f > 0 implies ('F' f) - (Eval (~ (^ f))) = ('F' f) `| )
assume len f > 0 ; :: thesis: ('F' f) - (Eval (~ (^ f))) = ('F' f) `|
then A2: ^ (Sum ('G' f)) = ^ (((Der1 INT.Ring) . (Sum ('G' f))) + f) by Lm19
.= (^ ((Der1 INT.Ring) . (Sum ('G' f)))) + (^ f) by Th27 ;
^ ((Der1 INT.Ring) . (Sum ('G' f))) = (Der1 F_Real) . (^ (Sum ('G' f))) by FIELD_14:66;
then A4: Eval (~ (^ (Sum ('G' f)))) = Eval ((~ ((Der1 F_Real) . (^ (Sum ('G' f))))) + (~ (^ f))) by A2, POLYNOM3:def 10
.= (Eval (~ ((Der1 F_Real) . (^ (Sum ('G' f)))))) + (Eval (~ (^ f))) by POLYDIFF:55
.= (('F' f) `|) + (Eval (~ (^ f))) by Th31 ;
A5: (Eval (~ (^ f))) - (Eval (~ (^ f))) = Eval ((~ (^ f)) - (~ (^ f))) by POLYDIFF:57
.= REAL --> 0 by POLYDIFF:52, POLYNOM3:29 ;
A6: dom (('F' f) `|) = REAL by FUNCT_2:def 1;
('F' f) - (Eval (~ (^ f))) = (('F' f) `|) + (REAL --> 0) by A5, A4, RFUNCT_1:8
.= ('F' f) `| by A6, POLYDIFF:6 ;
hence ('F' f) - (Eval (~ (^ f))) = ('F' f) `| ; :: thesis: verum