let X be RealNormSpace-Sequence; :: thesis: for x being Point of (product X)

for r being Real st 0 < r holds

ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st

( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )

let x be Point of (product X); :: thesis: for r being Real st 0 < r holds

ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st

( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )

let r be Real; :: thesis: ( 0 < r implies ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st

( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) ) )

assume A1: 0 < r ; :: thesis: ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st

( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )

A2: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;

consider s0 being Real such that

A3: ( 0 < s0 & s0 < r ) and

A4: sqrt ((s0 * s0) * (len X)) < r by A1, NDIFF825;

set CST = (len X) |-> s0;

( len X is natural Number & s0 is Element of REAL ) by XREAL_0:def 1;

then reconsider CST = (len X) |-> s0 as Element of (len X) -tuples_on REAL by FINSEQ_2:112;

A5: for i being Element of dom X holds

( 0 < CST . i & CST . i < r )_{1}[ object , object ] means ex i being Element of dom X st

( $1 = i & $2 = Ball ((x . i),(CST . i)) );

A6: for n being Nat st n in Seg (len X) holds

ex d being object st S_{1}[n,d]

A7: ( dom Y = Seg (len X) & ( for n being Nat st n in Seg (len X) holds

S_{1}[n,Y . n] ) )
from FINSEQ_1:sch 1(A6);

not {} in rng Y

take CST ; :: thesis: ex Y being non-empty non empty FinSequence st

( dom CST = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )

take Y ; :: thesis: ( dom CST = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )

thus dom CST = Seg (len X) by FUNCT_2:def 1

.= dom X by FINSEQ_1:def 3 ; :: thesis: ( dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )

thus A12: dom Y = dom X by A7, FINSEQ_1:def 3; :: thesis: ( product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )

A14: for i being Element of dom X holds Y . i = Ball ((x . i),(CST . i))

z in Ball (x,r)

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) ) by A5, A14, TARSKI:def 3; :: thesis: verum

for r being Real st 0 < r holds

ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st

( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )

let x be Point of (product X); :: thesis: for r being Real st 0 < r holds

ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st

( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )

let r be Real; :: thesis: ( 0 < r implies ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st

( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) ) )

assume A1: 0 < r ; :: thesis: ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st

( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )

A2: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;

consider s0 being Real such that

A3: ( 0 < s0 & s0 < r ) and

A4: sqrt ((s0 * s0) * (len X)) < r by A1, NDIFF825;

set CST = (len X) |-> s0;

( len X is natural Number & s0 is Element of REAL ) by XREAL_0:def 1;

then reconsider CST = (len X) |-> s0 as Element of (len X) -tuples_on REAL by FINSEQ_2:112;

A5: for i being Element of dom X holds

( 0 < CST . i & CST . i < r )

proof

defpred S
let i be Element of dom X; :: thesis: ( 0 < CST . i & CST . i < r )

i in dom X ;

then i in Seg (len X) by FINSEQ_1:def 3;

hence ( 0 < CST . i & CST . i < r ) by A3, FINSEQ_2:57; :: thesis: verum

end;i in dom X ;

then i in Seg (len X) by FINSEQ_1:def 3;

hence ( 0 < CST . i & CST . i < r ) by A3, FINSEQ_2:57; :: thesis: verum

( $1 = i & $2 = Ball ((x . i),(CST . i)) );

A6: for n being Nat st n in Seg (len X) holds

ex d being object st S

proof

consider Y being FinSequence such that
let n be Nat; :: thesis: ( n in Seg (len X) implies ex d being object st S_{1}[n,d] )

assume n in Seg (len X) ; :: thesis: ex d being object st S_{1}[n,d]

then reconsider i = n as Element of dom X by FINSEQ_1:def 3;

set d = Ball ((x . i),(CST . i));

take Ball ((x . i),(CST . i)) ; :: thesis: S_{1}[n, Ball ((x . i),(CST . i))]

thus S_{1}[n, Ball ((x . i),(CST . i))]
; :: thesis: verum

end;assume n in Seg (len X) ; :: thesis: ex d being object st S

then reconsider i = n as Element of dom X by FINSEQ_1:def 3;

set d = Ball ((x . i),(CST . i));

take Ball ((x . i),(CST . i)) ; :: thesis: S

thus S

A7: ( dom Y = Seg (len X) & ( for n being Nat st n in Seg (len X) holds

S

not {} in rng Y

proof

then reconsider Y = Y as non-empty non empty FinSequence by A7, FINSEQ_1:def 3, RELAT_1:def 9;
assume
{} in rng Y
; :: thesis: contradiction

then consider z being object such that

A9: ( z in dom Y & {} = Y . z ) by FUNCT_1:def 3;

reconsider n = z as Nat by A9;

consider i being Element of dom X such that

A10: ( n = i & Y . n = Ball ((x . i),(CST . i)) ) by A7, A9;

0 < CST . i by A5;

hence contradiction by A9, A10, NDIFF_8:14; :: thesis: verum

end;then consider z being object such that

A9: ( z in dom Y & {} = Y . z ) by FUNCT_1:def 3;

reconsider n = z as Nat by A9;

consider i being Element of dom X such that

A10: ( n = i & Y . n = Ball ((x . i),(CST . i)) ) by A7, A9;

0 < CST . i by A5;

hence contradiction by A9, A10, NDIFF_8:14; :: thesis: verum

take CST ; :: thesis: ex Y being non-empty non empty FinSequence st

( dom CST = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )

take Y ; :: thesis: ( dom CST = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )

thus dom CST = Seg (len X) by FUNCT_2:def 1

.= dom X by FINSEQ_1:def 3 ; :: thesis: ( dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )

thus A12: dom Y = dom X by A7, FINSEQ_1:def 3; :: thesis: ( product Y c= Ball (x,r) & ( for i being Element of dom X holds

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )

A14: for i being Element of dom X holds Y . i = Ball ((x . i),(CST . i))

proof

for z being object st z in product Y holds
let i be Element of dom X; :: thesis: Y . i = Ball ((x . i),(CST . i))

A13: i in dom X ;

reconsider n = i as Nat ;

n in Seg (len X) by A13, FINSEQ_1:def 3;

then ex i being Element of dom X st

( n = i & Y . n = Ball ((x . i),(CST . i)) ) by A7;

hence Y . i = Ball ((x . i),(CST . i)) ; :: thesis: verum

end;A13: i in dom X ;

reconsider n = i as Nat ;

n in Seg (len X) by A13, FINSEQ_1:def 3;

then ex i being Element of dom X st

( n = i & Y . n = Ball ((x . i),(CST . i)) ) by A7;

hence Y . i = Ball ((x . i),(CST . i)) ; :: thesis: verum

z in Ball (x,r)

proof

hence
( product Y c= Ball (x,r) & ( for i being Element of dom X holds
let z be object ; :: thesis: ( z in product Y implies z in Ball (x,r) )

assume z in product Y ; :: thesis: z in Ball (x,r)

then consider g being Function such that

A15: ( z = g & dom g = dom Y & ( for i being object st i in dom Y holds

g . i in Y . i ) ) by CARD_3:def 5;

A16: dom (carr X) = dom X by DCARXX;

A17: dom g = dom (carr X) by A12, A15, DCARXX;

A18: for i0 being object st i0 in dom (carr X) holds

( g . i0 in (carr X) . i0 & ex i being Element of dom X st

( i0 = i & g . i in Ball ((x . i),(CST . i)) & g . i in the carrier of (X . i) ) )

g . i0 in (carr X) . i0 ;

then reconsider x1 = g as Point of (product X) by A2, A17, CARD_3:def 5;

reconsider y1 = g as Element of product (carr X) by A20, A17, CARD_3:def 5;

reconsider xx1 = x - x1 as Element of product (carr X) by A2;

A21: ||.(x - x1).|| = |.(normsequence (X,xx1)).| by A2, PRVECT_2:def 12;

A22: len (normsequence (X,xx1)) = len X by PRVECT_2:def 11;

then A23: dom (normsequence (X,xx1)) = Seg (len X) by FINSEQ_1:def 3

.= dom X by FINSEQ_1:def 3 ;

then ||.(x - x1).|| < r by A4, A21, XXREAL_0:2;

hence z in Ball (x,r) by A15; :: thesis: verum

end;assume z in product Y ; :: thesis: z in Ball (x,r)

then consider g being Function such that

A15: ( z = g & dom g = dom Y & ( for i being object st i in dom Y holds

g . i in Y . i ) ) by CARD_3:def 5;

A16: dom (carr X) = dom X by DCARXX;

A17: dom g = dom (carr X) by A12, A15, DCARXX;

A18: for i0 being object st i0 in dom (carr X) holds

( g . i0 in (carr X) . i0 & ex i being Element of dom X st

( i0 = i & g . i in Ball ((x . i),(CST . i)) & g . i in the carrier of (X . i) ) )

proof

then A20:
for i0 being object st i0 in dom (carr X) holds
let i0 be object ; :: thesis: ( i0 in dom (carr X) implies ( g . i0 in (carr X) . i0 & ex i being Element of dom X st

( i0 = i & g . i in Ball ((x . i),(CST . i)) & g . i in the carrier of (X . i) ) ) )

assume i0 in dom (carr X) ; :: thesis: ( g . i0 in (carr X) . i0 & ex i being Element of dom X st

( i0 = i & g . i in Ball ((x . i),(CST . i)) & g . i in the carrier of (X . i) ) )

then reconsider i = i0 as Element of dom X by DCARXX;

g . i in Y . i by A12, A15;

then A19: g . i in Ball ((x . i),(CST . i)) by A14;

then g . i in the carrier of (X . i) ;

hence ( g . i0 in (carr X) . i0 & ex i being Element of dom X st

( i0 = i & g . i in Ball ((x . i),(CST . i)) & g . i in the carrier of (X . i) ) ) by A19, PRVECT_2:def 4; :: thesis: verum

end;( i0 = i & g . i in Ball ((x . i),(CST . i)) & g . i in the carrier of (X . i) ) ) )

assume i0 in dom (carr X) ; :: thesis: ( g . i0 in (carr X) . i0 & ex i being Element of dom X st

( i0 = i & g . i in Ball ((x . i),(CST . i)) & g . i in the carrier of (X . i) ) )

then reconsider i = i0 as Element of dom X by DCARXX;

g . i in Y . i by A12, A15;

then A19: g . i in Ball ((x . i),(CST . i)) by A14;

then g . i in the carrier of (X . i) ;

hence ( g . i0 in (carr X) . i0 & ex i being Element of dom X st

( i0 = i & g . i in Ball ((x . i),(CST . i)) & g . i in the carrier of (X . i) ) ) by A19, PRVECT_2:def 4; :: thesis: verum

g . i0 in (carr X) . i0 ;

then reconsider x1 = g as Point of (product X) by A2, A17, CARD_3:def 5;

reconsider y1 = g as Element of product (carr X) by A20, A17, CARD_3:def 5;

reconsider xx1 = x - x1 as Element of product (carr X) by A2;

A21: ||.(x - x1).|| = |.(normsequence (X,xx1)).| by A2, PRVECT_2:def 12;

A22: len (normsequence (X,xx1)) = len X by PRVECT_2:def 11;

then A23: dom (normsequence (X,xx1)) = Seg (len X) by FINSEQ_1:def 3

.= dom X by FINSEQ_1:def 3 ;

now :: thesis: for i0 being Nat st i0 in dom (normsequence (X,xx1)) holds

( 0 <= (normsequence (X,xx1)) . i0 & (normsequence (X,xx1)) . i0 <= s0 )

then
|.(normsequence (X,xx1)).| <= sqrt ((s0 * s0) * (len X))
by A22, NDIFF823;( 0 <= (normsequence (X,xx1)) . i0 & (normsequence (X,xx1)) . i0 <= s0 )

let i0 be Nat; :: thesis: ( i0 in dom (normsequence (X,xx1)) implies ( 0 <= (normsequence (X,xx1)) . i0 & (normsequence (X,xx1)) . i0 <= s0 ) )

assume i0 in dom (normsequence (X,xx1)) ; :: thesis: ( 0 <= (normsequence (X,xx1)) . i0 & (normsequence (X,xx1)) . i0 <= s0 )

then reconsider i = i0 as Element of dom X by A23;

reconsider xx1i = xx1 . i as Point of (X . i) ;

reconsider yi = x . i as Point of (X . i) ;

reconsider y1i = y1 . i as Point of (X . i) ;

i in dom X ;

then A24: i in Seg (len X) by FINSEQ_1:def 3;

A25: (normsequence (X,xx1)) . i = ||.xx1i.|| by PRVECT_2:def 11;

hence 0 <= (normsequence (X,xx1)) . i0 ; :: thesis: (normsequence (X,xx1)) . i0 <= s0

A26: xx1 . i = (x . i) - (y1 . i) by LOPBAN10:26;

ex j being Element of dom X st

( i = j & g . j in Ball ((x . j),(CST . j)) & g . j in the carrier of (X . j) ) by A16, A18;

then ex y being Point of (X . i) st

( y = y1i & ||.((x . i) - y).|| < CST . i ) ;

hence (normsequence (X,xx1)) . i0 <= s0 by A24, A25, A26, FINSEQ_2:57; :: thesis: verum

end;assume i0 in dom (normsequence (X,xx1)) ; :: thesis: ( 0 <= (normsequence (X,xx1)) . i0 & (normsequence (X,xx1)) . i0 <= s0 )

then reconsider i = i0 as Element of dom X by A23;

reconsider xx1i = xx1 . i as Point of (X . i) ;

reconsider yi = x . i as Point of (X . i) ;

reconsider y1i = y1 . i as Point of (X . i) ;

i in dom X ;

then A24: i in Seg (len X) by FINSEQ_1:def 3;

A25: (normsequence (X,xx1)) . i = ||.xx1i.|| by PRVECT_2:def 11;

hence 0 <= (normsequence (X,xx1)) . i0 ; :: thesis: (normsequence (X,xx1)) . i0 <= s0

A26: xx1 . i = (x . i) - (y1 . i) by LOPBAN10:26;

ex j being Element of dom X st

( i = j & g . j in Ball ((x . j),(CST . j)) & g . j in the carrier of (X . j) ) by A16, A18;

then ex y being Point of (X . i) st

( y = y1i & ||.((x . i) - y).|| < CST . i ) ;

hence (normsequence (X,xx1)) . i0 <= s0 by A24, A25, A26, FINSEQ_2:57; :: thesis: verum

then ||.(x - x1).|| < r by A4, A21, XXREAL_0:2;

hence z in Ball (x,r) by A15; :: thesis: verum

( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) ) by A5, A14, TARSKI:def 3; :: thesis: verum