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 FR2;
hence frac (a * a) = frac (((2 * [\a/]) * (frac a)) + ((frac a) * (frac a))) ; :: thesis: verum