let a be positive Real; :: thesis: ( frac a = 1 / 2 implies frac (2 * a) = 0 )
assume A1: frac a = 1 / 2 ; :: thesis: frac (2 * a) = 0
frac (2 * a) = frac (2 * (frac a)) by FR3;
hence frac (2 * a) = 0 by A1; :: thesis: verum