let X, Y be set ; :: thesis: for x being object
for f being Function of X,Y st Y <> {} & x in X holds
f . x in Y
let x be object ; :: 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 by Th4;
hence f . x in Y ; :: thesis: verum