let UN be Universe; :: thesis: for X being set
for Y being non empty set
for f being Function of X,Y st f in UN holds
X in UN
let X be set ; :: thesis: for Y being non empty set
for f being Function of X,Y st f in UN holds
X in UN
let Y be non empty set ; :: thesis: for f being Function of X,Y st f in UN holds
X in UN
let f be Function of X,Y; :: thesis: ( f in UN implies X in UN )
assume A1: f in UN ; :: thesis: X in UN
dom f = X by FUNCT_2:def 1;
hence X in UN by A1, Th37; :: thesis: verum