theorem Th2: :: YELLOW_6:2

for Y being non empty set
for J being 1-sorted-yielding ManySortedSet of Y
for i being Element of Y holds (Carrier J) . i = the carrier of (J . i)