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 )

proof

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;

then rng (proj (i,n)) = REAL by FUNCT_2:10;
hence proj (i,n) is onto by FUNCT_2:def 3; :: thesis: verum