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

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