set f = proj 1,1;
A1: proj 1,1 is one-to-one by Lm1;
A2: ( REAL = dom ((proj 1,1) " ) & REAL 1 = rng ((proj 1,1) " ) ) by Lm1, FUNCT_1:55;
A3: (proj 1,1) " is one-to-one by A1;
reconsider g = (proj 1,1) " as Function of REAL ,(REAL 1) by A2, FUNCT_2:3;
g is onto by A2, FUNCT_2:def 3;
then g is bijective by A3;
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