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