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

suppose x in dom f ; :: thesis: f . x is Element of k

then f . x in rng f by FUNCT_1:3;
hence f . x is Element of k ; :: thesis: verum

end;

suppose A1: not x in dom f ; :: thesis: f . x is Element of k

A2: ( k = 0 or k > 0 ) ;
f . x = 0 by A1, FUNCT_1:def 2;
hence f . x is Element of k by A2, NAT_1:44, SUBSET_1:def 1; :: thesis: verum

end;

end;