let x be set ; :: thesis: for F being Function holds F [;] (x,{}) = {}
let F be Function; :: thesis: F [;] (x,{}) = {}
F [;] (x,{}) = F .: (((dom {}) --> x),{}) ;
hence F [;] (x,{}) = {} by Th3; :: thesis: verum