let f be Element of Funcs (X,Y); :: thesis: f is Z -valued

per cases ( f = {} or Funcs (X,Y) <> {} ) by SUBSET_1:def 1;

suppose f = {} ; :: thesis: f is Z -valued

then rng f = {} ;
hence rng f c= Z ; :: according to RELAT_1:def 19 :: thesis: verum

end;

suppose Funcs (X,Y) <> {} ; :: thesis: f is Z -valued

then rng f c= Y by FUNCT_2:92;
hence rng f c= Z by XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: verum

end;

end;