take {} ; :: thesis: ( {} is finite & {} is X -defined & {} is Y -valued )
thus ( {} is finite & {} is X -defined & {} is Y -valued ) by FUNCT_1:174, RELAT_1:206; :: thesis: verum