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

.= 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