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

proof

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

end;

now

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

end;

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