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 Th4; :: thesis: verum