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 Th13;
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
;
[:A,B:] is connected now for 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}) holds
( not f is continuous or not f is onto )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
;
contradictionA5:
the
carrier of
(1TopSp {0,1}) = {0,1}
by PCOMPS_1:5;
then reconsider j0 =
0 ,
j1 = 1 as
Element of
(1TopSp {0,1}) by TARSKI:def 2;
A6:
rng f = the
carrier of
(1TopSp {0,1})
by A4;
then consider xy0 being
object such that A7:
xy0 in dom f
and A8:
f . xy0 = j0
by FUNCT_1:def 3;
consider xy1 being
object such that A9:
xy1 in dom f
and A10:
f . xy1 = j1
by A6, FUNCT_1:def 3;
A11:
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 2;
then consider x0,
y0 being
object such that A12:
x0 in the
carrier of
TopStruct(# the
carrier of
A, the
topology of
A #)
and A13:
y0 in the
carrier of
TopStruct(# the
carrier of
B, the
topology of
B #)
and A14:
xy0 = [x0,y0]
by A7, ZFMISC_1:def 2;
A15:
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;
consider x1,
y1 being
object 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 A11, A9, ZFMISC_1:def 2;
reconsider y0 =
y0,
y1 =
y1 as
Point of
TopStruct(# the
carrier of
B, the
topology of
B #)
by A13, A17;
reconsider x0 =
x0,
x1 =
x1 as
Point of
TopStruct(# the
carrier of
A, the
topology of
A #)
by A12, A16;
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 Y1 =
{y1} as non
empty Subset of
T by ZFMISC_1:31;
set h =
f | [:([#] S),Y1:];
A19:
dom (f | [:([#] S),Y1:]) = [:([#] S),Y1:]
by A15, RELAT_1:62;
the
carrier of
[:S,(T | Y1):] = [: the carrier of S, the carrier of (T | Y1):]
by BORSUK_1:def 2;
then A20:
dom (f | [:([#] S),Y1:]) = the
carrier of
[:S,(T | Y1):]
by A19, PRE_TOPC:8;
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 A20, FUNCT_2:2;
S,
[:(T | Y1),S:] are_homeomorphic
by BORSUK_3:13;
then
[:(T | Y1),S:] is
connected
by TOPREAL6:19;
then A21:
[:S,(T | Y1):] is
connected
by TOPREAL6:19, YELLOW12:44;
[:S,(T | Y1):] =
[:(S | ([#] S)),(T | Y1):]
by TSEP_1:3
.=
[:S,T:] | [:([#] S),Y1:]
by BORSUK_3:22
;
then A22:
h is
continuous
by A3, TOPMETR:7;
A23:
now not f . [x0,y1] <> 1assume A24:
f . [x0,y1] <> 1
;
contradiction
h is
onto
proof
thus
rng h c= the
carrier of
(1TopSp {0,1})
;
XBOOLE_0:def 10,
FUNCT_2:def 3 the carrier of (1TopSp {0,1}) c= rng h
let y be
object ;
TARSKI:def 3 ( not y in the carrier of (1TopSp {0,1}) or y in rng h )
A25:
y1 in Y1
by TARSKI:def 1;
assume A26:
y in the
carrier of
(1TopSp {0,1})
;
y in rng h
per cases
( y = 1 or y = 0 )
by A5, A26, TARSKI:def 2;
suppose A29:
y = 0
;
y in rng h
[x0,y1] in dom f
by A15, A11, A12, A17, ZFMISC_1:87;
then A30:
f . [x0,y1] in rng f
by FUNCT_1:def 3;
A31:
[x0,y1] in dom h
by A19, A25, ZFMISC_1:87;
then h . [x0,y1] =
f . [x0,y1]
by A19, FUNCT_1:49
.=
y
by A5, A24, A29, A30, TARSKI:def 2
;
hence
y in rng h
by A31, FUNCT_1:def 3;
verum end;
end; hence
contradiction
by A21, A22, Th7;
verum end; reconsider X0 =
{x0} as non
empty Subset of
S by ZFMISC_1:31;
set g =
f | [:X0,([#] T):];
A32:
dom (f | [:X0,([#] T):]) = [:X0,([#] T):]
by A15, RELAT_1:62;
the
carrier of
[:(S | X0),T:] = [: the carrier of (S | X0), the carrier of T:]
by BORSUK_1:def 2;
then A33:
dom (f | [:X0,([#] T):]) = the
carrier of
[:(S | X0),T:]
by A32, PRE_TOPC:8;
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 A33, FUNCT_2:2;
T,
[:(S | X0),T:] are_homeomorphic
by BORSUK_3:13;
then A34:
[:(S | X0),T:] is
connected
by TOPREAL6:19;
[:(S | X0),T:] =
[:(S | X0),(T | ([#] T)):]
by TSEP_1:3
.=
[:S,T:] | [:X0,([#] T):]
by BORSUK_3:22
;
then A35:
g is
continuous
by A3, TOPMETR:7;
now not f . [x0,y1] <> 0 assume A36:
f . [x0,y1] <> 0
;
contradiction
g is
onto
proof
thus
rng g c= the
carrier of
(1TopSp {0,1})
;
XBOOLE_0:def 10,
FUNCT_2:def 3 the carrier of (1TopSp {0,1}) c= rng g
let y be
object ;
TARSKI:def 3 ( not y in the carrier of (1TopSp {0,1}) or y in rng g )
A37:
x0 in X0
by TARSKI:def 1;
assume A38:
y in the
carrier of
(1TopSp {0,1})
;
y in rng g
per cases
( y = 0 or y = 1 )
by A5, A38, TARSKI:def 2;
suppose A41:
y = 1
;
y in rng g
[x0,y1] in dom f
by A15, A11, A12, A17, ZFMISC_1:87;
then A42:
f . [x0,y1] in rng f
by FUNCT_1:def 3;
A43:
[x0,y1] in dom g
by A32, A37, ZFMISC_1:87;
then g . [x0,y1] =
f . [x0,y1]
by A32, FUNCT_1:49
.=
y
by A5, A36, A41, A42, TARSKI:def 2
;
hence
y in rng g
by A43, FUNCT_1:def 3;
verum end;
end; hence
contradiction
by A34, A35, Th7;
verum end; hence
contradiction
by A23;
verum end; hence
[:A,B:] is
connected
by A1, Th7;
verum