let X be set ; :: thesis: for f being Element of Funcs X,X holds dom f = X
let f be Element of Funcs X,X; :: thesis: dom f = X
ex ff being Function st
( f = ff & dom ff = X & rng ff c= X ) by FUNCT_2:def 2;
hence dom f = X ; :: thesis: verum