Quelle  function_image_nonempty.pvs

% to be added to Jerry James's function_image_aux theory in the prelude

function_image_nonempty[D: TYPE, R: TYPE]: THEORY

BEGIN

  f: VAR [D -> R]
  S: VAR set[D]

  nonempty_image: JUDGEMENT
    image(f, (S: (nonempty?[D]))) HAS_TYPE (nonempty?[R])

  nonempty_finite_image: JUDGEMENT
    image(f, (S: non_empty_finite_set[D])) HAS_TYPE non_empty_finite_set[R]

%  image_witness: JUDGEMENT
%    f(x: (S)) HAS_TYPE (image?(f, S))

END function_image_nonempty