let f be Function; :: thesis: {} +* f = f
dom {} c= dom f by XBOOLE_1:2;
hence {} +* f = f by Th20; :: thesis: verum