let M be MetrSpace; :: thesis: for n being Nat
for F being Subset-Family of M
for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds
ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
let n be Nat; :: thesis: for F being Subset-Family of M
for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds
ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
let F be Subset-Family of M; :: thesis: for p being FinSequence st F is being_ball-family & rng p = F & dom p = Seg (n + 1) holds
ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
let p be FinSequence; :: thesis: ( F is being_ball-family & rng p = F & dom p = Seg (n + 1) implies ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) )
assume that
A1: F is being_ball-family and
A2: rng p = F and
A3: dom p = Seg (n + 1) ; :: thesis: ex G being Subset-Family of M st
( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
n + 1 in dom p by A3, FINSEQ_1:4;
then p . (n + 1) in F by A2, FUNCT_1:def 3;
then consider x being Point of M such that
A4: ex r being Real st p . (n + 1) = Ball (x,r) by A1, TOPMETR:def 4;
consider r being Real such that
A5: p . (n + 1) = Ball (x,r) by A4;
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15;
A6: rng q c= rng p by RELAT_1:70;
then reconsider G = rng q as Subset-Family of M by A2, XBOOLE_1:1;
reconsider G = G as Subset-Family of M ;
len p = n + 1 by A3, FINSEQ_1:def 3;
then n <= len p by NAT_1:11;
then A7: dom q = Seg n by FINSEQ_1:17;
then A8: (dom q) \/ {(n + 1)} = dom p by A3, FINSEQ_1:9;
A9: ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r))

proof

take x ; :: thesis: ex r being Real st union F c= (union G) \/ (Ball (x,r))
reconsider r = r as Real ;
take r ; :: thesis: union F c= (union G) \/ (Ball (x,r))
union F c= (union G) \/ (Ball (x,r))

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in union F or t in (union G) \/ (Ball (x,r)) )
assume t in union F ; :: thesis: t in (union G) \/ (Ball (x,r))
then consider A being set such that
A10: t in A and
A11: A in F by TARSKI:def 4;
consider s being object such that
A12: s in dom p and
A13: A = p . s by A2, A11, FUNCT_1:def 3;

now :: thesis: ( ( s in dom q & t in (union G) \/ (Ball (x,r)) ) or ( s in {(n + 1)} & t in (union G) \/ (Ball (x,r)) ) )

per cases ( s in dom q or s in {(n + 1)} ) by A8, A12, XBOOLE_0:def 3;

case s in dom q ; :: thesis: t in (union G) \/ (Ball (x,r))

then ( q . s in G & q . s = A ) by A13, FUNCT_1:47, FUNCT_1:def 3;
then A14: t in union G by A10, TARSKI:def 4;
union G c= (union G) \/ (Ball (x,r)) by XBOOLE_1:7;
hence t in (union G) \/ (Ball (x,r)) by A14; :: thesis: verum

end;

case s in {(n + 1)} ; :: thesis: t in (union G) \/ (Ball (x,r))

then p . s = Ball (x,r) by A5, TARSKI:def 1;
hence t in (union G) \/ (Ball (x,r)) by A10, A13, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence t in (union G) \/ (Ball (x,r)) ; :: thesis: verum

end;

hence union F c= (union G) \/ (Ball (x,r)) ; :: thesis: verum

end;

take G ; :: thesis: ( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) )
for x being set st x in G holds
ex y being Point of M ex r being Real st x = Ball (y,r) by A1, A2, A6, TOPMETR:def 4;
hence ( G is finite & G is being_ball-family & ex q being FinSequence st
( rng q = G & dom q = Seg n & ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball (x,r)) ) ) by A7, A9, TOPMETR:def 4; :: thesis: verum