defpred S1[ Real, Real, set ] means ex c being Element of REAL 2 st
( c = $3 & $3 = <*$1,$2*> );
let A, B be compact Subset of REAL; :: thesis: product ((1,2) --> (A,B)) is compact Subset of (TOP-REAL 2)
reconsider X = product ((1,2) --> (A,B)) as Subset of (TOP-REAL 2) by Th20;
reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:17;
A1: the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22;
A2: for x, y being Element of REAL ex u being Element of REAL 2 st S1[x,y,u]
proof
let x, y be Element of REAL ; :: thesis: ex u being Element of REAL 2 st S1[x,y,u]
take <*x,y*> ; :: thesis: ( <*x,y*> is Element of REAL 2 & S1[x,y,<*x,y*>] )
thus <*x,y*> is Element of REAL 2 by FINSEQ_2:137; :: thesis: S1[x,y,<*x,y*>]
<*x,y*> in 2 -tuples_on REAL by FINSEQ_2:137;
hence S1[x,y,<*x,y*>] ; :: thesis: verum
end;
consider h being Function of [:REAL,REAL:],(REAL 2) such that
A3: for x, y being Element of REAL holds S1[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:] by BORSUK_1:def 2;
then reconsider h = h as Function of [:R^1,R^1:],(TOP-REAL 2) by A1, TOPMETR:17;
A4: for x, y being Real holds h . [x,y] = <*x,y*>
proof
let x, y be Real; :: thesis: h . [x,y] = <*x,y*>
( x in REAL & y in REAL ) by XREAL_0:def 1;
then S1[x,y,h . (x,y)] by A3;
hence h . [x,y] = <*x,y*> ; :: thesis: verum
end;
then A5: h is being_homeomorphism by Th69;
A6: B1 is compact by JORDAN5A:25;
A1 is compact by JORDAN5A:25;
then A7: [:A1,B1:] is compact by A6, BORSUK_3:23;
h .: [:A1,B1:] = X by A4, Th68;
hence product ((1,2) --> (A,B)) is compact Subset of (TOP-REAL 2) by A7, A5, WEIERSTR:8; :: thesis: verum