let n be Nat; :: thesis: for r1 being Real
for z1 being Element of COMPLEX n holds Ball (z1,r1) is open
let r1 be Real; :: thesis: for z1 being Element of COMPLEX n holds Ball (z1,r1) is open
let z1 be Element of COMPLEX n; :: thesis: Ball (z1,r1) is open
let x be Element of COMPLEX n; :: according to SEQ_4:def 14 :: thesis: ( x in Ball (z1,r1) implies ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (z1,r1) ) ) )
assume x in Ball (z1,r1) ; :: thesis: ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (z1,r1) ) )
then A1: |.(z1 - x).| < r1 by Th109;
take r = r1 - |.(z1 - x).|; :: thesis: ( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (z1,r1) ) )
thus 0 < r by A1, XREAL_1:50; :: thesis: for z being Element of COMPLEX n st |.z.| < r holds
x + z in Ball (z1,r1)
let z be Element of COMPLEX n; :: thesis: ( |.z.| < r implies x + z in Ball (z1,r1) )
assume |.z.| < r ; :: thesis: x + z in Ball (z1,r1)
then A2: |.z.| + |.(z1 - x).| < r + |.(z1 - x).| by XREAL_1:6;
(z1 - x) - z = z1 - (x + z) by Th74;
then |.(z1 - (x + z)).| <= |.z.| + |.(z1 - x).| by Th98;
then |.(z1 - (x + z)).| < r + |.(z1 - x).| by A2, XXREAL_0:2;
hence x + z in Ball (z1,r1) by Th109; :: thesis: verum