let A, B be compact Subset of REAL ; :: thesis: product (1,2 --> A,B) is compact Subset of (TOP-REAL 2)
reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:24;
( A1 is compact & B1 is compact ) by Th81;
then A1: [:A1,B1:] is compact by BORSUK_3:27;
reconsider X = product (1,2 --> A,B) as Subset of (TOP-REAL 2) by Th30;
defpred S₁[ Element of REAL , Element of REAL , set ] means ex c being Element of REAL 2 st
( c = $3 & $3 = <*$1,$2*> );
A2: for x, y being Element of REAL ex u being Element of REAL 2 st S₁[x,y,u]

proof

let x, y be Element of REAL ; :: thesis: ex u being Element of REAL 2 st S₁[x,y,u]
take <*x,y*> ; :: thesis: ( <*x,y*> is Element of REAL 2 & S₁[x,y,<*x,y*>] )
A3: <*x,y*> in 2 -tuples_on REAL by CATALG_1:10;
thus <*x,y*> is Element of REAL 2 by CATALG_1:10; :: thesis: S₁[x,y,<*x,y*>]
thus S₁[x,y,<*x,y*>] by A3; :: thesis: verum

end;

consider h being Function of [:REAL ,REAL :],(REAL 2) such that
A4: for x, y being Element of REAL holds S₁[x,y,h . x,y] from BINOP_1:sch 3(A2);
( the carrier of [:R^1 ,R^1 :] = [:the carrier of R^1 ,the carrier of R^1 :] & the carrier of R^1 = REAL & the carrier of (TOP-REAL 2) = REAL 2 ) by BORSUK_1:def 5, EUCLID:25, TOPMETR:24;
then reconsider h = h as Function of [:R^1 ,R^1 :],(TOP-REAL 2) ;
A5: for x, y being Real holds h . [x,y] = <*x,y*>

proof

let x, y be Real; :: thesis: h . [x,y] = <*x,y*>
S₁[x,y,h . x,y] by A4;
hence h . [x,y] = <*x,y*> ; :: thesis: verum

end;

then A6: h .: [:A1,B1:] = X by Th84;
h is being_homeomorphism by A5, Th85;
then h is continuous ;
hence product (1,2 --> A,B) is compact Subset of (TOP-REAL 2) by A1, A6, WEIERSTR:14; :: thesis: verum