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