per cases ( k in dom f or not k in dom f ) ;

suppose k in dom f ; :: thesis: f . k is integer

then f . k = f /. k by PARTFUN1:def 8;
hence f . k is integer ; :: thesis: verum

end;

suppose not k in dom f ; :: thesis: f . k is integer

hence f . k is integer by FUNCT_1:def 4; :: thesis: verum

end;

end;