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