let A, B be non empty set ; :: thesis: for x being Element of A

for f being Function of A,B holds x in dom f

let x be Element of A; :: thesis: for f being Function of A,B holds x in dom f

let f be Function of A,B; :: thesis: x in dom f

x in A ;

hence x in dom f by FUNCT_2:def 1; :: thesis: verum

for f being Function of A,B holds x in dom f

let x be Element of A; :: thesis: for f being Function of A,B holds x in dom f

let f be Function of A,B; :: thesis: x in dom f

x in A ;

hence x in dom f by FUNCT_2:def 1; :: thesis: verum