let i, n be Element of 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 set st y in REAL holds
ex x being set st
( x in REAL n & y = (proj i,n) . x )

proof

let y be set ; :: thesis: ( y in REAL implies ex x being set st
( x in REAL n & y = (proj i,n) . x ) )
assume y in REAL ; :: thesis: ex x being set 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 by FINSEQ_2:132;
(proj i,n) . x = x . i by Def1;
then (proj i,n) . x = y by A1, FINSEQ_2:71;
hence ex x being set st
( x in REAL n & y = (proj i,n) . x ) ; :: thesis: verum

end;

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