theorem :: NEWTON06:16

for a being Real holds frac (a * a) = frac (((2 * a) * (frac a)) - ((frac a) * (frac a)))