theorem Th1: :: PDIFF_4:1

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