take {} ; :: thesis: ( {} is finite & {} is I -defined & {} is f -compatible )
thus ( {} is finite & {} is I -defined & {} is f -compatible ) by FUNCT_1:104, RELAT_1:171; :: thesis: verum