let m, n be Nat; :: thesis: for r being real number
for p being Point of (TOP-REAL m) st n in dom p holds
(PROJ m,n) .: (Ball p,r) = ].((p /. n) - r),((p /. n) + r).[
let r be real number ; :: thesis: for p being Point of (TOP-REAL m) st n in dom p holds
(PROJ m,n) .: (Ball p,r) = ].((p /. n) - r),((p /. n) + r).[
let p be Point of (TOP-REAL m); :: thesis: ( n in dom p implies (PROJ m,n) .: (Ball p,r) = ].((p /. n) - r),((p /. n) + r).[ )
assume A1: n in dom p ; :: thesis: (PROJ m,n) .: (Ball p,r) = ].((p /. n) - r),((p /. n) + r).[
reconsider P = p as FinSequence of REAL by EUCLID:27;
A2: m in NAT by ORDINAL1:def 13;

per cases ( r <= 0 or 0 < r ) ;

suppose A3: r <= 0 ; :: thesis: (PROJ m,n) .: (Ball p,r) = ].((p /. n) - r),((p /. n) + r).[

then ].((p /. n) - r),((p /. n) + r).[ = {} ;
hence (PROJ m,n) .: (Ball p,r) = ].((p /. n) - r),((p /. n) + r).[ by A3; :: thesis: verum

end;

suppose A4: 0 < r ; :: thesis: (PROJ m,n) .: (Ball p,r) = ].((p /. n) - r),((p /. n) + r).[

A5: dom p = Seg m by EUCLID:3;
thus (PROJ m,n) .: (Ball p,r) c= ].((p /. n) - r),((p /. n) + r).[ :: according to XBOOLE_0:def 10 :: thesis: ].((p /. n) - r),((p /. n) + r).[ c= (PROJ m,n) .: (Ball p,r)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (PROJ m,n) .: (Ball p,r) or y in ].((p /. n) - r),((p /. n) + r).[ )
assume y in (PROJ m,n) .: (Ball p,r) ; :: thesis: y in ].((p /. n) - r),((p /. n) + r).[
then consider x being Element of (TOP-REAL m) such that
A6: x in Ball p,r and
A7: y = (PROJ m,n) . x by FUNCT_2:116;
reconsider y = y as real number by A7;
A8: (PROJ m,n) . x = x /. n by Def6;
A9: |.(x - p).| < r by A2, A6, TOPREAL9:7;
0 <= Sum (sqr (x - p)) by RVSUM_1:116;
then (sqrt (Sum (sqr (x - p)))) ^2 = Sum (sqr (x - p)) by SQUARE_1:def 4;
then A10: Sum (sqr (x - p)) < r ^2 by A9, SQUARE_1:78;
dom x = Seg m by EUCLID:3;
then ((x /. n) - (p /. n)) ^2 <= Sum (sqr (x - p)) by A5, A1, EUCLID_9:8;
then ((x /. n) - (p /. n)) ^2 < r ^2 by A10, XXREAL_0:2;
then ( - r < (x /. n) - (p /. n) & (x /. n) - (p /. n) < r ) by A4, SQUARE_1:118;
then ( (- r) + (p /. n) < ((x /. n) - (p /. n)) + (p /. n) & ((x /. n) - (p /. n)) + (p /. n) < r + (p /. n) ) by XREAL_1:8;
hence y in ].((p /. n) - r),((p /. n) + r).[ by A7, A8, XXREAL_1:4; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in ].((p /. n) - r),((p /. n) + r).[ or y in (PROJ m,n) .: (Ball p,r) )
assume A11: y in ].((p /. n) - r),((p /. n) + r).[ ; :: thesis: y in (PROJ m,n) .: (Ball p,r)
then reconsider y = y as Element of REAL ;
set x = p +* n,y;
reconsider X = p +* n,y as FinSequence of REAL by EUCLID:27;
A12: dom X = dom p by FUNCT_7:32;
A13: p /. n = p . n by A1, PARTFUN1:def 8;
( (p /. n) - r < y & y < (p /. n) + r ) by A11, XXREAL_1:4;
then A14: ( y - (p /. n) < r & - r < y - (p /. n) ) by XREAL_1:21, XREAL_1:22;
(p +* n,y) - p = (0* m) +* n,(y - (p . n)) by Th17;
then |.((p +* n,y) - p).| = abs (y - (p . n)) by A1, A5, Th13;
then |.((p +* n,y) - p).| < r by A13, A14, SEQ_2:9;
then A15: p +* n,y in Ball p,r by A2, TOPREAL9:7;
(PROJ m,n) . (p +* n,y) = (p +* n,y) /. n by Def6
.= X . n by A12, A1, PARTFUN1:def 8
.= y by A1, FUNCT_7:33 ;
hence y in (PROJ m,n) .: (Ball p,r) by A15, FUNCT_2:43; :: thesis: verum

end;

end;