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

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

end;

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;hence (PROJ (m,n)) .: (Ball (p,r)) = ].((p /. n) - r),((p /. n) + r).[ by A2; :: thesis: verum

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))

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;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 ].((p /. n) - r),((p /. n) + r).[ or y in (PROJ (m,n)) .: (Ball (p,r)) )
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;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

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