set f = {} ;
reconsider f = {} as PartFunc of (X *),Y by XBOOLE_1:2;
take f ; :: thesis: f is homogeneous
thus dom f is with_common_domain ; :: according to MARGREL1:def 21 :: thesis: verum