consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A1: ( P1 is being_S-P_arc & P2 is being_S-P_arc & R^2-unit_square = P1 \/ P2 ) by TOPREAL1:34;
consider f being Function of I[01] ,((TOP-REAL 2) | P1) such that
A2: f is being_homeomorphism by A1, TOPREAL1:36;
A3: f is continuous by A2, TOPS_2:def 5;
consider f0 being Function of I[01] ,((TOP-REAL 2) | P2) such that
A4: f0 is being_homeomorphism by A1, TOPREAL1:36;
A5: f0 is continuous by A4, TOPS_2:def 5;
A6: I[01] is compact by HEINE:11, TOPMETR:27;
A7: rng f = [#] ((TOP-REAL 2) | P1) by A2, TOPS_2:def 5;
reconsider P1 = P1 as non empty Subset of (TOP-REAL 2) ;
(TOP-REAL 2) | P1 is compact by A3, A6, A7, COMPTS_1:23;
then A8: P1 is compact by COMPTS_1:12;
A9: rng f0 = [#] ((TOP-REAL 2) | P2) by A4, TOPS_2:def 5;
reconsider P2 = P2 as non empty Subset of (TOP-REAL 2) ;
(TOP-REAL 2) | P2 is compact by A5, A6, A9, COMPTS_1:23;
then P2 is compact by COMPTS_1:12;
hence R^2-unit_square is compact by A1, A8, COMPTS_1:19; :: thesis: verum