A1: REAL 1 = rng ((proj (1,1)) ") by Lm1, FUNCT_1:33;
REAL = dom ((proj (1,1)) ") by Lm1, FUNCT_1:33;
then reconsider g = (proj (1,1)) " as Function of REAL,(REAL 1) by A1, FUNCT_2:1;
g is onto by A1, FUNCT_2:def 3;
hence ( (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 ) ) by Lm1, FUNCT_1:33; :: thesis: verum