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