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:52;
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;
reconsider r = r as Real ;
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;
hence union F c= Ball (x,r) by A16; :: 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 A18: 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

set x = the 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 the Point of M ; :: thesis: ex r being Real st union F c= Ball ( the Point of M,r)
take 0 ; :: thesis: union F c= Ball ( the Point of M,0)
union F = {} by A19, A18, RELAT_1:42, ZFMISC_1:2;
hence union F c= Ball ( the Point of M,0) ; :: 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