theorem Th43: :: FUNCT_3:43

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