let x be set ; :: thesis: {} . x = {}
not x in dom {} ;
hence {} . x = {} by FUNCT_1:def 4; :: thesis: verum