theorem Th2: :: PDIFF_2:2

( dom (proj (2,2)) = REAL 2 & rng (proj (2,2)) = REAL & ( for x, y being Real holds (proj (2,2)) . <*x,y*> = y ) )