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 UNIALG_1:def 1 :: thesis: verum