theorem Th2: :: PDIFF_4:2

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