let n, m be Nat; :: thesis: ( n in Seg m implies PROJ (m,n) is open )
set f = PROJ (m,n);
assume A1: n in Seg m ; :: thesis: PROJ (m,n) is open
for p being Point of (TOP-REAL m)
for r being positive Real ex s being positive Real st ].(((PROJ (m,n)) . p) - s),(((PROJ (m,n)) . p) + s).[ c= (PROJ (m,n)) .: (Ball (p,r))

proof

let p be Point of (TOP-REAL m); :: thesis: for r being positive Real ex s being positive Real st ].(((PROJ (m,n)) . p) - s),(((PROJ (m,n)) . p) + s).[ c= (PROJ (m,n)) .: (Ball (p,r))
let r be positive Real; :: thesis: ex s being positive Real st ].(((PROJ (m,n)) . p) - s),(((PROJ (m,n)) . p) + s).[ c= (PROJ (m,n)) .: (Ball (p,r))
take r ; :: thesis: ].(((PROJ (m,n)) . p) - r),(((PROJ (m,n)) . p) + r).[ c= (PROJ (m,n)) .: (Ball (p,r))
A2: dom p = Seg m by FINSEQ_1:89;
p /. n = (PROJ (m,n)) . p by Def6;
hence ].(((PROJ (m,n)) . p) - r),(((PROJ (m,n)) . p) + r).[ c= (PROJ (m,n)) .: (Ball (p,r)) by A2, A1, Th55; :: thesis: verum

end;

hence PROJ (m,n) is open by TOPS_4:13; :: thesis: verum