let M be MetrSpace; :: thesis: for n being Nat
for F being Subset-Family of M
for p being FinSequence st F is finite & 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 finite & 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 finite & 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 finite & 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 A1: ( F is finite & F is being_ball-family & rng p = F & 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) ) )
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:19;
len p = n + 1 by A1, FINSEQ_1:def 3;
then n <= len p by NAT_1:11;
then A2: ( len q = n & dom q = Seg n ) by FINSEQ_1:21;
then A3: (dom q) \/ {(n + 1)} = dom p by A1, FINSEQ_1:11;
A4: ( dom q c= dom p & rng q c= rng p ) by RELAT_1:89, RELAT_1:99;
then reconsider G = rng q as Subset-Family of M by A1, XBOOLE_1:1;
reconsider G = G as Subset-Family of M ;
A5: G is being_ball-family

proof

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, A4, TOPMETR:def 4;
hence G is being_ball-family by TOPMETR:def 4; :: thesis: verum

end;

n + 1 in dom p by A1, FINSEQ_1:6;
then p . (n + 1) in F by A1, FUNCT_1:def 5;
then consider x being Point of M such that
A6: ex r being Real st p . (n + 1) = Ball x,r by A1, TOPMETR:def 4;
consider r being Real such that
A7: p . (n + 1) = Ball x,r by A6;
A8: ex x being Point of M ex r being Real st union F c= (union G) \/ (Ball x,r)

proof

A9: union F c= (union G) \/ (Ball x,r)

proof

let t be set ; :: 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 & A in F ) by TARSKI:def 4;
consider s being set such that
A11: ( s in dom p & A = p . s ) by A1, A10, FUNCT_1:def 5;

now

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

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

then A13: q . s in G by FUNCT_1:def 5;
q . s = A by A11, A12, FUNCT_1:70;
then A14: t in union G by A10, A13, 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 A7, TARSKI:def 1;
hence t in (union G) \/ (Ball x,r) by A10, A11, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

end;

take x ; :: thesis: ex r being Real st union F c= (union G) \/ (Ball x,r)
take r ; :: thesis: union F c= (union G) \/ (Ball x,r)
thus union F c= (union G) \/ (Ball x,r) by A9; :: 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) ) )
thus ( 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 A2, A5, A8, FINSEQ_1:73; :: thesis: verum