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