let A, B be compact Subset of REAL; A /\ B is compact
let s1 be Real_Sequence; RCOMP_1:def 3 ( not proj2 s1 c= A /\ B or ex b1 being Element of bool [:NAT,REAL:] st
( b1 is subsequence of s1 & b1 is convergent & lim b1 in A /\ B ) )
assume A1:
rng s1 c= A /\ B
; ex b1 being Element of bool [:NAT,REAL:] st
( b1 is subsequence of s1 & b1 is convergent & lim b1 in A /\ B )
A2:
A /\ B c= B
by XBOOLE_1:17;
A /\ B c= A
by XBOOLE_1:17;
then
rng s1 c= A
by A1;
then consider s2 being Real_Sequence such that
A3:
s2 is subsequence of s1
and
A4:
s2 is convergent
and
A5:
lim s2 in A
by RCOMP_1:def 3;
rng s2 c= rng s1
by A3, VALUED_0:21;
then
rng s2 c= A /\ B
by A1;
then
rng s2 c= B
by A2;
then consider s3 being Real_Sequence such that
A6:
s3 is subsequence of s2
and
A7:
s3 is convergent
and
A8:
lim s3 in B
by RCOMP_1:def 3;
take
s3
; ( s3 is subsequence of s1 & s3 is convergent & lim s3 in A /\ B )
thus
s3 is subsequence of s1
by A3, A6, VALUED_0:20; ( s3 is convergent & lim s3 in A /\ B )
thus
s3 is convergent
by A7; lim s3 in A /\ B
lim s3 = lim s2
by A4, A6, SEQ_4:17;
hence
lim s3 in A /\ B
by A5, A8, XBOOLE_0:def 4; verum