let a be Real; :: thesis: frac (a * a) = frac (((2 * a) * (frac a)) - ((frac a) * (frac a)))
frac (a * a) = frac (((a * (frac a)) + (a * (frac a))) - ((frac a) * (frac a))) by FR1;
hence frac (a * a) = frac (((2 * a) * (frac a)) - ((frac a) * (frac a))) ; :: thesis: verum