theorem :: POLYDIFF:51

for r, s being Element of F_Real holds poly_diff <%r,s%> = <%s%>