set y = the Element of Y;
reconsider Z = 0 -tuples_on X as non empty Subset of (X *) by FINSEQ_2:90;
reconsider f = Z --> the Element of Y as PartFunc of (X *),Y ;
take f ; :: thesis: ( not f is empty & f is homogeneous )
thus not f is empty ; :: thesis: f is homogeneous
thus dom f is with_common_domain ; :: according to MARGREL1:def 21 :: thesis: verum