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