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 ; :: thesis: [:A,B:] is connected
now :: thesis: for f being Function of [:TopStruct(# the carrier of A, the topology of A #),TopStruct(# the carrier of B, the topology of B #):],() 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 #):],() such that A3: f is continuous and
A4: f is onto ; :: thesis: contradiction
A5: the carrier of () = {0,1} by PCOMPS_1:5;
then reconsider j0 = 0 , j1 = 1 as Element of () by TARSKI:def 2;
A6: rng f = the carrier of () 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 ;
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 ;
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 ;
reconsider y0 = y0, y1 = y1 as Point of TopStruct(# the carrier of B, the topology of B #) by ;
reconsider x0 = x0, x1 = x1 as Point of TopStruct(# the carrier of A, the topology of A #) by ;
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 ;
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 ;
rng (f | [:([#] S),Y1:]) c= the carrier of () ;
then reconsider h = f | [:([#] S),Y1:] as Function of [:S,(T | Y1):],() by ;
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 ;
[: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 ;
A23: now :: thesis: not f . [x0,y1] <> 1
assume A24: f . [x0,y1] <> 1 ; :: thesis: contradiction
h is onto
proof
thus rng h c= the carrier of () ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of () c= rng h
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of () or y in rng h )
A25: y1 in Y1 by TARSKI:def 1;
assume A26: y in the carrier of () ; :: thesis: y in rng h
per cases ( y = 1 or y = 0 ) by ;
suppose A27: y = 1 ; :: thesis: y in rng h
A28: [x1,y1] in dom h by ;
then h . [x1,y1] = y by ;
hence y in rng h by ; :: thesis: verum
end;
suppose A29: y = 0 ; :: thesis: y in rng h
[x0,y1] in dom f by ;
then A30: f . [x0,y1] in rng f by FUNCT_1:def 3;
A31: [x0,y1] in dom h by ;
then h . [x0,y1] = f . [x0,y1] by
.= y by ;
hence y in rng h by ; :: thesis: verum
end;
end;
end;
hence contradiction by A21, A22, Th7; :: thesis: 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 ;
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 ;
rng (f | [:X0,([#] T):]) c= the carrier of () ;
then reconsider g = f | [:X0,([#] T):] as Function of [:(S | X0),T:],() by ;
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 ;
now :: thesis: not f . [x0,y1] <> 0
assume A36: f . [x0,y1] <> 0 ; :: thesis: contradiction
g is onto
proof
thus rng g c= the carrier of () ; :: according to XBOOLE_0:def 10,FUNCT_2:def 3 :: thesis: the carrier of () c= rng g
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of () or y in rng g )
A37: x0 in X0 by TARSKI:def 1;
assume A38: y in the carrier of () ; :: thesis: y in rng g
per cases ( y = 0 or y = 1 ) by ;
suppose A39: y = 0 ; :: thesis: y in rng g
A40: [x0,y0] in dom g by ;
then g . [x0,y0] = y by ;
hence y in rng g by ; :: thesis: verum
end;
suppose A41: y = 1 ; :: thesis: y in rng g
[x0,y1] in dom f by ;
then A42: f . [x0,y1] in rng f by FUNCT_1:def 3;
A43: [x0,y1] in dom g by ;
then g . [x0,y1] = f . [x0,y1] by
.= y by ;
hence y in rng g by ; :: thesis: verum
end;
end;
end;
hence contradiction by A34, A35, Th7; :: thesis: verum
end;
hence contradiction by A23; :: thesis: verum
end;
hence [:A,B:] is connected by ; :: thesis: verum
end;
suppose [: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
hence [:A,B:] is connected by Th13; :: thesis: verum
end;
end;