let F, f be Function; :: thesis: ( F .: ({},f) = {} & F .: (f,{}) = {} )
F .: ({},f) = F * {} by Th1;
hence ( F .: ({},f) = {} & F .: (f,{}) = {} ) by Th1; :: thesis: verum