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