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;

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

end;

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

end;

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 #):],(1TopSp {0,1}) holds

( not f is continuous or not f is onto )

hence
[:A,B:] is connected
by A1, Th7; :: thesis: verum( 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 ; :: thesis: contradiction

A5: 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;

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;

end;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: contradiction

A5: 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 :: thesis: not f . [x0,y1] <> 1

reconsider X0 = {x0} as non empty Subset of S by ZFMISC_1:31;assume A24:
f . [x0,y1] <> 1
; :: thesis: contradiction

h is onto

end;h is onto

proof

hence
contradiction
by A21, A22, Th7; :: thesis: verum
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 object ; :: according to TARSKI:def 3 :: thesis: ( 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}) ; :: thesis: y in rng h

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( 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}) ; :: thesis: y in rng h

per cases
( y = 1 or y = 0 )
by A5, A26, TARSKI:def 2;

end;

suppose A27:
y = 1
; :: thesis: y in rng h

A28:
[x1,y1] in dom h
by A19, A25, ZFMISC_1:87;

then h . [x1,y1] = y by A10, A18, A19, A27, FUNCT_1:49;

hence y in rng h by A28, FUNCT_1:def 3; :: thesis: verum

end;then h . [x1,y1] = y by A10, A18, A19, A27, FUNCT_1:49;

hence y in rng h by A28, FUNCT_1:def 3; :: thesis: verum

suppose A29:
y = 0
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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 :: thesis: not f . [x0,y1] <> 0

hence
contradiction
by A23; :: thesis: verumassume A36:
f . [x0,y1] <> 0
; :: thesis: contradiction

g is onto

end;g is onto

proof

hence
contradiction
by A34, A35, Th7; :: thesis: verum
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 object ; :: according to TARSKI:def 3 :: thesis: ( 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}) ; :: thesis: y in rng g

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( 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}) ; :: thesis: y in rng g

per cases
( y = 0 or y = 1 )
by A5, A38, TARSKI:def 2;

end;

suppose A39:
y = 0
; :: thesis: y in rng g

A40:
[x0,y0] in dom g
by A32, A37, ZFMISC_1:87;

then g . [x0,y0] = y by A8, A14, A32, A39, FUNCT_1:49;

hence y in rng g by A40, FUNCT_1:def 3; :: thesis: verum

end;then g . [x0,y0] = y by A8, A14, A32, A39, FUNCT_1:49;

hence y in rng g by A40, FUNCT_1:def 3; :: thesis: verum

suppose A41:
y = 1
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum