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

A7: dom (proj (1,1)) = REAL 1 by FUNCT_2:def 1;

ex x being object st

( x in REAL 1 & y = (proj (1,1)) . x )

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

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

then A6:
proj (1,1) is one-to-one
by FUNCT_1:def 4;
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 by FINSEQ_1:40;

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, FINSEQ_1:40; :: thesis: verum

end;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 by FINSEQ_1:40;

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, FINSEQ_1:40; :: thesis: verum

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*> )

A10:
for y being object st y in 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 by FINSEQ_1:40; :: thesis: ((proj (1,1)) ") . x = <*x*>

hence ((proj (1,1)) ") . x = <*x*> by A7, A6, A9, FUNCT_1:34; :: thesis: verum

end;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 by FINSEQ_1:40; :: thesis: ((proj (1,1)) ") . x = <*x*>

hence ((proj (1,1)) ") . x = <*x*> by A7, A6, A9, FUNCT_1:34; :: thesis: verum

ex x being object st

( x in REAL 1 & y = (proj (1,1)) . x )

proof

then
rng (proj (1,1)) = REAL
by FUNCT_2:10;
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 by FINSEQ_1:40;

hence ex x being object st

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

end;( 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 by FINSEQ_1:40;

hence ex x being object st

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

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