theorem Th2: :: PDIFF_1:2

( (proj (1,1)) " is Function of REAL,(REAL 1) & (proj (1,1)) " is one-to-one & dom ((proj (1,1)) ") = REAL & rng ((proj (1,1)) ") = REAL 1 & ex g being Function of REAL,(REAL 1) st
( g is bijective & (proj (1,1)) " = g ) )