set f = proj (1,1);
for x1, x2 being object 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 object ; :: 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:131;
then consider d1 being Element of REAL such that
A4: x1 = <*d1*> by FINSEQ_2:97;
d1 = <*d1*> . 1 ;
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:131;
then ex d2 being Element of REAL st x2 = <*d2*> by FINSEQ_2:97;
hence x1 = x2 by A4, A5; :: thesis: verum

end;

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

A8: now :: thesis: for x being Real holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> )

let x be Real; :: thesis: ( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> )
reconsider xx = x as Element of REAL by XREAL_0:def 1;
A9: <*xx*> is Element of 1 -tuples_on REAL by FINSEQ_2:98;
then (proj (1,1)) . <*x*> = <*x*> . 1 by Def1;
hence (proj (1,1)) . <*x*> = x ; :: thesis: ((proj (1,1)) ") . x = <*x*>
hence ((proj (1,1)) ") . x = <*x*> by A7, A6, A9, FUNCT_1:34; :: thesis: verum

end;

A10: 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 Def1;
then (proj (1,1)) . x = y ;
hence ex x being object st
( x in REAL 1 & y = (proj (1,1)) . x ) ; :: thesis: verum

end;

then rng (proj (1,1)) = REAL by FUNCT_2:10;
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 Real holds
( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) by A6, A10, A8, FUNCT_2:10, FUNCT_2:def 1; :: thesis: verum