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

proof

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

end;

hence ( dom (proj (2,2)) = REAL 2 & rng (proj (2,2)) = REAL ) by FUNCT_2:10, FUNCT_2:def 1; :: thesis: for x, y being Real holds (proj (2,2)) . <*x,y*> = y
let x, y be Real; :: thesis: (proj (2,2)) . <*x,y*> = y
reconsider x = x, y = y as Element of REAL by XREAL_0:def 1;

now :: thesis: for x, y being Element of REAL holds (proj (2,2)) . <*x,y*> = y

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:101;
then (proj (2,2)) . <*x,y*> = <*x,y*> . 2 by PDIFF_1:def 1;
hence (proj (2,2)) . <*x,y*> = y ; :: thesis: verum

end;

then (proj (2,2)) . <*x,y*> = y ;
hence (proj (2,2)) . <*x,y*> = y ; :: thesis: verum