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

proof

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

end;

now :: thesis: for x, y, z being Real holds (proj (2,3)) . <*x,y,z*> = y

let x, y, z be Real; :: thesis: (proj (2,3)) . <*x,y,z*> = y
reconsider xx = x, yy = y, zz = z as Element of REAL by XREAL_0:def 1;
<*xx,yy,zz*> is Element of 3 -tuples_on REAL by FINSEQ_2:104;
then (proj (2,3)) . <*x,y,z*> = <*x,y,z*> . 2 by PDIFF_1:def 1;
hence (proj (2,3)) . <*x,y,z*> = y ; :: thesis: verum

end;

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