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 )

( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) by FUNCT_2:10, FUNCT_2:def 1, PDIFF_1:1; :: thesis: verum

for y being object st y in REAL holds

ex x being object st

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

proof

hence
( dom (proj (1,1)) = REAL 1 & rng (proj (1,1)) = REAL & ( for x being Element of REAL holds
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;( 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

( (proj (1,1)) . <*x*> = x & ((proj (1,1)) ") . x = <*x*> ) ) ) by FUNCT_2:10, FUNCT_2:def 1, PDIFF_1:1; :: thesis: verum