let n, m be Nat; :: thesis: for r being Real
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; :: 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).[
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 (TOP-REAL m) 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 A5, TOPREAL9:7;
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 A8, SQUARE_1:16;
dom x = Seg m by FINSEQ_1:89;
then ((x /. n) - (p /. n)) ^2 <= Sum (sqr (x - p)) by A4, A1, EUCLID_9:8;
then ((x /. n) - (p /. n)) ^2 < r ^2 by A9, XXREAL_0:2;
then ( - r < (x /. n) - (p /. n) & (x /. n) - (p /. n) < r ) by A3, SQUARE_1:48;
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 A6, A7, XXREAL_1:4; :: 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 A1, PARTFUN1:def 6;
( (p /. n) - r < y & y < (p /. n) + r ) by A10, XXREAL_1:4;
then A13: ( y - (p /. n) < r & - r < y - (p /. n) ) by XREAL_1:19, XREAL_1:20;
(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 A12, A13, SEQ_2:1;
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 A11, A1, PARTFUN1:def 6
.= y by A1, FUNCT_7:31 ;
hence y in (PROJ (m,n)) .: (Ball (p,r)) by A14, FUNCT_2:35; :: thesis: verum
end;
end;