let n, m be Nat; :: thesis: for r being Real
for p being Point of () st n in dom p holds
(PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[

let r be Real; :: thesis: for p being Point of () st n in dom p holds
(PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[

let p be Point of (); :: 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).[
per cases ( r <= 0 or 0 < r ) ;
suppose A2: 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 A2; :: thesis: verum
end;
suppose A3: 0 < r ; :: thesis: (PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[
A4: dom p = Seg m by FINSEQ_1:89;
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 object ; :: 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 () such that
A5: x in Ball (p,r) and
A6: y = (PROJ (m,n)) . x by FUNCT_2:65;
A7: (PROJ (m,n)) . x = x /. n by Def6;
A8: |.(x - p).| < r by ;
0 <= Sum (sqr (x - p)) by RVSUM_1:86;
then (sqrt (Sum (sqr (x - p)))) ^2 = Sum (sqr (x - p)) by SQUARE_1:def 2;
then A9: Sum (sqr (x - p)) < r ^2 by ;
dom x = Seg m by FINSEQ_1:89;
then ((x /. n) - (p /. n)) ^2 <= Sum (sqr (x - p)) by ;
then ((x /. n) - (p /. n)) ^2 < r ^2 by ;
then ( - r < (x /. n) - (p /. n) & (x /. n) - (p /. n) < r ) by ;
then ( (- r) + (p /. n) < ((x /. n) - (p /. n)) + (p /. n) & ((x /. n) - (p /. n)) + (p /. n) < r + (p /. n) ) by XREAL_1:6;
hence y in ].((p /. n) - r),((p /. n) + r).[ by ; :: thesis: verum
end;
let y be object ; :: 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 A10: 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:24;
A11: dom X = dom p by FUNCT_7:30;
A12: p /. n = p . n by ;
( (p /. n) - r < y & y < (p /. n) + r ) by ;
then A13: ( y - (p /. n) < r & - r < y - (p /. n) ) by ;
(p +* (n,y)) - p = (0* m) +* (n,(y - (p . n))) by Th17;
then |.((p +* (n,y)) - p).| = |.(y - (p . n)).| by A1, A4, Th13;
then |.((p +* (n,y)) - p).| < r by ;
then A14: p +* (n,y) in Ball (p,r) by TOPREAL9:7;
(PROJ (m,n)) . (p +* (n,y)) = (p +* (n,y)) /. n by Def6
.= X . n by
.= y by ;
hence y in (PROJ (m,n)) .: (Ball (p,r)) by ; :: thesis: verum
end;
end;