set f = p .--> x;
thus not p .--> x is empty ; :: thesis: p .--> x is homogeneous
thus dom (p .--> x) is with_common_domain ; :: according to MARGREL1:def 21 :: thesis: verum