let n be Nat; :: thesis: for r being Real
for x, z being Element of COMPLEX n holds
( z in Ball (x,r) iff |.(x - z).| < r )
let r be Real; :: thesis: for x, z being Element of COMPLEX n holds
( z in Ball (x,r) iff |.(x - z).| < r )
let x, z be Element of COMPLEX n; :: thesis: ( z in Ball (x,r) iff |.(x - z).| < r )
A1: ( z in { z2 where z2 is Element of COMPLEX n : |.(z2 - x).| < r } iff ex z1 being Element of COMPLEX n st
( z = z1 & |.(z1 - x).| < r ) ) ;
|.(z - x).| = |.(x - z).| by Th103;
hence ( z in Ball (x,r) iff |.(x - z).| < r ) by A1; :: thesis: verum