let X, Y be set ; :: thesis: for f being Function of [:X,Y:],Y holds dom f = [:X,Y:]
let f be Function of [:X,Y:],Y; :: thesis: dom f = [:X,Y:]
( Y is empty implies [:X,Y:] is empty ) by ZFMISC_1:90;
hence dom f = [:X,Y:] by FUNCT_2:def 1; :: thesis: verum