theorem Th34: :: PARTIT1:34

for Y being non empty set holds ERl (%I Y) = id Y