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;