consider y being Element of Y;
reconsider Z = 0 -tuples_on X as non empty Subset of (X * ) by Th13;
reconsider f = Z --> 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 by FUNCOP_1:19; :: according to MARGREL1:def 22 :: thesis: verum