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

proof

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

end;

now

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

end;

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