A1: rng (1_. F_Rat) c= (rng (0_. F_Rat)) \/ {(1. F_Rat)} by FUNCT_7:100;
A2: {(1. F_Rat)} c= INT by ZFMISC_1:31, GAUSSINT:def 14;
rng (0_. F_Rat) c= INT by RELAT_1:def 19;
then (rng (0_. F_Rat)) \/ {(1. F_Rat)} c= INT by A2, XBOOLE_1:8;
then rng (1_. F_Rat) c= INT by A1;
hence 1_. F_Rat is INT -valued by RELAT_1:def 19; :: thesis: verum