per cases ( x in dom Fi or not x in dom Fi ) ;

suppose x in dom Fi ; :: thesis: Fi . x is Integer

then ( Fi . x in rng Fi & rng Fi c= INT ) by FUNCT_1:def 5, RELAT_1:def 19;
hence Fi . x is Integer ; :: thesis: verum

end;

suppose not x in dom Fi ; :: thesis: Fi . x is Integer

hence Fi . x is Integer by FUNCT_1:def 4; :: thesis: verum

end;

end;