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 ) )
set J = 1TopSp {0 ,1};
set X = {0 };
set Y = {1};
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;
A6: the carrier of T = (f " X) \/ (f " Y) by A1, Th4;
[#] (1TopSp {0 ,1}) <> {} ;
then A7: ( f " X is open & f " Y is open ) by A4, TOPS_2:55;
rng f = the carrier of (1TopSp {0 ,1}) by A5, FUNCT_2:def 3;
then A8: ( f " X <> {} T & f " Y <> {} T ) by RELAT_1:174;
f " X misses f " Y by FUNCT_1:141, ZFMISC_1:17;
hence contradiction by A2, A3, A6, A7, A8, CONNSP_1:12; :: thesis: verum

end;

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

end;

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

end;

A22: 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 A23: x in f " Y ; :: thesis: x in B
then ( x in dom f & f . x in Y ) by FUNCT_1:def 13;
then f . x = 1 by TARSKI:def 1;
then not S₁[x] by A17;
hence x in B by A10, A23, 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 A24: x in B ; :: thesis: x in f " Y
then not x in A by A15, XBOOLE_0:3;
then f . x = 1 by A17, A24;
then f . x in Y by TARSKI:def 1;
hence x in f " Y by A18, A24, FUNCT_1:def 13; :: thesis: verum

end;

A25: 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 A26: y in the carrier of (1TopSp {0 ,1}) ; :: thesis: y in rng f

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

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

consider x being set such that
A28: x in f " X by A11, A19, XBOOLE_0:def 1;
A29: ( x in dom f & f . x in X ) by A28, FUNCT_1:def 13;
then f . x = 0 by TARSKI:def 1;
hence y in rng f by A27, A29, FUNCT_1:def 5; :: thesis: verum

end;

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

consider x being set such that
A31: x in f " Y by A12, A22, XBOOLE_0:def 1;
A32: ( x in dom f & f . x in Y ) by A31, FUNCT_1:def 13;
then f . x = 1 by TARSKI:def 1;
hence y in rng f by A30, A32, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

then A33: f is onto by FUNCT_2:def 3;
A34: f " ({} (1TopSp {0 ,1})) = {} T by RELAT_1:171;
A35: [#] (1TopSp {0 ,1}) <> {} ;
f " ([#] (1TopSp {0 ,1})) = [#] T by A18, A25, RELAT_1:169;
then for P being Subset of (1TopSp {0 ,1}) st P is open holds
f " P is open by A1, A13, A14, A19, A22, A34, ZFMISC_1:42;
then f is continuous by A35, TOPS_2:55;
hence contradiction by A9, A33; :: thesis: verum