let p0 be Element of (Polynom-Ring F_Real); :: thesis: for p being Polynomial of F_Real st p0 = p holds
poly_diff p = (Der1 F_Real) . p0
let p be Polynomial of F_Real; :: thesis: ( p0 = p implies poly_diff p = (Der1 F_Real) . p0 )
assume A1: p0 = p ; :: thesis: poly_diff p = (Der1 F_Real) . p0
for n being Nat holds (poly_diff p) . n = ((Der1 F_Real) . p0) . n
proof
let n be Nat; :: thesis: (poly_diff p) . n = ((Der1 F_Real) . p0) . n
(poly_diff p) . n = (p . (n + 1)) * (n + 1) by Def9
.= (n + 1) * (p . (n + 1)) by BINOM:18
.= ((Der1 F_Real) . p0) . n by A1, Def8 ;
hence (poly_diff p) . n = ((Der1 F_Real) . p0) . n ; :: thesis: verum
end;
hence poly_diff p = (Der1 F_Real) . p0 ; :: thesis: verum