dom (((ProjMap J) .:.: (I -indexing (f "))) | (rng f)) = (dom ((ProjMap J) .:.: (I -indexing (f ")))) /\ (rng f) by RELAT_1:61
.= I /\ (rng f) by PARTFUN1:def 2
.= rng f by XBOOLE_1:28 ;
hence ((ProjMap J) .:.: (I -indexing (f "))) | (rng f) is ManySortedSet of rng f by PARTFUN1:def 2; :: thesis: verum