theorem Th45: :: FUNCT_3:45

for X, Y being set holds rng (pr2 (X,Y)) c= Y