set M = Monom (i,b);
( b in Bags X & Bags X = dom (0_ (X,F_Real)) ) by PARTFUN1:def 2, PRE_POLY:def 12;
then Monom (i,b) = (0_ (X,F_Real)) +* (b .--> i) by FUNCT_7:def 3;
then rng (Monom (i,b)) c= (rng (0_ (X,F_Real))) \/ (rng (b .--> i)) by FUNCT_4:17;
then rng (Monom (i,b)) c= INT by INT_1:def 2;
hence Monom (i,b) is INT -valued by RELAT_1:def 19; :: thesis: verum