set f = proj 2,2;
A1: for y being set st y in REAL holds
ex z being set st
( z in REAL 2 & y = (proj 2,2) . z )

proof

consider x being Element of REAL ;
let y be set ; :: thesis: ( y in REAL implies ex z being set st
( z in REAL 2 & y = (proj 2,2) . z ) )
assume y in REAL ; :: thesis: ex z being set st
( z in REAL 2 & y = (proj 2,2) . z )
then reconsider y1 = y as Element of REAL ;
reconsider z = <*x,y1*> as Element of REAL 2 by FINSEQ_2:121;
(proj 2,2) . z = z . 2 by PDIFF_1:def 1;
then (proj 2,2) . z = y by FINSEQ_1:61;
hence ex z being set st
( z in REAL 2 & y = (proj 2,2) . z ) ; :: thesis: verum

end;

now

let x, y be Element of REAL ; :: thesis: (proj 2,2) . <*x,y*> = y
<*x,y*> is Element of 2 -tuples_on REAL by FINSEQ_2:121;
then (proj 2,2) . <*x,y*> = <*x,y*> . 2 by PDIFF_1:def 1;
hence (proj 2,2) . <*x,y*> = y by FINSEQ_1:61; :: thesis: verum

end;

hence ( dom (proj 2,2) = REAL 2 & rng (proj 2,2) = REAL & ( for x, y being Element of REAL holds (proj 2,2) . <*x,y*> = y ) ) by A1, FUNCT_2:16, FUNCT_2:def 1; :: thesis: verum