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

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