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; verum