theorem Th55: :: POLYDIFF:55

for p, q being Polynomial of F_Real holds Eval (p + q) = (Eval p) + (Eval q)