set S = TopStruct(# the carrier of A,the topology of A #);
set T = TopStruct(# the carrier of B,the topology of B #);
A1:
TopStruct(# the carrier of [:A,B:],the topology of [:A,B:] #) = [:TopStruct(# the carrier of A,the topology of A #),TopStruct(# the carrier of B,the topology of B #):]
by Th14;
per cases
( not [:TopStruct(# the carrier of A,the topology of A #),TopStruct(# the carrier of B,the topology of B #):] is empty or [:TopStruct(# the carrier of A,the topology of A #),TopStruct(# the carrier of B,the topology of B #):] is empty )
;
suppose A2:
not
[:TopStruct(# the carrier of A,the topology of A #),TopStruct(# the carrier of B,the topology of B #):] is
empty
;
:: thesis: [:A,B:] is connected now set J =
1TopSp {0 ,1};
given f being
Function of
[:TopStruct(# the carrier of A,the topology of A #),TopStruct(# the carrier of B,the topology of B #):],
(1TopSp {0 ,1}) such that A3:
f is
continuous
and A4:
f is
onto
;
:: thesis: contradictionA5:
the
carrier of
(1TopSp {0 ,1}) = {0 ,1}
by PCOMPS_1:8;
then reconsider j0 =
0 ,
j1 = 1 as
Element of
(1TopSp {0 ,1}) by TARSKI:def 2;
A6:
dom f = the
carrier of
[:TopStruct(# the carrier of A,the topology of A #),TopStruct(# the carrier of B,the topology of B #):]
by FUNCT_2:def 1;
A7:
the
carrier of
[:TopStruct(# the carrier of A,the topology of A #),TopStruct(# the carrier of B,the topology of B #):] = [:the carrier of TopStruct(# the carrier of A,the topology of A #),the carrier of TopStruct(# the carrier of B,the topology of B #):]
by BORSUK_1:def 5;
A8:
rng f = the
carrier of
(1TopSp {0 ,1})
by A4, FUNCT_2:def 3;
then consider xy0 being
set such that A9:
xy0 in dom f
and A10:
f . xy0 = j0
by FUNCT_1:def 5;
consider x0,
y0 being
set such that A11:
x0 in the
carrier of
TopStruct(# the
carrier of
A,the
topology of
A #)
and A12:
y0 in the
carrier of
TopStruct(# the
carrier of
B,the
topology of
B #)
and A13:
xy0 = [x0,y0]
by A7, A9, ZFMISC_1:def 2;
consider xy1 being
set such that A14:
xy1 in dom f
and A15:
f . xy1 = j1
by A8, FUNCT_1:def 5;
consider x1,
y1 being
set such that A16:
x1 in the
carrier of
TopStruct(# the
carrier of
A,the
topology of
A #)
and A17:
y1 in the
carrier of
TopStruct(# the
carrier of
B,the
topology of
B #)
and A18:
xy1 = [x1,y1]
by A7, A14, ZFMISC_1:def 2;
reconsider x0 =
x0,
x1 =
x1 as
Point of
TopStruct(# the
carrier of
A,the
topology of
A #)
by A11, A16;
reconsider y0 =
y0,
y1 =
y1 as
Point of
TopStruct(# the
carrier of
B,the
topology of
B #)
by A12, A17;
reconsider S =
TopStruct(# the
carrier of
A,the
topology of
A #),
T =
TopStruct(# the
carrier of
B,the
topology of
B #) as non
empty TopSpace by A2;
reconsider X0 =
{x0} as non
empty Subset of
S by ZFMISC_1:37;
reconsider Y1 =
{y1} as non
empty Subset of
T by ZFMISC_1:37;
T,
[:(S | X0),T:] are_homeomorphic
by BORSUK_3:15;
then A19:
[:(S | X0),T:] is
connected
by TOPREAL6:25;
S,
[:(T | Y1),S:] are_homeomorphic
by BORSUK_3:15;
then
[:(T | Y1),S:] is
connected
by TOPREAL6:25;
then A20:
[:S,(T | Y1):] is
connected
by TOPREAL6:25, YELLOW12:44;
set g =
f | [:X0,([#] T):];
A21:
dom (f | [:X0,([#] T):]) = [:X0,([#] T):]
by A6, RELAT_1:91;
the
carrier of
[:(S | X0),T:] = [:the carrier of (S | X0),the carrier of T:]
by BORSUK_1:def 5;
then A22:
dom (f | [:X0,([#] T):]) = the
carrier of
[:(S | X0),T:]
by A21, PRE_TOPC:29;
rng (f | [:X0,([#] T):]) c= the
carrier of
(1TopSp {0 ,1})
;
then reconsider g =
f | [:X0,([#] T):] as
Function of
[:(S | X0),T:],
(1TopSp {0 ,1}) by A22, FUNCT_2:4;
[:(S | X0),T:] =
[:(S | X0),(T | ([#] T)):]
by TSEP_1:3
.=
[:S,T:] | [:X0,([#] T):]
by BORSUK_3:26
;
then A23:
g is
continuous
by A3, TOPMETR:10;
set h =
f | [:([#] S),Y1:];
A24:
dom (f | [:([#] S),Y1:]) = [:([#] S),Y1:]
by A6, RELAT_1:91;
the
carrier of
[:S,(T | Y1):] = [:the carrier of S,the carrier of (T | Y1):]
by BORSUK_1:def 5;
then A25:
dom (f | [:([#] S),Y1:]) = the
carrier of
[:S,(T | Y1):]
by A24, PRE_TOPC:29;
rng (f | [:([#] S),Y1:]) c= the
carrier of
(1TopSp {0 ,1})
;
then reconsider h =
f | [:([#] S),Y1:] as
Function of
[:S,(T | Y1):],
(1TopSp {0 ,1}) by A25, FUNCT_2:4;
[:S,(T | Y1):] =
[:(S | ([#] S)),(T | Y1):]
by TSEP_1:3
.=
[:S,T:] | [:([#] S),Y1:]
by BORSUK_3:26
;
then A26:
h is
continuous
by A3, TOPMETR:10;
A27:
now assume A28:
f . [x0,y1] <> 0
;
:: thesis: contradiction
g is
onto
proof
thus
rng g c= the
carrier of
(1TopSp {0 ,1})
;
:: according to XBOOLE_0:def 10,
FUNCT_2:def 3 :: thesis: the carrier of (1TopSp {0 ,1}) c= rng g
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (1TopSp {0 ,1}) or y in rng g )
assume A29:
y in the
carrier of
(1TopSp {0 ,1})
;
:: thesis: y in rng g
A30:
x0 in X0
by TARSKI:def 1;
per cases
( y = 0 or y = 1 )
by A5, A29, TARSKI:def 2;
suppose A33:
y = 1
;
:: thesis: y in rng g
[x0,y1] in dom f
by A6, A7, A11, A17, ZFMISC_1:106;
then A34:
f . [x0,y1] in rng f
by FUNCT_1:def 5;
A35:
[x0,y1] in dom g
by A21, A30, ZFMISC_1:106;
then g . [x0,y1] =
f . [x0,y1]
by A21, FUNCT_1:72
.=
y
by A5, A28, A33, A34, TARSKI:def 2
;
hence
y in rng g
by A35, FUNCT_1:def 5;
:: thesis: verum end;
end; hence
contradiction
by A19, A23, Th8;
:: thesis: verum end; now assume A36:
f . [x0,y1] <> 1
;
:: thesis: contradiction
h is
onto
proof
thus
rng h c= the
carrier of
(1TopSp {0 ,1})
;
:: according to XBOOLE_0:def 10,
FUNCT_2:def 3 :: thesis: the carrier of (1TopSp {0 ,1}) c= rng h
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (1TopSp {0 ,1}) or y in rng h )
assume A37:
y in the
carrier of
(1TopSp {0 ,1})
;
:: thesis: y in rng h
A38:
y1 in Y1
by TARSKI:def 1;
per cases
( y = 1 or y = 0 )
by A5, A37, TARSKI:def 2;
suppose A41:
y = 0
;
:: thesis: y in rng h
[x0,y1] in dom f
by A6, A7, A11, A17, ZFMISC_1:106;
then A42:
f . [x0,y1] in rng f
by FUNCT_1:def 5;
A43:
[x0,y1] in dom h
by A24, A38, ZFMISC_1:106;
then h . [x0,y1] =
f . [x0,y1]
by A24, FUNCT_1:72
.=
y
by A5, A36, A41, A42, TARSKI:def 2
;
hence
y in rng h
by A43, FUNCT_1:def 5;
:: thesis: verum end;
end; hence
contradiction
by A20, A26, Th8;
:: thesis: verum end; hence
contradiction
by A27;
:: thesis: verum end; hence
[:A,B:] is
connected
by A1, A2, Th8;
:: thesis: verum