let S be RealUnitarySpace; :: thesis: for x being Point of S
for y being Point of (MetricSpaceNorm (RUSp2RNSp S))
for r being Real st x = y holds
Ball (x,r) = Ball (y,r)
let x be Point of S; :: thesis: for y being Point of (MetricSpaceNorm (RUSp2RNSp S))
for r being Real st x = y holds
Ball (x,r) = Ball (y,r)
let y be Point of (MetricSpaceNorm (RUSp2RNSp S)); :: thesis: for r being Real st x = y holds
Ball (x,r) = Ball (y,r)
let r be Real; :: thesis: ( x = y implies Ball (x,r) = Ball (y,r) )
assume A1: x = y ; :: thesis: Ball (x,r) = Ball (y,r)
set PM = MetricSpaceNorm (RUSp2RNSp S);
A2: Ball (y,r) = { z where z is Element of (MetricSpaceNorm (RUSp2RNSp S)) : dist (y,z) < r } by METRIC_1:def 14;
for p being object holds
( p in Ball (x,r) iff p in Ball (y,r) )

proof

let p be object ; :: thesis: ( p in Ball (x,r) iff p in Ball (y,r) )

hereby :: thesis: ( p in Ball (y,r) implies p in Ball (x,r) )

assume p in Ball (x,r) ; :: thesis: p in Ball (y,r)
then consider z being Point of S such that
A3: ( p = z & ||.(x - z).|| < r ) ;
reconsider w = z as Element of (MetricSpaceNorm (RUSp2RNSp S)) ;
dist (y,w) < r by A3, Th1, A1;
hence p in Ball (y,r) by A3, A2; :: thesis: verum

end;

assume p in Ball (y,r) ; :: thesis: p in Ball (x,r)
then consider w being Point of (MetricSpaceNorm (RUSp2RNSp S)) such that
A4: ( p = w & dist (y,w) < r ) by A2;
reconsider z = w as Element of S ;
||.(x - z).|| < r by A4, Th1, A1;
hence p in Ball (x,r) by A4; :: thesis: verum

end;

hence Ball (x,r) = Ball (y,r) by TARSKI:2; :: thesis: verum