let p be Polynomial of F_Real; :: thesis: poly_diff (- p) = - (poly_diff p)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (poly_diff (- p)) . n = (- (poly_diff p)) . n
A1: (poly_diff p) . n = (p . (n + 1)) * (n + 1) by Def5;
dom (- p) = NAT by FUNCT_2:def 1;
then A2: (- p) /. (n + 1) = - (p /. (n + 1)) by VFUNCT_1:def 5;
A3: dom (- (poly_diff p)) = NAT by FUNCT_2:def 1;
thus (poly_diff (- p)) . n = ((- p) . (n + 1)) * (n + 1) by Def5
.= - ((poly_diff p) /. n) by A1, A2
.= (- (poly_diff p)) /. n by A3, VFUNCT_1:def 5
.= (- (poly_diff p)) . n ; :: thesis: verum