set X = {0};
set Y = {1};
set J = 1TopSp {0,1};
let T be non empty TopSpace; :: thesis: ( T is connected iff for f being Function of T,(1TopSp {0,1}) holds
( not f is continuous or not f is onto ) )
A1: the carrier of (1TopSp {0,1}) = {0,1} by PCOMPS_1:8;
then reconsider X = {0}, Y = {1} as non empty open Subset of (1TopSp {0,1}) by TDLAT_3:17, ZFMISC_1:12;
A2: [#] T = the carrier of T ;
thus ( T is connected implies for f being Function of T,(1TopSp {0,1}) holds
( not f is continuous or not f is onto ) ) :: thesis: ( ( for f being Function of T,(1TopSp {0,1}) holds
( not f is continuous or not f is onto ) ) implies T is connected )

proof

assume A3: T is connected ; :: thesis: for f being Function of T,(1TopSp {0,1}) holds
( not f is continuous or not f is onto )
given f being Function of T,(1TopSp {0,1}) such that A4: f is continuous and
A5: f is onto ; :: thesis: contradiction
set A = f " X;
set B = f " Y;
rng f = the carrier of (1TopSp {0,1}) by A5, FUNCT_2:def 3;
then A6: ( f " X <> {} T & f " Y <> {} T ) by RELAT_1:174;
A7: ( the carrier of T = (f " X) \/ (f " Y) & f " X misses f " Y ) by A1, Th4, FUNCT_1:141, ZFMISC_1:17;
[#] (1TopSp {0,1}) <> {} ;
then ( f " X is open & f " Y is open ) by A4, TOPS_2:55;
hence contradiction by A2, A3, A6, A7, CONNSP_1:12; :: thesis: verum

end;

reconsider j0 = 0 , j1 = 1 as Element of (1TopSp {0,1}) by A1, TARSKI:def 2;
assume A8: for f being Function of T,(1TopSp {0,1}) holds
( not f is continuous or not f is onto ) ; :: thesis: T is connected
deffunc H₁( set ) -> Element of (1TopSp {0,1}) = j1;
deffunc H₂( set ) -> Element of (1TopSp {0,1}) = j0;
assume not T is connected ; :: thesis: contradiction
then consider A, B being Subset of T such that
A9: [#] T = A \/ B and
A10: A <> {} T and
A11: B <> {} T and
A12: ( A is open & B is open ) and
A13: A misses B by CONNSP_1:12;
defpred S₁[ set ] means $1 in A;
A14: for x being set st x in the carrier of T holds
( ( S₁[x] implies H₂(x) in the carrier of (1TopSp {0,1}) ) & ( not S₁[x] implies H₁(x) in the carrier of (1TopSp {0,1}) ) ) ;
consider f being Function of the carrier of T, the carrier of (1TopSp {0,1}) such that
A15: for x being set st x in the carrier of T holds
( ( S₁[x] implies f . x = H₂(x) ) & ( not S₁[x] implies f . x = H₁(x) ) ) from FUNCT_2:sch 5(A14);
reconsider f = f as Function of T,(1TopSp {0,1}) ;
A16: dom f = the carrier of T by FUNCT_2:def 1;
A17: f " Y = B

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: B c= f " Y

let x be set ; :: thesis: ( x in f " Y implies x in B )
assume A18: x in f " Y ; :: thesis: x in B
then f . x in Y by FUNCT_1:def 13;
then f . x = 1 by TARSKI:def 1;
then not S₁[x] by A15;
hence x in B by A9, A18, XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in f " Y )
assume A19: x in B ; :: thesis: x in f " Y
then not x in A by A13, XBOOLE_0:3;
then f . x = 1 by A15, A19;
then f . x in Y by TARSKI:def 1;
hence x in f " Y by A16, A19, FUNCT_1:def 13; :: thesis: verum

end;

A20: f " X = A

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A c= f " X

let x be set ; :: thesis: ( x in f " X implies x in A )
assume A21: x in f " X ; :: thesis: x in A
then f . x in X by FUNCT_1:def 13;
then f . x = 0 by TARSKI:def 1;
hence x in A by A15, A21; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in f " X )
assume A22: x in A ; :: thesis: x in f " X
then f . x = 0 by A15;
then f . x in X by TARSKI:def 1;
hence x in f " X by A16, A22, FUNCT_1:def 13; :: thesis: verum

end;

A23: rng f = the carrier of (1TopSp {0,1})

proof

thus rng f c= the carrier of (1TopSp {0,1}) ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of (1TopSp {0,1}) c= rng f
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of (1TopSp {0,1}) or y in rng f )
assume A24: y in the carrier of (1TopSp {0,1}) ; :: thesis: y in rng f

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

suppose A25: y = 0 ; :: thesis: y in rng f

consider x being set such that
A26: x in f " X by A10, A20, XBOOLE_0:def 1;
f . x in X by A26, FUNCT_1:def 13;
then A27: f . x = 0 by TARSKI:def 1;
x in dom f by A26, FUNCT_1:def 13;
hence y in rng f by A25, A27, FUNCT_1:def 5; :: thesis: verum

end;

suppose A28: y = 1 ; :: thesis: y in rng f

consider x being set such that
A29: x in f " Y by A11, A17, XBOOLE_0:def 1;
f . x in Y by A29, FUNCT_1:def 13;
then A30: f . x = 1 by TARSKI:def 1;
x in dom f by A29, FUNCT_1:def 13;
hence y in rng f by A28, A30, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

then ( f " ({} (1TopSp {0,1})) = {} T & f " ([#] (1TopSp {0,1})) = [#] T ) by A16, RELAT_1:169, RELAT_1:171;
then ( [#] (1TopSp {0,1}) <> {} & ( for P being Subset of (1TopSp {0,1}) st P is open holds
f " P is open ) ) by A1, A12, A20, A17, ZFMISC_1:42;
then A31: f is continuous by TOPS_2:55;
f is onto by A23, FUNCT_2:def 3;
hence contradiction by A8, A31; :: thesis: verum