consider R being ManySortedRelation of X such that
A1: ( R = I --> {} & R is terminating ) by Th77;
take R ; :: thesis: R is empty-yielding
rng R c= {{}} by A1, FUNCOP_1:13;
hence R is empty-yielding by RELAT_1:def 15; :: thesis: verum