let n be Element of NAT ; :: thesis: for r being Real
for z, x being Element of COMPLEX n holds
( z in Ball x,r iff |.(x - z).| < r )
let r be Real; :: thesis: for z, x being Element of COMPLEX n holds
( z in Ball x,r iff |.(x - z).| < r )
let z, x be Element of COMPLEX n; :: thesis: ( z in Ball x,r iff |.(x - z).| < r )
A1: |.(z - x).| = |.(x - z).| by Th74;
( 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 ) ) ;
hence ( z in Ball x,r iff |.(x - z).| < r ) by A1; :: thesis: verum