set f = proj 1,1;
for x1, x2 being set st x1 in dom (proj 1,1) & x2 in dom (proj 1,1) & (proj 1,1) . x1 = (proj 1,1) . x2 holds
x1 = x2

proof

let x1, x2 be set ; :: thesis: ( x1 in dom (proj 1,1) & x2 in dom (proj 1,1) & (proj 1,1) . x1 = (proj 1,1) . x2 implies x1 = x2 )
assume that
A1: x1 in dom (proj 1,1) and
A2: x2 in dom (proj 1,1) and
A3: (proj 1,1) . x1 = (proj 1,1) . x2 ; :: thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of REAL 1 by A1, A2;
x1 is Tuple of 1, REAL by A1, FINSEQ_2:151;
then consider d1 being Element of REAL such that
A4: x1 = <*d1*> by FINSEQ_2:117;
d1 = <*d1*> . 1 by FINSEQ_1:57;
then d1 = (proj 1,1) . y1 by A4, Def1;
then A5: d1 = y2 . 1 by A3, Def1;
x2 is Tuple of 1, REAL by A2, FINSEQ_2:151;
then ex d2 being Element of REAL st x2 = <*d2*> by FINSEQ_2:117;
hence x1 = x2 by A4, A5, FINSEQ_1:57; :: thesis: verum

end;

then A6: proj 1,1 is one-to-one by FUNCT_1:def 8;
A7: dom (proj 1,1) = REAL 1 by FUNCT_2:def 1;

A8: now

let x be Element of REAL ; :: thesis: ( (proj 1,1) . <*x*> = x & ((proj 1,1) " ) . x = <*x*> )
A9: <*x*> is Element of 1 -tuples_on REAL by FINSEQ_2:118;
then (proj 1,1) . <*x*> = <*x*> . 1 by Def1;
hence (proj 1,1) . <*x*> = x by FINSEQ_1:57; :: thesis: ((proj 1,1) " ) . x = <*x*>
hence ((proj 1,1) " ) . x = <*x*> by A7, A6, A9, FUNCT_1:56; :: thesis: verum

end;

A10: for y being set st y in REAL holds
ex x being set st
( x in REAL 1 & y = (proj 1,1) . x )

proof

let y be set ; :: thesis: ( y in REAL implies ex x being set st
( x in REAL 1 & y = (proj 1,1) . x ) )
assume y in REAL ; :: thesis: ex x being set 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:118;
(proj 1,1) . x = x . 1 by Def1;
then (proj 1,1) . x = y by FINSEQ_1:57;
hence ex x being set st
( x in REAL 1 & y = (proj 1,1) . x ) ; :: thesis: verum

end;

then rng (proj 1,1) = REAL by FUNCT_2:16;
then proj 1,1 is onto by FUNCT_2:def 3;
hence ( proj 1,1 is bijective & 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 A6, A10, A8, FUNCT_2:16, FUNCT_2:def 1; :: thesis: verum