let i, n be Nat; :: thesis: ( i in Seg n implies proj (i,n) is onto )

set f = proj (i,n);

assume A1: i in Seg n ; :: thesis: proj (i,n) is onto

for y being object st y in REAL holds

ex x being object st

( x in REAL n & y = (proj (i,n)) . x )

hence proj (i,n) is onto by FUNCT_2:def 3; :: thesis: verum

set f = proj (i,n);

assume A1: i in Seg n ; :: thesis: proj (i,n) is onto

for y being object st y in REAL holds

ex x being object st

( x in REAL n & y = (proj (i,n)) . x )

proof

then
rng (proj (i,n)) = REAL
by FUNCT_2:10;
let y be object ; :: thesis: ( y in REAL implies ex x being object st

( x in REAL n & y = (proj (i,n)) . x ) )

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

( x in REAL n & y = (proj (i,n)) . x )

then reconsider y1 = y as Element of REAL ;

reconsider x = n |-> y1 as Element of REAL n ;

(proj (i,n)) . x = x . i by Def1;

then (proj (i,n)) . x = y by A1, FINSEQ_2:57;

hence ex x being object st

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

end;( x in REAL n & y = (proj (i,n)) . x ) )

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

( x in REAL n & y = (proj (i,n)) . x )

then reconsider y1 = y as Element of REAL ;

reconsider x = n |-> y1 as Element of REAL n ;

(proj (i,n)) . x = x . i by Def1;

then (proj (i,n)) . x = y by A1, FINSEQ_2:57;

hence ex x being object st

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

hence proj (i,n) is onto by FUNCT_2:def 3; :: thesis: verum