let M be MetrSpace; :: thesis: for F being Subset-Family of M st F is finite & F is being_ball-family holds
ex x being Point of M ex r being Real st union F c= Ball x,r
let F be Subset-Family of M; :: thesis: ( F is finite & F is being_ball-family implies ex x being Point of M ex r being Real st union F c= Ball x,r )
assume that
A1: F is finite and
A2: F is being_ball-family ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball x,r
consider p being FinSequence such that
A3: rng p = F by A1, FINSEQ_1:73;
A4: for F being Subset-Family of M st F is finite & F is being_ball-family holds
for n being Nat
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r

proof

defpred S₁[ Nat] means for F being Subset-Family of M st F is finite & F is being_ball-family holds
for n being Nat st n = $1 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
let F be Subset-Family of M; :: thesis: ( F is finite & F is being_ball-family implies for n being Nat st n = k + 1 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r )
assume that
F is finite and
A7: F is being_ball-family ; :: thesis: for n being Nat st n = k + 1 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r
let n be Nat; :: thesis: ( n = k + 1 implies for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r )
assume A8: n = k + 1 ; :: thesis: for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r
let p be FinSequence; :: thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball x,r )
assume ( rng p = F & dom p = Seg n ) ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball x,r
then consider F1 being Subset-Family of M such that
A9: ( F1 is finite & F1 is being_ball-family ) and
A10: ex p1 being FinSequence st
( rng p1 = F1 & dom p1 = Seg k & ex x2 being Point of M ex r2 being Real st union F c= (union F1) \/ (Ball x2,r2) ) by A7, A8, Th2;
consider x1 being Point of M such that
A11: ex r being Real st union F1 c= Ball x1,r by A6, A9, A10;
consider x2 being Point of M such that
A12: ex r2 being Real st union F c= (union F1) \/ (Ball x2,r2) by A10;
consider r2 being Real such that
A13: union F c= (union F1) \/ (Ball x2,r2) by A12;
consider r1 being Real such that
A14: union F1 c= Ball x1,r1 by A11;
consider x being Point of M such that
A15: ex r being Real st (Ball x1,r1) \/ (Ball x2,r2) c= Ball x,r by Th1;
take x ; :: thesis: ex r being Real st union F c= Ball x,r
consider r being Real such that
A16: (Ball x1,r1) \/ (Ball x2,r2) c= Ball x,r by A15;
take r ; :: thesis: union F c= Ball x,r
(union F1) \/ (Ball x2,r2) c= (Ball x1,r1) \/ (Ball x2,r2) by A14, XBOOLE_1:9;
then union F c= (Ball x1,r1) \/ (Ball x2,r2) by A13, XBOOLE_1:1;
hence union F c= Ball x,r by A16, XBOOLE_1:1; :: thesis: verum

end;

A17: S₁[ 0 ]

proof

let F be Subset-Family of M; :: thesis: ( F is finite & F is being_ball-family implies for n being Nat st n = 0 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r )
assume that
F is finite and
F is being_ball-family ; :: thesis: for n being Nat st n = 0 holds
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r
let n be Nat; :: thesis: ( n = 0 implies for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r )
assume n = 0 ; :: thesis: for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r
then B18: Seg n = {} ;
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r

proof

consider x being Point of M;
let p be FinSequence; :: thesis: ( rng p = F & dom p = Seg n implies ex x being Point of M ex r being Real st union F c= Ball x,r )
assume A19: ( rng p = F & dom p = Seg n ) ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball x,r
take x ; :: thesis: ex r being Real st union F c= Ball x,r
take 0 ; :: thesis: union F c= Ball x,0
union F = {} by A19, B18, RELAT_1:65, ZFMISC_1:2;
hence union F c= Ball x,0 by XBOOLE_1:2; :: thesis: verum

end;

hence for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A17, A5);
hence for F being Subset-Family of M st F is finite & F is being_ball-family holds
for n being Nat
for p being FinSequence st rng p = F & dom p = Seg n holds
ex x being Point of M ex r being Real st union F c= Ball x,r ; :: thesis: verum

end;

ex n being Nat st dom p = Seg n by FINSEQ_1:def 2;
hence ex x being Point of M ex r being Real st union F c= Ball x,r by A2, A4, A3; :: thesis: verum