set f = proj (1,2);

for x being object st x in REAL holds

ex z being object st

( z in REAL 2 & x = (proj (1,2)) . z )

let x, y be Real; :: thesis: (proj (1,2)) . <*x,y*> = x

reconsider x = x, y = y as Element of REAL by XREAL_0:def 1;

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

for x being object st x in REAL holds

ex z being object st

( z in REAL 2 & x = (proj (1,2)) . z )

proof

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

let x be object ; :: thesis: ( x in REAL implies ex z being object st

( z in REAL 2 & x = (proj (1,2)) . z ) )

assume x in REAL ; :: thesis: ex z being object st

( z in REAL 2 & x = (proj (1,2)) . z )

then reconsider x1 = x as Element of REAL ;

reconsider z = <*x1, the Element of REAL *> as Element of REAL 2 by FINSEQ_2:101;

(proj (1,2)) . z = z . 1 by PDIFF_1:def 1;

then (proj (1,2)) . z = x by FINSEQ_1:44;

hence ex z being object st

( z in REAL 2 & x = (proj (1,2)) . z ) ; :: thesis: verum

end;let x be object ; :: thesis: ( x in REAL implies ex z being object st

( z in REAL 2 & x = (proj (1,2)) . z ) )

assume x in REAL ; :: thesis: ex z being object st

( z in REAL 2 & x = (proj (1,2)) . z )

then reconsider x1 = x as Element of REAL ;

reconsider z = <*x1, the Element of REAL *> as Element of REAL 2 by FINSEQ_2:101;

(proj (1,2)) . z = z . 1 by PDIFF_1:def 1;

then (proj (1,2)) . z = x by FINSEQ_1:44;

hence ex z being object st

( z in REAL 2 & x = (proj (1,2)) . z ) ; :: thesis: verum

let x, y be Real; :: thesis: (proj (1,2)) . <*x,y*> = x

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 (1,2)) . <*x,y*> = x

then
(proj (1,2)) . <*x,y*> = x
;let x, y be Element of REAL ; :: thesis: (proj (1,2)) . <*x,y*> = x

<*x,y*> is Element of 2 -tuples_on REAL by FINSEQ_2:101;

then (proj (1,2)) . <*x,y*> = <*x,y*> . 1 by PDIFF_1:def 1;

hence (proj (1,2)) . <*x,y*> = x by FINSEQ_1:44; :: thesis: verum

end;<*x,y*> is Element of 2 -tuples_on REAL by FINSEQ_2:101;

then (proj (1,2)) . <*x,y*> = <*x,y*> . 1 by PDIFF_1:def 1;

hence (proj (1,2)) . <*x,y*> = x by FINSEQ_1:44; :: thesis: verum

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