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