theorem Th1: :: PDIFF_2:1

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