theorem :: NEWTON06:17

for a being Real holds frac (a * a) = frac (((2 * [\a/]) * (frac a)) + ((frac a) * (frac a)))