rng ([0] I) c= {{} } by FUNCOP_1:19;
hence [0] I is empty-yielding by RELAT_1:def 15; :: thesis: verum