theorem Th3: :: PDIFF_4:3

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