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

proof

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

end;

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