(f . 1) - (f . 0) is Integer ;
hence difference f is integer by NUMBER06:def 5; :: thesis: verum