let p, q be Polynomial of F_Real; poly_diff (p + q) = (poly_diff p) + (poly_diff q)
let n be Element of NAT ; FUNCT_2:def 8 (poly_diff (p + q)) . n = ((poly_diff p) + (poly_diff q)) . n
A1:
(poly_diff p) . n = (p . (n + 1)) * (n + 1)
by Def5;
A2:
(poly_diff q) . n = (q . (n + 1)) * (n + 1)
by Def5;
A3:
(p + q) . (n + 1) = (p . (n + 1)) + (q . (n + 1))
by NORMSP_1:def 2;
thus (poly_diff (p + q)) . n =
((p + q) . (n + 1)) * (n + 1)
by Def5
.=
((poly_diff p) . n) + ((poly_diff q) . n)
by A1, A2, A3
.=
((poly_diff p) + (poly_diff q)) . n
by NORMSP_1:def 2
; verum