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