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