let X, Y be RealNormSpace; :: thesis:
let x be Point of X; :: thesis:
let y be Point of Y; :: thesis:
let z be Point of [:X,Y:]; :: thesis:
let r1 be Real; :: thesis:
assume A1: ( 0 < r1 & z = [x,y] ) ; :: thesis:
take r2 = r1 / 2; :: thesis:
thus ( 0 < r2 & r2 < r1 ) by A1, XREAL_1:215, XREAL_1:216; :: thesis:
A2: (r1 ^2) / 2 < r1 ^2 by A1, SQUARE_1:12, XREAL_1:216;
thus [:(Ball (x,r2)),(Ball (y,r2)):] c= Ball (z,r1) :: thesis:

proof

let w be object ; :: according to TARSKI:def 3 :: thesis:
assume w in [:(Ball (x,r2)),(Ball (y,r2)):] ; :: thesis:
then consider x1, y1 being object such that
A3: ( x1 in Ball (x,r2) & y1 in Ball (y,r2) & w = [x1,y1] ) by ZFMISC_1:def 2;
reconsider x1 = x1 as Point of X by A3;
reconsider y1 = y1 as Point of Y by A3;
[x1,y1] is set ;
then reconsider xy = w as Point of [:X,Y:] by A3;
ex p being Point of X st
( x1 = p & ||.(x - p).|| < r2 ) by A3;
then A4: ||.(x - x1).|| ^2 < r2 ^2 by SQUARE_1:16;
ex p being Point of Y st
( y1 = p & ||.(y - p).|| < r2 ) by A3;
then A5: ||.(y - y1).|| ^2 < r2 ^2 by SQUARE_1:16;
- xy = [(- x1),(- y1)] by A3, PRVECT_3:18;
then z - xy = [(x - x1),(y - y1)] by A1, PRVECT_3:18;
then A7: ||.(z - xy).|| = sqrt ((||.(x - x1).|| ^2) + (||.(y - y1).|| ^2)) by LMNR0;
(||.(x - x1).|| ^2) + (||.(y - y1).|| ^2) < (r2 ^2) + (r2 ^2) by A4, A5, XREAL_1:8;
then (||.(x - x1).|| ^2) + (||.(y - y1).|| ^2) < r1 ^2 by A2, XXREAL_0:2;
then sqrt ((||.(x - x1).|| ^2) + (||.(y - y1).|| ^2)) < sqrt (r1 ^2) by SQUARE_1:27;
then ||.(z - xy).|| < r1 by A1, A7, SQUARE_1:22;
hence w in Ball (z,r1) ; :: thesis:

end;