let n be Element of NAT ; :: thesis: for r being Real
for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball A,r iff dist z,A < r )
let r be Real; :: thesis: for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball A,r iff dist z,A < r )
let z be Element of COMPLEX n; :: thesis: for A being Subset of (COMPLEX n) holds
( z in Ball A,r iff dist z,A < r )
let A be Subset of (COMPLEX n); :: thesis: ( z in Ball A,r iff dist z,A < r )
( z in { z2 where z2 is Element of COMPLEX n : dist z2,A < r } iff ex z1 being Element of COMPLEX n st
( z = z1 & dist z1,A < r ) ) ;
hence ( z in Ball A,r iff dist z,A < r ) ; :: thesis: verum