let P, Q be RealNormSpace; :: thesis: for E being Subset of P
for F being Subset of Q st E is compact & F is compact holds
( [:E,F:] is Subset of [:P,Q:] & [:E,F:] is compact )
let E be Subset of P; :: thesis: for F being Subset of Q st E is compact & F is compact holds
( [:E,F:] is Subset of [:P,Q:] & [:E,F:] is compact )
let F be Subset of Q; :: thesis: ( E is compact & F is compact implies ( [:E,F:] is Subset of [:P,Q:] & [:E,F:] is compact ) )
assume A1: ( E is compact & F is compact ) ; :: thesis: ( [:E,F:] is Subset of [:P,Q:] & [:E,F:] is compact )
set S = [:P,Q:];
set X = [:E,F:];
reconsider X = [:E,F:] as Subset of [:P,Q:] ;
for s1 being sequence of [:P,Q:] st rng s1 c= X holds
ex s2 being sequence of [:P,Q:] st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X )

proof

let u1 be sequence of [:P,Q:]; :: thesis: ( rng u1 c= X implies ex s2 being sequence of [:P,Q:] st
( s2 is subsequence of u1 & s2 is convergent & lim s2 in X ) )
assume A2: rng u1 c= X ; :: thesis: ex s2 being sequence of [:P,Q:] st
( s2 is subsequence of u1 & s2 is convergent & lim s2 in X )
defpred S₁[ Nat, object ] means ex u being Point of [:P,Q:] ex x1 being Point of P ex x2 being Point of Q st
( u = u1 . $1 & u = [x1,x2] & $2 = x1 );
A3: for i being Element of NAT ex y being Element of the carrier of P st S₁[i,y]

proof

let i be Element of NAT ; :: thesis: ex y being Element of the carrier of P st S₁[i,y]
reconsider u = u1 . i as Point of [:P,Q:] ;
consider xx1 being Point of P, xx2 being Point of Q such that
A4: u = [xx1,xx2] by PRVECT_3:18;
reconsider xx1 = xx1 as Element of the carrier of P ;
take y = xx1; :: thesis: S₁[i,y]
thus S₁[i,y] by A4; :: thesis: verum

end;

consider s1 being Function of NAT, the carrier of P such that
A5: for i being Element of NAT holds S₁[i,s1 . i] from FUNCT_2:sch 3(A3);
defpred S₂[ Nat, object ] means ex u being Point of [:P,Q:] ex x1 being Point of P ex x2 being Point of Q st
( u = u1 . $1 & u = [x1,x2] & $2 = x2 );
A6: for i being Element of NAT ex y being Element of the carrier of Q st S₂[i,y]

proof

let i be Element of NAT ; :: thesis: ex y being Element of the carrier of Q st S₂[i,y]
reconsider u = u1 . i as Point of [:P,Q:] ;
consider xx1 being Point of P, xx2 being Point of Q such that
A7: u = [xx1,xx2] by PRVECT_3:18;
reconsider xx2 = xx2 as Element of the carrier of Q ;
take y = xx2; :: thesis: S₂[i,y]
thus S₂[i,y] by A7; :: thesis: verum

end;

consider t1 being Function of NAT, the carrier of Q such that
A8: for i being Element of NAT holds S₂[i,t1 . i] from FUNCT_2:sch 3(A6);
reconsider s1 = s1 as sequence of P ;
reconsider t1 = t1 as sequence of Q ;
A9: for i being Nat holds u1 . i = [(s1 . i),(t1 . i)]

proof

let i be Nat; :: thesis: u1 . i = [(s1 . i),(t1 . i)]
A10: i is Element of NAT by ORDINAL1:def 12;
then A11: ex u being Point of [:P,Q:] ex x1 being Point of P ex x2 being Point of Q st
( u = u1 . i & u = [x1,x2] & s1 . i = x1 ) by A5;
ex v being Point of [:P,Q:] ex y1 being Point of P ex y2 being Point of Q st
( v = u1 . i & v = [y1,y2] & t1 . i = y2 ) by A8, A10;
hence u1 . i = [(s1 . i),(t1 . i)] by A11, XTUPLE_0:1; :: thesis: verum

end;

now :: thesis: for z being object st z in rng s1 holds
z in E

let z be object ; :: thesis: ( z in rng s1 implies z in E )
assume z in rng s1 ; :: thesis: z in E
then consider i being Element of NAT such that
A12: ( i in dom s1 & z = s1 . i ) by PARTFUN1:3;
A13: i in NAT ;
consider u being Point of [:P,Q:], x1 being Point of P, x2 being Point of Q such that
A14: ( u = u1 . i & u = [x1,x2] & s1 . i = x1 ) by A5;
i in dom u1 by A13, FUNCT_2:def 1;
then u in X by A2, A14, FUNCT_1:3;
hence z in E by A14, A12, ZFMISC_1:87; :: thesis: verum

end;

then rng s1 c= E ;
then consider s2 being sequence of P such that
A15: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in E ) by A1;
consider N1 being increasing sequence of NAT such that
A16: s2 = s1 * N1 by A15, VALUED_0:def 17;

A17: now :: thesis: for z being object st z in rng t1 holds
z in F

let z be object ; :: thesis: ( z in rng t1 implies z in F )
assume z in rng t1 ; :: thesis: z in F
then consider i being Element of NAT such that
A18: ( i in dom t1 & z = t1 . i ) by PARTFUN1:3;
consider u being Point of [:P,Q:], x1 being Point of P, x2 being Point of Q such that
A19: ( u = u1 . i & u = [x1,x2] & t1 . i = x2 ) by A8;
i in NAT ;
then i in dom u1 by FUNCT_2:def 1;
then u in X by A2, A19, FUNCT_1:3;
hence z in F by A19, A18, ZFMISC_1:87; :: thesis: verum

end;

reconsider t2 = t1 * N1 as sequence of Q ;
rng t2 c= rng t1 by VALUED_0:21;
then rng t2 c= F by A17;
then consider t3 being sequence of Q such that
A20: ( t3 is subsequence of t2 & t3 is convergent & lim t3 in F ) by A1;
consider N2 being increasing sequence of NAT such that
A21: t3 = t2 * N2 by A20, VALUED_0:def 17;
reconsider s3 = (s1 * N1) * N2 as sequence of P ;
A22: ( s3 is convergent & lim s3 = lim s2 ) by A15, A16, LOPBAN_3:7, LOPBAN_3:8;
reconsider u2 = u1 * N1 as sequence of [:P,Q:] ;
reconsider u3 = u2 * N2 as sequence of [:P,Q:] ;
take u3 ; :: thesis: ( u3 is subsequence of u1 & u3 is convergent & lim u3 in X )
thus u3 is subsequence of u1 by VALUED_0:20; :: thesis: ( u3 is convergent & lim u3 in X )
A23: for i being Nat holds u3 . i = [(s3 . i),(t3 . i)]

proof

let i be Nat; :: thesis: u3 . i = [(s3 . i),(t3 . i)]
i in NAT by ORDINAL1:def 12;
then A24: i in dom N2 by FUNCT_2:def 1;
N2 . i in NAT by ORDINAL1:def 12;
then A25: N2 . i in dom N1 by FUNCT_2:def 1;
u3 . i = u2 . (N2 . i) by A24, FUNCT_1:13;
then u3 . i = u1 . (N1 . (N2 . i)) by A25, FUNCT_1:13;
then A26: u3 . i = [(s1 . (N1 . (N2 . i))),(t1 . (N1 . (N2 . i)))] by A9;
s3 . i = (s1 * N1) . (N2 . i) by A24, FUNCT_1:13;
then A27: s3 . i = s1 . (N1 . (N2 . i)) by A25, FUNCT_1:13;
t3 . i = (t1 * N1) . (N2 . i) by A21, A24, FUNCT_1:13;
hence u3 . i = [(s3 . i),(t3 . i)] by A26, A27, A25, FUNCT_1:13; :: thesis: verum

end;

reconsider v3 = [(lim s3),(lim t3)] as Point of [:P,Q:] ;
A28: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((u3 . n) - v3).|| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((u3 . n) - v3).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((u3 . n) - v3).|| < r
then A29: 0 < r / 2 by XREAL_1:215;
then consider m1 being Nat such that
A30: for n being Nat st m1 <= n holds
||.((s3 . n) - (lim s3)).|| < r / 2 by A22, NORMSP_1:def 7;
consider m2 being Nat such that
A31: for n being Nat st m2 <= n holds
||.((t3 . n) - (lim t3)).|| < r / 2 by A20, NORMSP_1:def 7, A29;
reconsider m = max (m1,m2) as Nat by XXREAL_0:16;
A32: ( m1 <= m & m2 <= m ) by XXREAL_0:25;
take m ; :: thesis: for n being Nat st m <= n holds
||.((u3 . n) - v3).|| < r
let n be Nat; :: thesis: ( m <= n implies ||.((u3 . n) - v3).|| < r )
assume A33: m <= n ; :: thesis: ||.((u3 . n) - v3).|| < r
then m1 <= n by A32, XXREAL_0:2;
then A34: ||.((s3 . n) - (lim s3)).|| < r / 2 by A30;
m2 <= n by A32, A33, XXREAL_0:2;
then A35: ||.((t3 . n) - (lim t3)).|| < r / 2 by A31;
A36: u3 . n = [(s3 . n),(t3 . n)] by A23;
set x1 = s3 . n;
set y1 = t3 . n;
set x2 = lim s3;
set y2 = lim t3;
reconsider z1 = [(s3 . n),(t3 . n)], z2 = [(lim s3),(lim t3)] as Point of [:P,Q:] ;
- z2 = [(- (lim s3)),(- (lim t3))] by PRVECT_3:18;
then z1 - z2 = [((s3 . n) - (lim s3)),((t3 . n) - (lim t3))] by PRVECT_3:18;
then A37: ||.(z1 - z2).|| <= ||.((s3 . n) - (lim s3)).|| + ||.((t3 . n) - (lim t3)).|| by NDIFF_9:6;
||.((s3 . n) - (lim s3)).|| + ||.((t3 . n) - (lim t3)).|| < (r / 2) + (r / 2) by A34, A35, XREAL_1:8;
hence ||.((u3 . n) - v3).|| < r by A36, A37, XXREAL_0:2; :: thesis: verum

end;

then u3 is convergent ;
then lim u3 = [(lim s3),(lim t3)] by A28, NORMSP_1:def 7;
hence ( u3 is convergent & lim u3 in X ) by A15, A28, A20, A22, ZFMISC_1:87; :: thesis: verum

end;

hence ( [:E,F:] is Subset of [:P,Q:] & [:E,F:] is compact ) ; :: thesis: verum