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 )
proof
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;
defpred S1[ 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 S1[n,d]
proof
let n be Nat; :: thesis: ( n in Seg (len X) implies ex d being object st S1[n,d] )
assume n in Seg (len X) ; :: thesis: ex d being object st S1[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: S1[n, Ball ((x . i),(CST . i))]
thus S1[n, Ball ((x . i),(CST . i))] ; :: thesis: verum
end;
consider Y being FinSequence such that
A7: ( dom Y = Seg (len X) & ( for n being Nat st n in Seg (len X) holds
S1[n,Y . n] ) ) from FINSEQ_1:sch 1(A6);
 not {} in rng Y
proof
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 reconsider Y = Y as non-empty non empty FinSequence by A7, FINSEQ_1:def 3, RELAT_1:def 9;
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
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;
for z being object st z in product Y holds
z in Ball (x,r)
proof
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) ) )
proof
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_1:def 11; :: thesis: verum
end;
then A20: for i0 being object st i0 in dom (carr X) holds
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 )
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;
then |.(normsequence (X,xx1)).| <= sqrt ((s0 * s0) * (len X)) by A22, NDIFF823;
then ||.(x - x1).|| < r by A4, A21, XXREAL_0:2;
hence z in Ball (x,r) by A15; :: thesis: verum
end;
hence ( 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)) ) ) ) by A5, A14, TARSKI:def 3; :: thesis: verum