let a be positive Real; :: thesis: ( 1 / 2 > frac a implies frac (2 * a) = 2 * (frac a) )
assume A1: 1 / 2 > frac a ; :: thesis: frac (2 * a) = 2 * (frac a)

per cases ( frac a is zero or frac a is positive ) ;

suppose frac a is zero ; :: thesis: frac (2 * a) = 2 * (frac a)

then reconsider a = a as Integer ;
frac (2 * a) = 0 ;
hence frac (2 * a) = 2 * (frac a) ; :: thesis: verum

end;

suppose frac a is positive ; :: thesis: frac (2 * a) = 2 * (frac a)

then reconsider a = a as non integer Real ;
reconsider b = frac a as positive light Real ;
2 * (1 / 2) > 2 * (frac a) by A1, XREAL_1:68;
then reconsider c = 2 * b as positive light Real by COMPLEX3:1;
c = frac (2 * (frac a)) ;
hence frac (2 * a) = 2 * (frac a) by FR3; :: thesis: verum

end;

end;