let X, Y, x be set ; :: thesis: for f being Function of X,Y st Y <> {} & x in X holds
f . x in Y
let f be Function of X,Y; :: thesis: ( Y <> {} & x in X implies f . x in Y )
assume ( Y <> {} & x in X ) ; :: thesis: f . x in Y
then ( f . x in rng f & rng f c= Y ) by Th6;
hence f . x in Y ; :: thesis: verum