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).[
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;
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;