A1:
I[01] is compact
by HEINE:4, TOPMETR:20;

consider P1, P2 being non empty Subset of (TOP-REAL 2) such that

A2: P1 is being_S-P_arc and

A3: P2 is being_S-P_arc and

A4: R^2-unit_square = P1 \/ P2 by TOPREAL1:27;

consider f being Function of I[01],((TOP-REAL 2) | P1) such that

A5: f is being_homeomorphism by A2, TOPREAL1:29;

A6: rng f = [#] ((TOP-REAL 2) | P1) by A5;

consider f0 being Function of I[01],((TOP-REAL 2) | P2) such that

A7: f0 is being_homeomorphism by A3, TOPREAL1:29;

A8: rng f0 = [#] ((TOP-REAL 2) | P2) by A7;

reconsider P2 = P2 as non empty Subset of (TOP-REAL 2) ;

f0 is continuous by A7;

then (TOP-REAL 2) | P2 is compact by A1, A8, COMPTS_1:14;

then A9: P2 is compact by COMPTS_1:3;

reconsider P1 = P1 as non empty Subset of (TOP-REAL 2) ;

f is continuous by A5;

then (TOP-REAL 2) | P1 is compact by A1, A6, COMPTS_1:14;

then P1 is compact by COMPTS_1:3;

hence R^2-unit_square is compact by A4, A9, COMPTS_1:10; :: thesis: verum

consider P1, P2 being non empty Subset of (TOP-REAL 2) such that

A2: P1 is being_S-P_arc and

A3: P2 is being_S-P_arc and

A4: R^2-unit_square = P1 \/ P2 by TOPREAL1:27;

consider f being Function of I[01],((TOP-REAL 2) | P1) such that

A5: f is being_homeomorphism by A2, TOPREAL1:29;

A6: rng f = [#] ((TOP-REAL 2) | P1) by A5;

consider f0 being Function of I[01],((TOP-REAL 2) | P2) such that

A7: f0 is being_homeomorphism by A3, TOPREAL1:29;

A8: rng f0 = [#] ((TOP-REAL 2) | P2) by A7;

reconsider P2 = P2 as non empty Subset of (TOP-REAL 2) ;

f0 is continuous by A7;

then (TOP-REAL 2) | P2 is compact by A1, A8, COMPTS_1:14;

then A9: P2 is compact by COMPTS_1:3;

reconsider P1 = P1 as non empty Subset of (TOP-REAL 2) ;

f is continuous by A5;

then (TOP-REAL 2) | P1 is compact by A1, A6, COMPTS_1:14;

then P1 is compact by COMPTS_1:3;

hence R^2-unit_square is compact by A4, A9, COMPTS_1:10; :: thesis: verum