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 A1: ( F is finite & F is being_ball-family ) ; :: thesis: ex x being Point of M ex r being Real st union F c= Ball x,r
A2: 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;
A3: 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 ( F is finite & 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 A4: 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
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

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 A5: union F = {} by A4, FINSEQ_1:4, RELAT_1:65, ZFMISC_1:2;
consider x being Point of M;
take x ; :: thesis: ex r being Real st union F c= Ball x,r
take 0 ; :: thesis: union F c= Ball x,0
thus union F c= Ball x,0 by A5, 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;

A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: 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 A8: ( F is finite & 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 A9: 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
A10: ( F1 is finite & F1 is being_ball-family & 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 A8, A9, Th2;
consider x2 being Point of M such that
A11: ex r2 being Real st union F c= (union F1) \/ (Ball x2,r2) by A10;
consider r2 being Real such that
A12: union F c= (union F1) \/ (Ball x2,r2) by A11;
consider x1 being Point of M such that
A13: ex r being Real st union F1 c= Ball x1,r by A7, A10;
consider r1 being Real such that
A14: union F1 c= Ball x1,r1 by A13;
A15: (union F1) \/ (Ball x2,r2) c= (Ball x1,r1) \/ (Ball x2,r2) by A14, XBOOLE_1:9;
consider x being Point of M such that
A16: ex r being Real st (Ball x1,r1) \/ (Ball x2,r2) c= Ball x,r by Th1;
consider r being Real such that
A17: (Ball x1,r1) \/ (Ball x2,r2) c= Ball x,r by A16;
take x ; :: thesis: ex r being Real st union F c= Ball x,r
take r ; :: thesis: union F c= Ball x,r
union F c= (Ball x1,r1) \/ (Ball x2,r2) by A12, A15, XBOOLE_1:1;
hence union F c= Ball x,r by A17, XBOOLE_1:1; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A6);
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;

consider p being FinSequence such that
A18: rng p = F by A1, FINSEQ_1:73;
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 A1, A2, A18; :: thesis: verum