:: TOPALG_3 semantic presentation

begin

set I = the carrier of I[01];

Lm1:  the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:]
by BORSUK_1:def_2;

reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15;

theorem :: TOPALG_3:1
for A, B, a, b being set
for f being Function of A,B st a in A & b in B holds
f +* (a .--> b) is Function of A,B
proof
let A, B, a, b be set ; ::_thesis: for f being Function of A,B st a in A & b in B holds
f +* (a .--> b) is Function of A,B
let f be Function of A,B; ::_thesis: ( a in A & b in B implies f +* (a .--> b) is Function of A,B )
assume that
A1: a in A and
A2: b in B ; ::_thesis: f +* (a .--> b) is Function of A,B
A3: {a} c= A by A1, ZFMISC_1:31;
set g = a .--> b;
set f1 = f +* (a .--> b);
 rng (a .--> b) = {b} by FUNCOP_1:8;
then  rng (a .--> b) c= B by A2, ZFMISC_1:31;
then A4: ( rng (f +* (a .--> b)) c= (rng f) \/ (rng (a .--> b)) & (rng f) \/ (rng (a .--> b)) c= B \/ B ) by FUNCT_4:17, XBOOLE_1:13;
dom (f +* (a .--> b)) = (dom f) \/ (dom (a .--> b)) by FUNCT_4:def_1
.= A \/ (dom (a .--> b)) by A2, FUNCT_2:def_1
.= A \/ {a} by FUNCOP_1:13
.= A by A3, XBOOLE_1:12 ;
hence  f +* (a .--> b) is Function of A,B by A4, FUNCT_2:2, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: TOPALG_3:2
for f being Function
for X, x being set st f | X is one-to-one & x in rng (f | X) holds
(f * ((f | X) ")) . x = x
proof
let f be Function; ::_thesis: for X, x being set st f | X is one-to-one & x in rng (f | X) holds
(f * ((f | X) ")) . x = x
let X, x be set ; ::_thesis: ( f | X is one-to-one & x in rng (f | X) implies (f * ((f | X) ")) . x = x )
set g = f | X;
assume that
A1: f | X is one-to-one and
A2: x in rng (f | X) ; ::_thesis: (f * ((f | X) ")) . x = x
consider a being set  such that
A3: a in dom (f | X) and
A4: (f | X) . a = x by A2, FUNCT_1:def_3;
 dom (f | X) = (dom f) /\ X by RELAT_1:61;
then A5: a in X by A3, XBOOLE_0:def_4;
 dom ((f | X) ") = rng (f | X) by A1, FUNCT_1:32;
hence (f * ((f | X) ")) . x = f . (((f | X) ") . x) by A2, FUNCT_1:13
.= f . a by A1, A3, A4, FUNCT_1:32
.= x by A4, A5, FUNCT_1:49 ;
::_thesis: verum
end;

theorem Th3: :: TOPALG_3:3
for X, a, b being set
for f being Function of X,{a,b} holds X = (f " {a}) \/ (f " {b})
proof
let X, a, b be set ; ::_thesis: for f being Function of X,{a,b} holds X = (f " {a}) \/ (f " {b})
let f be Function of X,{a,b}; ::_thesis: X = (f " {a}) \/ (f " {b})
thus X = f " {a,b} by FUNCT_2:40
.= f " ({a} \/ {b}) by ENUMSET1:1
.= (f " {a}) \/ (f " {b}) by RELAT_1:140 ; ::_thesis: verum
end;

theorem :: TOPALG_3:4
for S, T being non empty 1-sorted
for s being Point of S
for t being Point of T holds (S --> t) . s = t by FUNCOP_1:7;

theorem :: TOPALG_3:5
for T being non empty TopStruct
for t being Point of T
for A being Subset of T st A = {t} holds
Sspace t = T | A
proof
let T be non empty TopStruct ; ::_thesis: for t being Point of T
for A being Subset of T st A = {t} holds
Sspace t = T | A
let t be Point of T; ::_thesis: for A being Subset of T st A = {t} holds
Sspace t = T | A
let A be Subset of T; ::_thesis: ( A = {t} implies Sspace t = T | A )
assume A1: A = {t} ; ::_thesis: Sspace t = T | A
the carrier of (Sspace t) = {t} by TEX_2:def_2
.= [#] (T | A) by A1, PRE_TOPC:def_5
.= the carrier of (T | A) ;
hence  Sspace t = T | A by TSEP_1:5; ::_thesis: verum
end;

theorem Th6: :: TOPALG_3:6
for T being TopSpace
for A, B being Subset of T
for C, D being Subset of TopStruct(# the carrier of T, the topology of T #) st A = C & B = D holds
( A,B are_separated iff C,D are_separated )
proof
let T be TopSpace; ::_thesis: for A, B being Subset of T
for C, D being Subset of TopStruct(# the carrier of T, the topology of T #) st A = C & B = D holds
( A,B are_separated iff C,D are_separated )
let A, B be Subset of T; ::_thesis: for C, D being Subset of TopStruct(# the carrier of T, the topology of T #) st A = C & B = D holds
( A,B are_separated iff C,D are_separated )
let C, D be Subset of TopStruct(# the carrier of T, the topology of T #); ::_thesis: ( A = C & B = D implies ( A,B are_separated iff C,D are_separated ) )
assume A1: ( A = C & B = D ) ; ::_thesis: ( A,B are_separated iff C,D are_separated )
then A2: ( Cl A = Cl C & Cl B = Cl D ) by TOPS_3:80;
hereby  ::_thesis: ( C,D are_separated implies A,B are_separated )
assume  A,B are_separated ; ::_thesis: C,D are_separated
then  ( Cl A misses B & A misses Cl B ) by CONNSP_1:def_1;
hence  C,D are_separated by A1, A2, CONNSP_1:def_1; ::_thesis: verum
end;
assume  C,D are_separated ; ::_thesis: A,B are_separated
then  ( Cl C misses D & C misses Cl D ) by CONNSP_1:def_1;
hence  A,B are_separated by A1, A2, CONNSP_1:def_1; ::_thesis: verum
end;

theorem Th7: :: TOPALG_3:7
for T being non empty TopSpace holds
( T is connected iff for f being Function of T,(1TopSp {0,1}) holds
( not f is continuous or not f is onto ) )
proof
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:5;
then reconsider X = {0}, Y = {1} as non empty open Subset of (1TopSp {0,1}) by TDLAT_3:15, ZFMISC_1:7;
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:139;
A7: ( the carrier of T = (f " X) \/ (f " Y) & f " X misses f " Y ) by A1, Th3, FUNCT_1:71, ZFMISC_1:11;
 [#] (1TopSp {0,1}) <> {} ;
then  ( f " X is open & f " Y is open ) by A4, TOPS_2:43;
hence  contradiction by A2, A3, A6, A7, CONNSP_1:11; ::_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 H1( set ) ->  Element of (1TopSp {0,1}) = j1;
deffunc H2( 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:11;
defpred S1[ set ] means $1 in A;
A14: for x being set st x in the carrier of T holds
( ( S1[x] implies H2(x) in the carrier of (1TopSp {0,1}) ) & ( not S1[x] implies H1(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
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(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_7;
then  f . x = 1 by TARSKI:def_1;
then  not S1[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_7; ::_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_7;
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_7; ::_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
percases ( y = 0 or y = 1 ) by A1, A24, TARSKI:def_2;
supposeA25: 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_7;
then A27: f . x = 0 by TARSKI:def_1;
 x in dom f by A26, FUNCT_1:def_7;
hence  y in rng f by A25, A27, FUNCT_1:def_3; ::_thesis: verum
end;
supposeA28: 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_7;
then A30: f . x = 1 by TARSKI:def_1;
 x in dom f by A29, FUNCT_1:def_7;
hence  y in rng f by A28, A30, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
then  ( f " ({} (1TopSp {0,1})) = {} T & f " ([#] (1TopSp {0,1})) = [#] T ) by A16, RELAT_1:134;
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:36;
then A31: f is continuous by TOPS_2:43;
 f is onto by A23, FUNCT_2:def_3;
hence  contradiction by A8, A31; ::_thesis: verum
end;

registration
cluster empty  ->  connected for TopStruct ;
coherence
 for b1 being TopStruct st b1 is empty holds
b1 is connected
proof
let T be TopStruct ; ::_thesis: ( T is empty implies T is connected )
assume A1: T is empty ; ::_thesis: T is connected
let A be Subset of T; :: according to CONNSP_1:def_2 ::_thesis: for b1 being Element of bool the carrier of T holds
( not [#] T = A \/ b1 or not A,b1 are_separated or A = {} T or b1 = {} T )
reconsider T = T as empty TopStruct by A1;
 the carrier of T is empty ;
hence  for b1 being Element of bool the carrier of T holds
( not [#] T = A \/ b1 or not A,b1 are_separated or A = {} T or b1 = {} T ) ; ::_thesis: verum
end;
end;

theorem :: TOPALG_3:8
for T being TopSpace st TopStruct(# the carrier of T, the topology of T #) is connected holds
T is connected
proof
let T be TopSpace; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) is connected implies T is connected )
set G = TopStruct(# the carrier of T, the topology of T #);
assume A1: TopStruct(# the carrier of T, the topology of T #) is connected ; ::_thesis: T is connected
let A, B be Subset of T; :: according to CONNSP_1:def_2 ::_thesis: ( not [#] T = A \/ B or not A,B are_separated or A = {} T or B = {} T )
assume A2: ( [#] T = A \/ B & A,B are_separated ) ; ::_thesis: ( A = {} T or B = {} T )
reconsider A1 = A, B1 = B as Subset of TopStruct(# the carrier of T, the topology of T #) ;
 ( [#] TopStruct(# the carrier of T, the topology of T #) = A1 \/ B1 & A1,B1 are_separated ) by A2, Th6;
then  ( A1 = {} TopStruct(# the carrier of T, the topology of T #) or B1 = {} TopStruct(# the carrier of T, the topology of T #) ) by A1, CONNSP_1:def_2;
hence  ( A = {} T or B = {} T ) ; ::_thesis: verum
end;

registration
let T be connected TopSpace;
cluster TopStruct(# the carrier of T, the topology of T #) ->  connected ;
coherence
 TopStruct(# the carrier of T, the topology of T #) is connected
proof
set G = TopStruct(# the carrier of T, the topology of T #);
let A, B be Subset of TopStruct(# the carrier of T, the topology of T #); :: according to CONNSP_1:def_2 ::_thesis: ( not [#] TopStruct(# the carrier of T, the topology of T #) = A \/ B or not A,B are_separated or A = {} TopStruct(# the carrier of T, the topology of T #) or B = {} TopStruct(# the carrier of T, the topology of T #) )
assume A1: ( [#] TopStruct(# the carrier of T, the topology of T #) = A \/ B & A,B are_separated ) ; ::_thesis: ( A = {} TopStruct(# the carrier of T, the topology of T #) or B = {} TopStruct(# the carrier of T, the topology of T #) )
reconsider A1 = A, B1 = B as Subset of T ;
 ( [#] T = A1 \/ B1 & A1,B1 are_separated ) by A1, Th6;
then  ( A1 = {} T or B1 = {} T ) by CONNSP_1:def_2;
hence  ( A = {} TopStruct(# the carrier of T, the topology of T #) or B = {} TopStruct(# the carrier of T, the topology of T #) ) ; ::_thesis: verum
end;
end;

theorem :: TOPALG_3:9
for S, T being non empty TopSpace st S,T are_homeomorphic & S is pathwise_connected holds
T is pathwise_connected
proof
let S, T be non empty TopSpace; ::_thesis: ( S,T are_homeomorphic & S is pathwise_connected implies T is pathwise_connected )
given h being Function of S,T such that A1: h is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: ( not S is pathwise_connected or T is pathwise_connected )
assume A2: for a, b being Point of S holds a,b are_connected ; :: according to BORSUK_2:def_3 ::_thesis: T is pathwise_connected
let a, b be Point of T; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected
 (h ") . a,(h ") . b are_connected by A2;
then consider f being Function of I[01],S such that
A3: f is continuous and
A4: f . 0 = (h ") . a and
A5: f . 1 = (h ") . b by BORSUK_2:def_1;
take g = h * f; :: according to BORSUK_2:def_1 ::_thesis: ( g is continuous & g . 0 = a & g . 1 = b )
 h is continuous by A1, TOPS_2:def_5;
hence  g is continuous by A3; ::_thesis: ( g . 0 = a & g . 1 = b )
A6: ( h is one-to-one & rng h = [#] T ) by A1, TOPS_2:def_5;
thus g . 0 = h . ((h ") . a) by A4, BORSUK_1:def_14, FUNCT_2:15
.= (h * (h ")) . a by FUNCT_2:15
.= (id T) . a by A6, TOPS_2:52
.= a by FUNCT_1:18 ; ::_thesis: g . 1 = b
thus g . 1 = h . ((h ") . b) by A5, BORSUK_1:def_15, FUNCT_2:15
.= (h * (h ")) . b by FUNCT_2:15
.= (id T) . b by A6, TOPS_2:52
.= b by FUNCT_1:18 ; ::_thesis: verum
end;

registration
cluster non empty trivial TopSpace-like  ->  non empty pathwise_connected for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is trivial holds
b1 is pathwise_connected
proof
let T be non empty TopSpace; ::_thesis: ( T is trivial implies T is pathwise_connected )
assume A1: T is trivial ; ::_thesis: T is pathwise_connected
let a, b be Point of T; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected
take f = I[01] --> a; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b )
thus  f is continuous ; ::_thesis: ( f . 0 = a & f . 1 = b )
 a = b by A1, STRUCT_0:def_10;
hence  ( f . 0 = a & f . 1 = b ) by BORSUK_1:def_14, BORSUK_1:def_15, FUNCOP_1:7; ::_thesis: verum
end;
end;

theorem :: TOPALG_3:10
for T being SubSpace of TOP-REAL 2 st the carrier of T is Simple_closed_curve holds
T is pathwise_connected
proof
let T be SubSpace of TOP-REAL 2; ::_thesis: ( the carrier of T is Simple_closed_curve implies T is pathwise_connected )
assume A1: the carrier of T is Simple_closed_curve ; ::_thesis: T is pathwise_connected
then reconsider P = the carrier of T as Simple_closed_curve ;
let a, b be Point of T; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected
 ( a in P & b in P ) ;
then reconsider p1 = a, p2 = b as Point of (TOP-REAL 2) ;
percases ( p1 <> p2 or p1 = p2 ) ;
suppose p1 <> p2 ; ::_thesis: a,b are_connected
then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A2: P1 is_an_arc_of p1,p2 and
 P2 is_an_arc_of p1,p2 and
A3: P = P1 \/ P2 and
 P1 /\ P2 = {p1,p2} by TOPREAL2:5;
 the carrier of ((TOP-REAL 2) | P1) = P1 by PRE_TOPC:8;
then A4: the carrier of ((TOP-REAL 2) | P1) c= P by A3, XBOOLE_1:7;
then A5: (TOP-REAL 2) | P1 is SubSpace of T by TSEP_1:4;
consider f1 being Function of I[01],((TOP-REAL 2) | P1) such that
A6: f1 is being_homeomorphism and
A7: ( f1 . 0 = p1 & f1 . 1 = p2 ) by A2, TOPREAL1:def_1;
reconsider f = f1 as Function of I[01],T by A4, FUNCT_2:7;
take  f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b )
 f1 is continuous by A6, TOPS_2:def_5;
hence  f is continuous by A5, PRE_TOPC:26; ::_thesis: ( f . 0 = a & f . 1 = b )
thus  ( f . 0 = a & f . 1 = b ) by A7; ::_thesis: verum
end;
supposeA8: p1 = p2 ; ::_thesis: a,b are_connected
reconsider T1 = T as non empty SubSpace of TOP-REAL 2 by A1;
reconsider a1 = a as Point of T1 ;
reconsider f = I[01] --> a1 as Function of I[01],T ;
take  f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b )
thus  f is continuous ; ::_thesis: ( f . 0 = a & f . 1 = b )
thus f . 0 = f . j0
.= a by FUNCOP_1:7 ; ::_thesis: f . 1 = b
thus f . 1 = f . j1
.= b by A8, FUNCOP_1:7 ; ::_thesis: verum
end;
end;
end;

theorem :: TOPALG_3:11
for T being TopSpace ex F being Subset-Family of T st
( F = { the carrier of T} & F is Cover of T & F is open )
proof
let T be TopSpace; ::_thesis: ex F being Subset-Family of T st
( F = { the carrier of T} & F is Cover of T & F is open )
set F = { the carrier of T};
 { the carrier of T} c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { the carrier of T} or a in bool the carrier of T )
assume  a in { the carrier of T} ; ::_thesis: a in bool the carrier of T
then  a = the carrier of T by TARSKI:def_1;
hence  a in bool the carrier of T by ZFMISC_1:def_1; ::_thesis: verum
end;
then reconsider F = { the carrier of T} as Subset-Family of T ;
take  F ; ::_thesis: ( F = { the carrier of T} & F is Cover of T & F is open )
thus  F = { the carrier of T} ; ::_thesis: ( F is Cover of T & F is open )
 the carrier of T c= union F by ZFMISC_1:25;
hence  F is Cover of T by SETFAM_1:def_11; ::_thesis: F is open
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open )
 [#] T = the carrier of T ;
hence  ( not P in F or P is open ) by TARSKI:def_1; ::_thesis: verum
end;

registration
let T be TopSpace;
cluster non empty open closed mutually-disjoint for Element of bool (bool the carrier of T);
existence
 ex b1 being Subset-Family of T st
( not b1 is empty & b1 is mutually-disjoint & b1 is open & b1 is closed )
proof
set F = {({} T)};
 {({} T)} c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {({} T)} or a in bool the carrier of T )
assume  a in {({} T)} ; ::_thesis: a in bool the carrier of T
then  a = {} T by TARSKI:def_1;
hence  a in bool the carrier of T ; ::_thesis: verum
end;
then reconsider F = {({} T)} as Subset-Family of T ;
take  F ; ::_thesis: ( not F is empty & F is mutually-disjoint & F is open & F is closed )
thus  ( not F is empty & F is mutually-disjoint ) by TAXONOM2:10; ::_thesis: ( F is open & F is closed )
thus  F is open ::_thesis: F is closed
proof
let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open )
thus  ( not P in F or P is open ) by TARSKI:def_1; ::_thesis: verum
end;
let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not P in F or P is closed )
thus  ( not P in F or P is closed ) by TARSKI:def_1; ::_thesis: verum
end;
end;

theorem :: TOPALG_3:12
for T being TopSpace
for D being open mutually-disjoint Subset-Family of T
for A being Subset of T
for X being set st A is connected & X in D & X meets A & D is Cover of A holds
A c= X
proof
let T be TopSpace; ::_thesis: for D being open mutually-disjoint Subset-Family of T
for A being Subset of T
for X being set st A is connected & X in D & X meets A & D is Cover of A holds
A c= X
let D be open mutually-disjoint Subset-Family of T; ::_thesis: for A being Subset of T
for X being set st A is connected & X in D & X meets A & D is Cover of A holds
A c= X
let A be Subset of T; ::_thesis: for X being set st A is connected & X in D & X meets A & D is Cover of A holds
A c= X
let X be set ; ::_thesis: ( A is connected & X in D & X meets A & D is Cover of A implies A c= X )
assume that
A1: T | A is connected and
A2: X in D and
A3: X meets A ; :: according to CONNSP_1:def_3 ::_thesis: ( not D is Cover of A or A c= X )
consider x being set  such that
A4: ( x in X & x in A ) by A3, XBOOLE_0:3;
assume  D is Cover of A ; ::_thesis: A c= X
then A5: A c= union D by SETFAM_1:def_11;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in X )
assume A6: a in A ; ::_thesis: a in X
then consider Z being set  such that
A7: a in Z and
A8: Z in D by A5, TARSKI:def_4;
set D2 =  {  (K /\ A) where K is Subset of T : ( K in D & not a in K )  }  ;
  {  (K /\ A) where K is Subset of T : ( K in D & not a in K )  }  c= bool A
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in  {  (K /\ A) where K is Subset of T : ( K in D & not a in K )  }  or d in bool A )
assume  d in  {  (K /\ A) where K is Subset of T : ( K in D & not a in K )  }  ; ::_thesis: d in bool A
then  ex K1 being Subset of T st
( d = K1 /\ A & K1 in D & not a in K1 ) ;
then  d c= A by XBOOLE_1:17;
hence  d in bool A ; ::_thesis: verum
end;
then reconsider D2 =  {  (K /\ A) where K is Subset of T : ( K in D & not a in K )  }  as Subset-Family of (T | A) by PRE_TOPC:8;
assume  not a in X ; ::_thesis: contradiction
then A9: X /\ A in D2 by A2;
 x in X /\ A by A4, XBOOLE_0:def_4;
then A10: x in union D2 by A9, TARSKI:def_4;
set D1 =  {  (K /\ A) where K is Subset of T : ( K in D & a in K )  }  ;
  {  (K /\ A) where K is Subset of T : ( K in D & a in K )  }  c= bool A
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in  {  (K /\ A) where K is Subset of T : ( K in D & a in K )  }  or d in bool A )
assume  d in  {  (K /\ A) where K is Subset of T : ( K in D & a in K )  }  ; ::_thesis: d in bool A
then  ex K1 being Subset of T st
( d = K1 /\ A & K1 in D & a in K1 ) ;
then  d c= A by XBOOLE_1:17;
hence  d in bool A ; ::_thesis: verum
end;
then reconsider D1 =  {  (K /\ A) where K is Subset of T : ( K in D & a in K )  }  as Subset-Family of (T | A) by PRE_TOPC:8;
A11: A c= (union D1) \/ (union D2)
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in A or b in (union D1) \/ (union D2) )
assume A12: b in A ; ::_thesis: b in (union D1) \/ (union D2)
then consider Z being set  such that
A13: b in Z and
A14: Z in D by A5, TARSKI:def_4;
reconsider Z = Z as Subset of T by A14;
A15: b in Z /\ A by A12, A13, XBOOLE_0:def_4;
percases ( a in Z or not a in Z ) ;
suppose a in Z ; ::_thesis: b in (union D1) \/ (union D2)
then  Z /\ A in D1 by A14;
then  b in union D1 by A15, TARSKI:def_4;
hence  b in (union D1) \/ (union D2) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose not a in Z ; ::_thesis: b in (union D1) \/ (union D2)
then  Z /\ A in D2 by A14;
then  b in union D2 by A15, TARSKI:def_4;
hence  b in (union D1) \/ (union D2) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
A16: Z /\ A in D1 by A7, A8;
A17: [#] (T | A) = A by PRE_TOPC:def_5;
 D1 is open
proof
let P be Subset of (T | A); :: according to TOPS_2:def_1 ::_thesis: ( not P in D1 or P is open )
assume  P in D1 ; ::_thesis: P is open
then consider K1 being Subset of T such that
A18: P = K1 /\ A and
A19: K1 in D and
 a in K1 ;
 K1 is open by A19, TOPS_2:def_1;
hence  P is open by A17, A18, TOPS_2:24; ::_thesis: verum
end;
then A20: union D1 is open by TOPS_2:19;
 D2 is open
proof
let P be Subset of (T | A); :: according to TOPS_2:def_1 ::_thesis: ( not P in D2 or P is open )
assume  P in D2 ; ::_thesis: P is open
then consider K1 being Subset of T such that
A21: P = K1 /\ A and
A22: K1 in D and
 not a in K1 ;
 K1 is open by A22, TOPS_2:def_1;
hence  P is open by A17, A21, TOPS_2:24; ::_thesis: verum
end;
then A23: union D2 is open by TOPS_2:19;
 the carrier of (T | A) = A by PRE_TOPC:8;
then A24: A = (union D1) \/ (union D2) by A11, XBOOLE_0:def_10;
 a in Z /\ A by A6, A7, XBOOLE_0:def_4;
then  union D1 <> {} (T | A) by A16, TARSKI:def_4;
then  union D1 meets union D2 by A1, A17, A20, A23, A24, A10, CONNSP_1:11;
then consider y being set  such that
A25: y in union D1 and
A26: y in union D2 by XBOOLE_0:3;
consider Y2 being set  such that
A27: y in Y2 and
A28: Y2 in D2 by A26, TARSKI:def_4;
consider K2 being Subset of T such that
A29: Y2 = K2 /\ A and
A30: ( K2 in D & not a in K2 ) by A28;
A31: y in K2 by A27, A29, XBOOLE_0:def_4;
consider Y1 being set  such that
A32: y in Y1 and
A33: Y1 in D1 by A25, TARSKI:def_4;
consider K1 being Subset of T such that
A34: Y1 = K1 /\ A and
A35: ( K1 in D & a in K1 ) by A33;
 y in K1 by A32, A34, XBOOLE_0:def_4;
then  K1 meets K2 by A31, XBOOLE_0:3;
hence  contradiction by A35, A30, TAXONOM2:def_5; ::_thesis: verum
end;

begin

theorem Th13: :: TOPALG_3:13
for S, T being TopSpace holds TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
proof
let S, T be TopSpace; ::_thesis: TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]
A1: the carrier of [:S,T:] = [: the carrier of S, the carrier of T:] by BORSUK_1:def_2
.= the carrier of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] by BORSUK_1:def_2 ;
 for C1 being Subset of [:S,T:]
for C2 being Subset of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] st C1 = C2 holds
( C1 is open iff C2 is open )
proof
let C1 be Subset of [:S,T:]; ::_thesis: for C2 being Subset of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] st C1 = C2 holds
( C1 is open iff C2 is open )
let C2 be Subset of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):]; ::_thesis: ( C1 = C2 implies ( C1 is open iff C2 is open ) )
assume A2: C1 = C2 ; ::_thesis: ( C1 is open iff C2 is open )
hereby  ::_thesis: ( C2 is open implies C1 is open )
assume  C1 is open ; ::_thesis: C2 is open
then consider A being Subset-Family of [:S,T:] such that
A3: C1 = union A and
A4: for e being set st e in A holds
ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
reconsider AA = A as Subset-Family of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] by A1;
 for e being set st e in AA holds
ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
proof
let e be set ; ::_thesis: ( e in AA implies ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume  e in AA ; ::_thesis: ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then consider X1 being Subset of S, Y1 being Subset of T such that
A5: ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A4;
reconsider Y2 = Y1 as Subset of TopStruct(# the carrier of T, the topology of T #) ;
reconsider X2 = X1 as Subset of TopStruct(# the carrier of S, the topology of S #) ;
take  X2 ; ::_thesis: ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X2,Y1:] & X2 is open & Y1 is open )
take  Y2 ; ::_thesis: ( e = [:X2,Y2:] & X2 is open & Y2 is open )
thus  ( e = [:X2,Y2:] & X2 is open & Y2 is open ) by A5, TOPS_3:76; ::_thesis: verum
end;
hence  C2 is open by A2, A3, BORSUK_1:5; ::_thesis: verum
end;
assume  C2 is open ; ::_thesis: C1 is open
then consider A being Subset-Family of [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] such that
A6: C2 = union A and
A7: for e being set st e in A holds
ex X1 being Subset of TopStruct(# the carrier of S, the topology of S #) ex Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
reconsider AA = A as Subset-Family of [:S,T:] by A1;
 for e being set st e in AA holds
ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
proof
let e be set ; ::_thesis: ( e in AA implies ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume  e in AA ; ::_thesis: ex X1 being Subset of S ex Y1 being Subset of T st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then consider X1 being Subset of TopStruct(# the carrier of S, the topology of S #), Y1 being Subset of TopStruct(# the carrier of T, the topology of T #) such that
A8: ( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A7;
reconsider Y2 = Y1 as Subset of T ;
reconsider X2 = X1 as Subset of S ;
take  X2 ; ::_thesis: ex Y1 being Subset of T st
( e = [:X2,Y1:] & X2 is open & Y1 is open )
take  Y2 ; ::_thesis: ( e = [:X2,Y2:] & X2 is open & Y2 is open )
thus  ( e = [:X2,Y2:] & X2 is open & Y2 is open ) by A8, TOPS_3:76; ::_thesis: verum
end;
hence  C1 is open by A2, A6, BORSUK_1:5; ::_thesis: verum
end;
hence  TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] by A1, TOPS_3:72; ::_thesis: verum
end;

theorem Th14: :: TOPALG_3:14
for S, T being TopSpace
for A being Subset of S
for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]
proof
let S, T be TopSpace; ::_thesis: for A being Subset of S
for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]
let A be Subset of S; ::_thesis: for B being Subset of T holds Cl [:A,B:] = [:(Cl A),(Cl B):]
let B be Subset of T; ::_thesis: Cl [:A,B:] = [:(Cl A),(Cl B):]
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: [:(Cl A),(Cl B):] c= Cl [:A,B:]
let x be set ; ::_thesis: ( x in Cl [:A,B:] implies x in [:(Cl A),(Cl B):] )
assume A1: x in Cl [:A,B:] ; ::_thesis: x in [:(Cl A),(Cl B):]
then reconsider S1 = S, T1 = T as non empty TopSpace ;
reconsider p = x as Point of [:S1,T1:] by A1;
consider K being Basis of p such that
A2: for Q being Subset of [:S1,T1:] st Q in K holds
[:A,B:] meets Q by A1, YELLOW13:17;
consider p1 being Point of S1, p2 being Point of T1 such that
A3: p = [p1,p2] by BORSUK_1:10;
 for G being Subset of T1 st G is open & p2 in G holds
B meets G
proof
let G be Subset of T1; ::_thesis: ( G is open & p2 in G implies B meets G )
assume  ( G is open & p2 in G ) ; ::_thesis: B meets G
then  ( [p1,p2] in [:([#] S1),G:] & [:([#] S1),G:] is open ) by BORSUK_1:6, ZFMISC_1:87;
then consider V being Subset of [:S1,T1:] such that
A4: V in K and
A5: V c= [:([#] S1),G:] by A3, YELLOW_8:def_1;
 [:A,B:] meets V by A2, A4;
then consider a being set  such that
A6: ( a in [:A,B:] & a in V ) by XBOOLE_0:3;
 a in [:A,B:] /\ [:([#] S1),G:] by A5, A6, XBOOLE_0:def_4;
then  a in [:(A /\ ([#] S1)),(B /\ G):] by ZFMISC_1:100;
then  ex a1, a2 being set st
( a1 in A /\ ([#] S1) & a2 in B /\ G & a = [a1,a2] ) by ZFMISC_1:def_2;
hence  B meets G by XBOOLE_0:def_7; ::_thesis: verum
end;
then A7: p2 in Cl B by PRE_TOPC:def_7;
 for G being Subset of S1 st G is open & p1 in G holds
A meets G
proof
let G be Subset of S1; ::_thesis: ( G is open & p1 in G implies A meets G )
assume  ( G is open & p1 in G ) ; ::_thesis: A meets G
then  ( [p1,p2] in [:G,([#] T1):] & [:G,([#] T1):] is open ) by BORSUK_1:6, ZFMISC_1:87;
then consider V being Subset of [:S1,T1:] such that
A8: V in K and
A9: V c= [:G,([#] T1):] by A3, YELLOW_8:def_1;
 [:A,B:] meets V by A2, A8;
then consider a being set  such that
A10: ( a in [:A,B:] & a in V ) by XBOOLE_0:3;
 a in [:A,B:] /\ [:G,([#] T1):] by A9, A10, XBOOLE_0:def_4;
then  a in [:(A /\ G),(B /\ ([#] T1)):] by ZFMISC_1:100;
then  ex a1, a2 being set st
( a1 in A /\ G & a2 in B /\ ([#] T1) & a = [a1,a2] ) by ZFMISC_1:def_2;
hence  A meets G by XBOOLE_0:def_7; ::_thesis: verum
end;
then  p1 in Cl A by PRE_TOPC:def_7;
hence  x in [:(Cl A),(Cl B):] by A3, A7, ZFMISC_1:87; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:(Cl A),(Cl B):] or x in Cl [:A,B:] )
assume  x in [:(Cl A),(Cl B):] ; ::_thesis: x in Cl [:A,B:]
then consider x1, x2 being set  such that
A11: x1 in Cl A and
A12: x2 in Cl B and
A13: x = [x1,x2] by ZFMISC_1:def_2;
reconsider S1 = S, T1 = T as non empty TopSpace by A11, A12;
reconsider x1 = x1 as Point of S1 by A11;
consider K1 being Basis of x1 such that
A14: for Q being Subset of S1 st Q in K1 holds
A meets Q by A11, YELLOW13:17;
reconsider x2 = x2 as Point of T1 by A12;
consider K2 being Basis of x2 such that
A15: for Q being Subset of T1 st Q in K2 holds
B meets Q by A12, YELLOW13:17;
 for G being Subset of [:S1,T1:] st G is open & [x1,x2] in G holds
[:A,B:] meets G
proof
let G be Subset of [:S1,T1:]; ::_thesis: ( G is open & [x1,x2] in G implies [:A,B:] meets G )
assume that
A16: G is open and
A17: [x1,x2] in G ; ::_thesis: [:A,B:] meets G
consider F being Subset-Family of [:S1,T1:] such that
A18: G = union F and
A19: for e being set st e in F holds
ex X1 being Subset of S1 ex Y1 being Subset of T1 st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A16, BORSUK_1:5;
consider Z being set  such that
A20: [x1,x2] in Z and
A21: Z in F by A17, A18, TARSKI:def_4;
consider X1 being Subset of S1, Y1 being Subset of T1 such that
A22: Z = [:X1,Y1:] and
A23: X1 is open and
A24: Y1 is open by A19, A21;
 x2 in Y1 by A20, A22, ZFMISC_1:87;
then consider V2 being Subset of T1 such that
A25: V2 in K2 and
A26: V2 c= Y1 by A24, YELLOW_8:def_1;
 B meets V2 by A15, A25;
then consider a2 being set  such that
A27: a2 in B and
A28: a2 in V2 by XBOOLE_0:3;
 x1 in X1 by A20, A22, ZFMISC_1:87;
then consider V1 being Subset of S1 such that
A29: V1 in K1 and
A30: V1 c= X1 by A23, YELLOW_8:def_1;
 A meets V1 by A14, A29;
then consider a1 being set  such that
A31: a1 in A and
A32: a1 in V1 by XBOOLE_0:3;
 [a1,a2] in Z by A22, A30, A32, A26, A28, ZFMISC_1:87;
then A33: [a1,a2] in union F by A21, TARSKI:def_4;
 [a1,a2] in [:A,B:] by A31, A27, ZFMISC_1:87;
hence  [:A,B:] meets G by A18, A33, XBOOLE_0:3; ::_thesis: verum
end;
hence  x in Cl [:A,B:] by A13, PRE_TOPC:def_7; ::_thesis: verum
end;

theorem Th15: :: TOPALG_3:15
for S, T being TopSpace
for A being closed Subset of S
for B being closed Subset of T holds [:A,B:] is closed
proof
let S, T be TopSpace; ::_thesis: for A being closed Subset of S
for B being closed Subset of T holds [:A,B:] is closed
let A be closed Subset of S; ::_thesis: for B being closed Subset of T holds [:A,B:] is closed
let B be closed Subset of T; ::_thesis: [:A,B:] is closed
 ( Cl A = A & Cl [:A,B:] = [:(Cl A),(Cl B):] ) by Th14, PRE_TOPC:22;
hence  [:A,B:] is closed by PRE_TOPC:22; ::_thesis: verum
end;

registration
let A, B be connected TopSpace;
cluster[:A,B:] ->  connected ;
coherence
 [:A,B:] is connected
proof
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;
percases ( 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 ) ;
supposeA2: 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_#):],(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 ; ::_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, FUNCT_2:def_3;
then consider xy0 being set  such that
A7: xy0 in dom f and
A8: f . xy0 = j0 by FUNCT_1:def_3;
consider xy1 being set  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 set  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 set  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
assume A24: f . [x0,y1] <> 1 ; ::_thesis: contradiction
 h is onto
proof
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 set ; :: 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
percases ( y = 1 or y = 0 ) by A5, A26, TARSKI:def_2;
supposeA27: 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;
supposeA29: 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;
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 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
assume A36: f . [x0,y1] <> 0 ; ::_thesis: contradiction
 g is onto
proof
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 set ; :: 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
percases ( y = 0 or y = 1 ) by A5, A38, TARSKI:def_2;
supposeA39: 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;
supposeA41: 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;
end;
end;
hence  contradiction by A34, A35, Th7; ::_thesis: verum
end;
hence  contradiction by A23; ::_thesis: verum
end;
hence  [:A,B:] is connected by A1, A2, Th7; ::_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;
end;
end;

theorem :: TOPALG_3:16
for S, T being TopSpace
for A being Subset of S
for B being Subset of T st A is connected & B is connected holds
[:A,B:] is connected
proof
let S, T be TopSpace; ::_thesis: for A being Subset of S
for B being Subset of T st A is connected & B is connected holds
[:A,B:] is connected
let A be Subset of S; ::_thesis: for B being Subset of T st A is connected & B is connected holds
[:A,B:] is connected
let B be Subset of T; ::_thesis: ( A is connected & B is connected implies [:A,B:] is connected )
assume  ( S | A is connected & T | B is connected ) ; :: according to CONNSP_1:def_3 ::_thesis: [:A,B:] is connected
then reconsider SA = S | A, TB = T | B as connected TopSpace ;
 [:SA,TB:] is connected ;
hence  [:S,T:] | [:A,B:] is connected by BORSUK_3:22; :: according to CONNSP_1:def_3 ::_thesis: verum
end;

theorem :: TOPALG_3:17
for S, T being TopSpace
for Y being non empty TopSpace
for A being Subset of S
for f being Function of [:S,T:],Y
for g being Function of [:(S | A),T:],Y st g = f | [:A, the carrier of T:] & f is continuous holds
g is continuous
proof
let S, T be TopSpace; ::_thesis: for Y being non empty TopSpace
for A being Subset of S
for f being Function of [:S,T:],Y
for g being Function of [:(S | A),T:],Y st g = f | [:A, the carrier of T:] & f is continuous holds
g is continuous
let Y be non empty TopSpace; ::_thesis: for A being Subset of S
for f being Function of [:S,T:],Y
for g being Function of [:(S | A),T:],Y st g = f | [:A, the carrier of T:] & f is continuous holds
g is continuous
let A be Subset of S; ::_thesis: for f being Function of [:S,T:],Y
for g being Function of [:(S | A),T:],Y st g = f | [:A, the carrier of T:] & f is continuous holds
g is continuous
let f be Function of [:S,T:],Y; ::_thesis: for g being Function of [:(S | A),T:],Y st g = f | [:A, the carrier of T:] & f is continuous holds
g is continuous
let g be Function of [:(S | A),T:],Y; ::_thesis: ( g = f | [:A, the carrier of T:] & f is continuous implies g is continuous )
assume A1: ( g = f | [:A, the carrier of T:] & f is continuous ) ; ::_thesis: g is continuous
set TT = TopStruct(# the carrier of T, the topology of T #);
A2: [:(S | A),TopStruct(# the carrier of T, the topology of T #):] = [:(S | A),(TopStruct(# the carrier of T, the topology of T #) | ([#] TopStruct(# the carrier of T, the topology of T #))):] by TSEP_1:3
.= [:S,TopStruct(# the carrier of T, the topology of T #):] | [:A,([#] TopStruct(# the carrier of T, the topology of T #)):] by BORSUK_3:22 ;
 TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] by Th13;
then A3: TopStruct(# the carrier of [:S,TopStruct(# the carrier of T, the topology of T #):], the topology of [:S,TopStruct(# the carrier of T, the topology of T #):] #) = TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) by Th13;
 TopStruct(# the carrier of [:(S | A),TopStruct(# the carrier of T, the topology of T #):], the topology of [:(S | A),TopStruct(# the carrier of T, the topology of T #):] #) = TopStruct(# the carrier of [:(S | A),T:], the topology of [:(S | A),T:] #) by Th13;
hence  g is continuous by A1, A3, A2, TOPMETR:7; ::_thesis: verum
end;

theorem :: TOPALG_3:18
for S, T being TopSpace
for Y being non empty TopSpace
for A being Subset of T
for f being Function of [:S,T:],Y
for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous
proof
let S, T be TopSpace; ::_thesis: for Y being non empty TopSpace
for A being Subset of T
for f being Function of [:S,T:],Y
for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous
let Y be non empty TopSpace; ::_thesis: for A being Subset of T
for f being Function of [:S,T:],Y
for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous
let A be Subset of T; ::_thesis: for f being Function of [:S,T:],Y
for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous
let f be Function of [:S,T:],Y; ::_thesis: for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous
let g be Function of [:S,(T | A):],Y; ::_thesis: ( g = f | [: the carrier of S,A:] & f is continuous implies g is continuous )
assume A1: ( g = f | [: the carrier of S,A:] & f is continuous ) ; ::_thesis: g is continuous
set SS = TopStruct(# the carrier of S, the topology of S #);
A2: [:TopStruct(# the carrier of S, the topology of S #),(T | A):] = [:(TopStruct(# the carrier of S, the topology of S #) | ([#] TopStruct(# the carrier of S, the topology of S #))),(T | A):] by TSEP_1:3
.= [:TopStruct(# the carrier of S, the topology of S #),T:] | [:([#] TopStruct(# the carrier of S, the topology of S #)),A:] by BORSUK_3:22 ;
 TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) = [:TopStruct(# the carrier of S, the topology of S #),TopStruct(# the carrier of T, the topology of T #):] by Th13;
then A3: TopStruct(# the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:], the topology of [:TopStruct(# the carrier of S, the topology of S #),T:] #) = TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) by Th13;
 TopStruct(# the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | A):], the topology of [:TopStruct(# the carrier of S, the topology of S #),(T | A):] #) = TopStruct(# the carrier of [:S,(T | A):], the topology of [:S,(T | A):] #) by Th13;
hence  g is continuous by A1, A3, A2, TOPMETR:7; ::_thesis: verum
end;

theorem :: TOPALG_3:19
for S, T, T1, T2, Y being non empty TopSpace
for f being Function of [:Y,T1:],S
for g being Function of [:Y,T2:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) holds
ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )
proof
let S, T, T1, T2, Y be non empty TopSpace; ::_thesis: for f being Function of [:Y,T1:],S
for g being Function of [:Y,T2:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) holds
ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )
let f be Function of [:Y,T1:],S; ::_thesis: for g being Function of [:Y,T2:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) holds
ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )
let g be Function of [:Y,T2:],S; ::_thesis: for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) holds
ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )
let F1, F2 be closed Subset of T; ::_thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ) implies ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous ) )
assume that
A1: T1 is SubSpace of T and
A2: T2 is SubSpace of T and
A3: F1 = [#] T1 and
A4: F2 = [#] T2 and
A5: ([#] T1) \/ ([#] T2) = [#] T and
A6: f is continuous and
A7: g is continuous and
A8: for p being set st p in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) holds
f . p = g . p ; ::_thesis: ex h being Function of [:Y,T:],S st
( h = f +* g & h is continuous )
A9: dom f = the carrier of [:Y,T1:] by FUNCT_2:def_1;
set h = f +* g;
A10: the carrier of [:Y,T2:] = [: the carrier of Y, the carrier of T2:] by BORSUK_1:def_2;
A11: [:Y,T2:] is SubSpace of [:Y,T:] by A2, BORSUK_3:15;
A12: rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
A13: dom g = the carrier of [:Y,T2:] by FUNCT_2:def_1;
A14: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1;
A15: the carrier of [:Y,T1:] = [: the carrier of Y, the carrier of T1:] by BORSUK_1:def_2;
then A16: dom (f +* g) = [: the carrier of Y, the carrier of T:] by A5, A10, A9, A13, A14, ZFMISC_1:97;
A17: the carrier of [:Y,T:] = [: the carrier of Y, the carrier of T:] by BORSUK_1:def_2;
then reconsider h = f +* g as Function of [:Y,T:],S by A16, A12, FUNCT_2:2, XBOOLE_1:1;
take  h ; ::_thesis: ( h = f +* g & h is continuous )
thus  h = f +* g ; ::_thesis: h is continuous
A18: [:Y,T1:] is SubSpace of [:Y,T:] by A1, BORSUK_3:15;
 for P being Subset of S st P is closed holds
h " P is closed
proof
reconsider M = [:([#] Y),F1:] as Subset of [:Y,T:] ;
let P be Subset of S; ::_thesis: ( P is closed implies h " P is closed )
A19: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_[:Y,T2:])_implies_x_in_g_"_P_)_&_(_x_in_g_"_P_implies_x_in_(h_"_P)_/\_([#]_[:Y,T2:])_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] [:Y,T2:]) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] [:Y,T2:]) ) )
thus  ( x in (h " P) /\ ([#] [:Y,T2:]) implies x in g " P ) ::_thesis: ( x in g " P implies x in (h " P) /\ ([#] [:Y,T2:]) )
proof
assume A20: x in (h " P) /\ ([#] [:Y,T2:]) ; ::_thesis: x in g " P
then  x in h " P by XBOOLE_0:def_4;
then A21: h . x in P by FUNCT_1:def_7;
 g . x = h . x by A13, A20, FUNCT_4:13;
hence  x in g " P by A13, A20, A21, FUNCT_1:def_7; ::_thesis: verum
end;
assume A22: x in g " P ; ::_thesis: x in (h " P) /\ ([#] [:Y,T2:])
then A23: x in dom g by FUNCT_1:def_7;
 g . x in P by A22, FUNCT_1:def_7;
then A24: h . x in P by A23, FUNCT_4:13;
 x in dom h by A14, A23, XBOOLE_0:def_3;
then  x in h " P by A24, FUNCT_1:def_7;
hence  x in (h " P) /\ ([#] [:Y,T2:]) by A22, XBOOLE_0:def_4; ::_thesis: verum
end;
A25: for x being set st x in [#] [:Y,T1:] holds
h . x = f . x
proof
let x be set ; ::_thesis: ( x in [#] [:Y,T1:] implies h . x = f . x )
assume A26: x in [#] [:Y,T1:] ; ::_thesis: h . x = f . x
now__::_thesis:_h_._x_=_f_._x
percases ( x in [#] [:Y,T2:] or not x in [#] [:Y,T2:] ) ;
supposeA27: x in [#] [:Y,T2:] ; ::_thesis: h . x = f . x
then  x in ([#] [:Y,T1:]) /\ ([#] [:Y,T2:]) by A26, XBOOLE_0:def_4;
then  f . x = g . x by A8;
hence  h . x = f . x by A13, A27, FUNCT_4:13; ::_thesis: verum
end;
suppose not x in [#] [:Y,T2:] ; ::_thesis: h . x = f . x
hence  h . x = f . x by A13, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
hence  h . x = f . x ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_[:Y,T1:])_implies_x_in_f_"_P_)_&_(_x_in_f_"_P_implies_x_in_(h_"_P)_/\_([#]_[:Y,T1:])_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] [:Y,T1:]) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] [:Y,T1:]) ) )
thus  ( x in (h " P) /\ ([#] [:Y,T1:]) implies x in f " P ) ::_thesis: ( x in f " P implies x in (h " P) /\ ([#] [:Y,T1:]) )
proof
assume A28: x in (h " P) /\ ([#] [:Y,T1:]) ; ::_thesis: x in f " P
then  x in h " P by XBOOLE_0:def_4;
then A29: h . x in P by FUNCT_1:def_7;
 x in [#] [:Y,T1:] by A28;
then A30: x in dom f by FUNCT_2:def_1;
 f . x = h . x by A25, A28;
hence  x in f " P by A29, A30, FUNCT_1:def_7; ::_thesis: verum
end;
assume A31: x in f " P ; ::_thesis: x in (h " P) /\ ([#] [:Y,T1:])
then  x in dom f by FUNCT_1:def_7;
then A32: x in dom h by A14, XBOOLE_0:def_3;
 f . x in P by A31, FUNCT_1:def_7;
then  h . x in P by A25, A31;
then  x in h " P by A32, FUNCT_1:def_7;
hence  x in (h " P) /\ ([#] [:Y,T1:]) by A31, XBOOLE_0:def_4; ::_thesis: verum
end;
then A33: (h " P) /\ ([#] [:Y,T1:]) = f " P by TARSKI:1;
 the carrier of T2 is Subset of T by A2, TSEP_1:1;
then  [#] [:Y,T2:] c= [#] [:Y,T:] by A17, A10, ZFMISC_1:95;
then reconsider P2 = g " P as Subset of [:Y,T:] by XBOOLE_1:1;
 the carrier of T1 is Subset of T by A1, TSEP_1:1;
then  [#] [:Y,T1:] c= [#] [:Y,T:] by A17, A15, ZFMISC_1:95;
then reconsider P1 = f " P as Subset of [:Y,T:] by XBOOLE_1:1;
assume A34: P is closed ; ::_thesis: h " P is closed
then  f " P is closed by A6, PRE_TOPC:def_6;
then A35: ex F01 being Subset of [:Y,T:] st
( F01 is closed & f " P = F01 /\ ([#] [:Y,T1:]) ) by A18, PRE_TOPC:13;
h " P = (h " P) /\ (([#] [:Y,T1:]) \/ ([#] [:Y,T2:])) by A17, A9, A13, A14, A16, XBOOLE_1:28
.= ((h " P) /\ ([#] [:Y,T1:])) \/ ((h " P) /\ ([#] [:Y,T2:])) by XBOOLE_1:23 ;
then A36: h " P = (f " P) \/ (g " P) by A33, A19, TARSKI:1;
 ( M is closed & [#] [:Y,T1:] = [:([#] Y),F1:] ) by A3, Th15, BORSUK_3:1;
then A37: P1 is closed by A35;
 g " P is closed by A7, A34, PRE_TOPC:def_6;
then A38: ex F02 being Subset of [:Y,T:] st
( F02 is closed & g " P = F02 /\ ([#] [:Y,T2:]) ) by A11, PRE_TOPC:13;
reconsider M = [:([#] Y),F2:] as Subset of [:Y,T:] ;
 ( M is closed & [#] [:Y,T2:] = [:([#] Y),F2:] ) by A4, Th15, BORSUK_3:1;
then  P2 is closed by A38;
hence  h " P is closed by A36, A37; ::_thesis: verum
end;
hence  h is continuous by PRE_TOPC:def_6; ::_thesis: verum
end;

theorem :: TOPALG_3:20
for S, T, T1, T2, Y being non empty TopSpace
for f being Function of [:T1,Y:],S
for g being Function of [:T2,Y:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds
f . p = g . p ) holds
ex h being Function of [:T,Y:],S st
( h = f +* g & h is continuous )
proof
let S, T, T1, T2, Y be non empty TopSpace; ::_thesis: for f being Function of [:T1,Y:],S
for g being Function of [:T2,Y:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds
f . p = g . p ) holds
ex h being Function of [:T,Y:],S st
( h = f +* g & h is continuous )
let f be Function of [:T1,Y:],S; ::_thesis: for g being Function of [:T2,Y:],S
for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds
f . p = g . p ) holds
ex h being Function of [:T,Y:],S st
( h = f +* g & h is continuous )
let g be Function of [:T2,Y:],S; ::_thesis: for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds
f . p = g . p ) holds
ex h being Function of [:T,Y:],S st
( h = f +* g & h is continuous )
let F1, F2 be closed Subset of T; ::_thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds
f . p = g . p ) implies ex h being Function of [:T,Y:],S st
( h = f +* g & h is continuous ) )
assume that
A1: T1 is SubSpace of T and
A2: T2 is SubSpace of T and
A3: F1 = [#] T1 and
A4: F2 = [#] T2 and
A5: ([#] T1) \/ ([#] T2) = [#] T and
A6: f is continuous and
A7: g is continuous and
A8: for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds
f . p = g . p ; ::_thesis: ex h being Function of [:T,Y:],S st
( h = f +* g & h is continuous )
A9: dom f = the carrier of [:T1,Y:] by FUNCT_2:def_1;
A10: Y is SubSpace of Y by TSEP_1:2;
then A11: [:T2,Y:] is SubSpace of [:T,Y:] by A2, BORSUK_3:21;
set h = f +* g;
A12: the carrier of [:T2,Y:] = [: the carrier of T2, the carrier of Y:] by BORSUK_1:def_2;
A13: dom (f +* g) = (dom f) \/ (dom g) by FUNCT_4:def_1;
A14: rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
A15: dom g = the carrier of [:T2,Y:] by FUNCT_2:def_1;
A16: the carrier of [:T1,Y:] = [: the carrier of T1, the carrier of Y:] by BORSUK_1:def_2;
then A17: dom (f +* g) = [: the carrier of T, the carrier of Y:] by A5, A12, A9, A15, A13, ZFMISC_1:97;
A18: the carrier of [:T,Y:] = [: the carrier of T, the carrier of Y:] by BORSUK_1:def_2;
then reconsider h = f +* g as Function of [:T,Y:],S by A17, A14, FUNCT_2:2, XBOOLE_1:1;
take  h ; ::_thesis: ( h = f +* g & h is continuous )
thus  h = f +* g ; ::_thesis: h is continuous
A19: [:T1,Y:] is SubSpace of [:T,Y:] by A1, A10, BORSUK_3:21;
 for P being Subset of S st P is closed holds
h " P is closed
proof
reconsider M = [:F1,([#] Y):] as Subset of [:T,Y:] ;
let P be Subset of S; ::_thesis: ( P is closed implies h " P is closed )
A20: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_[:T2,Y:])_implies_x_in_g_"_P_)_&_(_x_in_g_"_P_implies_x_in_(h_"_P)_/\_([#]_[:T2,Y:])_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] [:T2,Y:]) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] [:T2,Y:]) ) )
thus  ( x in (h " P) /\ ([#] [:T2,Y:]) implies x in g " P ) ::_thesis: ( x in g " P implies x in (h " P) /\ ([#] [:T2,Y:]) )
proof
assume A21: x in (h " P) /\ ([#] [:T2,Y:]) ; ::_thesis: x in g " P
then  x in h " P by XBOOLE_0:def_4;
then A22: h . x in P by FUNCT_1:def_7;
 g . x = h . x by A15, A21, FUNCT_4:13;
hence  x in g " P by A15, A21, A22, FUNCT_1:def_7; ::_thesis: verum
end;
assume A23: x in g " P ; ::_thesis: x in (h " P) /\ ([#] [:T2,Y:])
then A24: x in dom g by FUNCT_1:def_7;
 g . x in P by A23, FUNCT_1:def_7;
then A25: h . x in P by A24, FUNCT_4:13;
 x in dom h by A13, A24, XBOOLE_0:def_3;
then  x in h " P by A25, FUNCT_1:def_7;
hence  x in (h " P) /\ ([#] [:T2,Y:]) by A23, XBOOLE_0:def_4; ::_thesis: verum
end;
A26: for x being set st x in [#] [:T1,Y:] holds
h . x = f . x
proof
let x be set ; ::_thesis: ( x in [#] [:T1,Y:] implies h . x = f . x )
assume A27: x in [#] [:T1,Y:] ; ::_thesis: h . x = f . x
now__::_thesis:_h_._x_=_f_._x
percases ( x in [#] [:T2,Y:] or not x in [#] [:T2,Y:] ) ;
supposeA28: x in [#] [:T2,Y:] ; ::_thesis: h . x = f . x
then  x in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) by A27, XBOOLE_0:def_4;
then  f . x = g . x by A8;
hence  h . x = f . x by A15, A28, FUNCT_4:13; ::_thesis: verum
end;
suppose not x in [#] [:T2,Y:] ; ::_thesis: h . x = f . x
hence  h . x = f . x by A15, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
hence  h . x = f . x ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_[:T1,Y:])_implies_x_in_f_"_P_)_&_(_x_in_f_"_P_implies_x_in_(h_"_P)_/\_([#]_[:T1,Y:])_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] [:T1,Y:]) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] [:T1,Y:]) ) )
thus  ( x in (h " P) /\ ([#] [:T1,Y:]) implies x in f " P ) ::_thesis: ( x in f " P implies x in (h " P) /\ ([#] [:T1,Y:]) )
proof
assume A29: x in (h " P) /\ ([#] [:T1,Y:]) ; ::_thesis: x in f " P
then  x in h " P by XBOOLE_0:def_4;
then A30: h . x in P by FUNCT_1:def_7;
 x in [#] [:T1,Y:] by A29;
then A31: x in dom f by FUNCT_2:def_1;
 f . x = h . x by A26, A29;
hence  x in f " P by A30, A31, FUNCT_1:def_7; ::_thesis: verum
end;
assume A32: x in f " P ; ::_thesis: x in (h " P) /\ ([#] [:T1,Y:])
then  x in dom f by FUNCT_1:def_7;
then A33: x in dom h by A13, XBOOLE_0:def_3;
 f . x in P by A32, FUNCT_1:def_7;
then  h . x in P by A26, A32;
then  x in h " P by A33, FUNCT_1:def_7;
hence  x in (h " P) /\ ([#] [:T1,Y:]) by A32, XBOOLE_0:def_4; ::_thesis: verum
end;
then A34: (h " P) /\ ([#] [:T1,Y:]) = f " P by TARSKI:1;
 the carrier of T2 is Subset of T by A2, TSEP_1:1;
then  [#] [:T2,Y:] c= [#] [:T,Y:] by A18, A12, ZFMISC_1:95;
then reconsider P2 = g " P as Subset of [:T,Y:] by XBOOLE_1:1;
 the carrier of T1 is Subset of T by A1, TSEP_1:1;
then  [#] [:T1,Y:] c= [#] [:T,Y:] by A18, A16, ZFMISC_1:95;
then reconsider P1 = f " P as Subset of [:T,Y:] by XBOOLE_1:1;
assume A35: P is closed ; ::_thesis: h " P is closed
then  f " P is closed by A6, PRE_TOPC:def_6;
then A36: ex F01 being Subset of [:T,Y:] st
( F01 is closed & f " P = F01 /\ ([#] [:T1,Y:]) ) by A19, PRE_TOPC:13;
h " P = (h " P) /\ (([#] [:T1,Y:]) \/ ([#] [:T2,Y:])) by A18, A9, A15, A13, A17, XBOOLE_1:28
.= ((h " P) /\ ([#] [:T1,Y:])) \/ ((h " P) /\ ([#] [:T2,Y:])) by XBOOLE_1:23 ;
then A37: h " P = (f " P) \/ (g " P) by A34, A20, TARSKI:1;
 ( M is closed & [#] [:T1,Y:] = [:F1,([#] Y):] ) by A3, Th15, BORSUK_3:1;
then A38: P1 is closed by A36;
 g " P is closed by A7, A35, PRE_TOPC:def_6;
then A39: ex F02 being Subset of [:T,Y:] st
( F02 is closed & g " P = F02 /\ ([#] [:T2,Y:]) ) by A11, PRE_TOPC:13;
reconsider M = [:F2,([#] Y):] as Subset of [:T,Y:] ;
 ( M is closed & [#] [:T2,Y:] = [:F2,([#] Y):] ) by A4, Th15, BORSUK_3:1;
then  P2 is closed by A39;
hence  h " P is closed by A37, A38; ::_thesis: verum
end;
hence  h is continuous by PRE_TOPC:def_6; ::_thesis: verum
end;

begin

registration
let T be non empty TopSpace;
let t be Point of T;
cluster  ->  continuous for Path of t,t;
coherence
 for b1 being Loop of t holds b1 is continuous
proof
 t,t are_connected ;
hence  for b1 being Loop of t holds b1 is continuous by BORSUK_2:def_2; ::_thesis: verum
end;
end;

theorem :: TOPALG_3:21
for T being non empty TopSpace
for t being Point of T
for x being Point of I[01]
for P being constant Loop of t holds P . x = t
proof
let T be non empty TopSpace; ::_thesis: for t being Point of T
for x being Point of I[01]
for P being constant Loop of t holds P . x = t
let t be Point of T; ::_thesis: for x being Point of I[01]
for P being constant Loop of t holds P . x = t
let x be Point of I[01]; ::_thesis: for P being constant Loop of t holds P . x = t
let P be constant Loop of t; ::_thesis: P . x = t
 P = I[01] --> t by BORSUK_2:5;
hence  P . x = t by FUNCOP_1:7; ::_thesis: verum
end;

theorem Th22: :: TOPALG_3:22
for T being non empty TopSpace
for t being Point of T
for P being Loop of t holds
( P . 0 = t & P . 1 = t )
proof
let T be non empty TopSpace; ::_thesis: for t being Point of T
for P being Loop of t holds
( P . 0 = t & P . 1 = t )
let t be Point of T; ::_thesis: for P being Loop of t holds
( P . 0 = t & P . 1 = t )
let P be Loop of t; ::_thesis: ( P . 0 = t & P . 1 = t )
 t,t are_connected ;
hence  ( P . 0 = t & P . 1 = t ) by BORSUK_2:def_2; ::_thesis: verum
end;

theorem Th23: :: TOPALG_3:23
for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S st a,b are_connected holds
f . a,f . b are_connected
proof
let S, T be non empty TopSpace; ::_thesis: for f being continuous Function of S,T
for a, b being Point of S st a,b are_connected holds
f . a,f . b are_connected
let f be continuous Function of S,T; ::_thesis: for a, b being Point of S st a,b are_connected holds
f . a,f . b are_connected
let a, b be Point of S; ::_thesis: ( a,b are_connected implies f . a,f . b are_connected )
given g being Function of I[01],S such that A1: g is continuous and
A2: g . 0 = a and
A3: g . 1 = b ; :: according to BORSUK_2:def_1 ::_thesis: f . a,f . b are_connected
take h = f * g; :: according to BORSUK_2:def_1 ::_thesis: ( h is continuous & h . 0 = f . a & h . 1 = f . b )
thus  h is continuous by A1; ::_thesis: ( h . 0 = f . a & h . 1 = f . b )
thus h . 0 = f . (g . j0) by FUNCT_2:15
.= f . a by A2 ; ::_thesis: h . 1 = f . b
thus h . 1 = f . (g . j1) by FUNCT_2:15
.= f . b by A3 ; ::_thesis: verum
end;

theorem :: TOPALG_3:24
for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b
proof
let S, T be non empty TopSpace; ::_thesis: for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b
let f be continuous Function of S,T; ::_thesis: for a, b being Point of S
for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b
let a, b be Point of S; ::_thesis: for P being Path of a,b st a,b are_connected holds
f * P is Path of f . a,f . b
let P be Path of a,b; ::_thesis: ( a,b are_connected implies f * P is Path of f . a,f . b )
assume A1: a,b are_connected ; ::_thesis: f * P is Path of f . a,f . b
A2: (f * P) . 1 = f . (P . j1) by FUNCT_2:15
.= f . b by A1, BORSUK_2:def_2 ;
A3: (f * P) . 0 = f . (P . j0) by FUNCT_2:15
.= f . a by A1, BORSUK_2:def_2 ;
 ( P is continuous & f . a,f . b are_connected ) by A1, Th23, BORSUK_2:def_2;
hence  f * P is Path of f . a,f . b by A3, A2, BORSUK_2:def_2; ::_thesis: verum
end;

theorem Th25: :: TOPALG_3:25
for S being non empty pathwise_connected TopSpace
for T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b holds f * P is Path of f . a,f . b
proof
let S be non empty pathwise_connected TopSpace; ::_thesis: for T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b holds f * P is Path of f . a,f . b
let T be non empty TopSpace; ::_thesis: for f being continuous Function of S,T
for a, b being Point of S
for P being Path of a,b holds f * P is Path of f . a,f . b
let f be continuous Function of S,T; ::_thesis: for a, b being Point of S
for P being Path of a,b holds f * P is Path of f . a,f . b
let a, b be Point of S; ::_thesis: for P being Path of a,b holds f * P is Path of f . a,f . b
let P be Path of a,b; ::_thesis: f * P is Path of f . a,f . b
A1: a,b are_connected by BORSUK_2:def_3;
A2: (f * P) . 1 = f . (P . j1) by FUNCT_2:15
.= f . b by A1, BORSUK_2:def_2 ;
A3: (f * P) . 0 = f . (P . j0) by FUNCT_2:15
.= f . a by A1, BORSUK_2:def_2 ;
 f . a,f . b are_connected by A1, Th23;
hence  f * P is Path of f . a,f . b by A3, A2, BORSUK_2:def_2; ::_thesis: verum
end;

definition
let S be non empty pathwise_connected TopSpace;
let T be non empty TopSpace;
let a, b be Point of S;
let P be Path of a,b;
let f be continuous Function of S,T;
:: original: *
redefine funcf * P ->  Path of f . a,f . b;
coherence
 P * f is Path of f . a,f . b by Th25;
end;

theorem Th26: :: TOPALG_3:26
for S, T being non empty TopSpace
for f being continuous Function of S,T
for a being Point of S
for P being Loop of a holds f * P is Loop of f . a
proof
let S, T be non empty TopSpace; ::_thesis: for f being continuous Function of S,T
for a being Point of S
for P being Loop of a holds f * P is Loop of f . a
let f be continuous Function of S,T; ::_thesis: for a being Point of S
for P being Loop of a holds f * P is Loop of f . a
let a be Point of S; ::_thesis: for P being Loop of a holds f * P is Loop of f . a
let P be Loop of a; ::_thesis: f * P is Loop of f . a
A1: f . a,f . a are_connected ;
A2: (f * P) . 1 = f . (P . j1) by FUNCT_2:15
.= f . a by Th22 ;
(f * P) . 0 = f . (P . j0) by FUNCT_2:15
.= f . a by Th22 ;
hence  f * P is Loop of f . a by A2, A1, BORSUK_2:def_2; ::_thesis: verum
end;

definition
let S, T be non empty TopSpace;
let a be Point of S;
let P be Loop of a;
let f be continuous Function of S,T;
:: original: *
redefine funcf * P ->  Loop of f . a;
coherence
 P * f is Loop of f . a by Th26;
end;

theorem Th27: :: TOPALG_3:27
for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
P1,Q1 are_homotopic
proof
let S, T be non empty TopSpace; ::_thesis: for f being continuous Function of S,T
for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
P1,Q1 are_homotopic
let f be continuous Function of S,T; ::_thesis: for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
P1,Q1 are_homotopic
let a, b be Point of S; ::_thesis: for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
P1,Q1 are_homotopic
let P, Q be Path of a,b; ::_thesis: for P1, Q1 being Path of f . a,f . b st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
P1,Q1 are_homotopic
let P1, Q1 be Path of f . a,f . b; ::_thesis: ( P,Q are_homotopic & P1 = f * P & Q1 = f * Q implies P1,Q1 are_homotopic )
assume that
A1: P,Q are_homotopic and
A2: P1 = f * P and
A3: Q1 = f * Q ; ::_thesis: P1,Q1 are_homotopic
set F = the Homotopy of P,Q;
take G = f * the Homotopy of P,Q; :: according to BORSUK_2:def_7 ::_thesis: ( G is continuous & ( for b1 being Element of the carrier of K527() holds
( G . (b1,0) = P1 . b1 & G . (b1,1) = Q1 . b1 & G . (0,b1) = f . a & G . (1,b1) = f . b ) ) )
 the Homotopy of P,Q is continuous by A1, BORSUK_6:def_11;
hence  G is continuous ; ::_thesis: for b1 being Element of the carrier of K527() holds
( G . (b1,0) = P1 . b1 & G . (b1,1) = Q1 . b1 & G . (0,b1) = f . a & G . (1,b1) = f . b )
let s be Point of I[01]; ::_thesis: ( G . (s,0) = P1 . s & G . (s,1) = Q1 . s & G . (0,s) = f . a & G . (1,s) = f . b )
thus G . (s,0) = f . ( the Homotopy of P,Q . (s,j0)) by Lm1, BINOP_1:18
.= f . (P . s) by A1, BORSUK_6:def_11
.= P1 . s by A2, FUNCT_2:15 ; ::_thesis: ( G . (s,1) = Q1 . s & G . (0,s) = f . a & G . (1,s) = f . b )
thus G . (s,1) = f . ( the Homotopy of P,Q . (s,j1)) by Lm1, BINOP_1:18
.= f . (Q . s) by A1, BORSUK_6:def_11
.= Q1 . s by A3, FUNCT_2:15 ; ::_thesis: ( G . (0,s) = f . a & G . (1,s) = f . b )
thus G . (0,s) = f . ( the Homotopy of P,Q . (j0,s)) by Lm1, BINOP_1:18
.= f . a by A1, BORSUK_6:def_11 ; ::_thesis: G . (1,s) = f . b
thus G . (1,s) = f . ( the Homotopy of P,Q . (j1,s)) by Lm1, BINOP_1:18
.= f . b by A1, BORSUK_6:def_11 ; ::_thesis: verum
end;

theorem :: TOPALG_3:28
for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
proof
let S, T be non empty TopSpace; ::_thesis: for f being continuous Function of S,T
for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let f be continuous Function of S,T; ::_thesis: for a, b being Point of S
for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let a, b be Point of S; ::_thesis: for P, Q being Path of a,b
for P1, Q1 being Path of f . a,f . b
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let P, Q be Path of a,b; ::_thesis: for P1, Q1 being Path of f . a,f . b
for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let P1, Q1 be Path of f . a,f . b; ::_thesis: for F being Homotopy of P,Q st P,Q are_homotopic & P1 = f * P & Q1 = f * Q holds
f * F is Homotopy of P1,Q1
let F be Homotopy of P,Q; ::_thesis: ( P,Q are_homotopic & P1 = f * P & Q1 = f * Q implies f * F is Homotopy of P1,Q1 )
assume that
A1: P,Q are_homotopic and
A2: P1 = f * P and
A3: Q1 = f * Q ; ::_thesis: f * F is Homotopy of P1,Q1
thus  P1,Q1 are_homotopic by A1, A2, A3, Th27; :: according to BORSUK_6:def_11 ::_thesis: ( f * F is continuous & ( for b1 being Element of the carrier of K527() holds
( (f * F) . (b1,0) = P1 . b1 & (f * F) . (b1,1) = Q1 . b1 & (f * F) . (0,b1) = f . a & (f * F) . (1,b1) = f . b ) ) )
set G = f * F;
 F is continuous by A1, BORSUK_6:def_11;
hence  f * F is continuous ; ::_thesis: for b1 being Element of the carrier of K527() holds
( (f * F) . (b1,0) = P1 . b1 & (f * F) . (b1,1) = Q1 . b1 & (f * F) . (0,b1) = f . a & (f * F) . (1,b1) = f . b )
let s be Point of I[01]; ::_thesis: ( (f * F) . (s,0) = P1 . s & (f * F) . (s,1) = Q1 . s & (f * F) . (0,s) = f . a & (f * F) . (1,s) = f . b )
thus (f * F) . (s,0) = f . (F . (s,j0)) by Lm1, BINOP_1:18
.= f . (P . s) by A1, BORSUK_6:def_11
.= P1 . s by A2, FUNCT_2:15 ; ::_thesis: ( (f * F) . (s,1) = Q1 . s & (f * F) . (0,s) = f . a & (f * F) . (1,s) = f . b )
thus (f * F) . (s,1) = f . (F . (s,j1)) by Lm1, BINOP_1:18
.= f . (Q . s) by A1, BORSUK_6:def_11
.= Q1 . s by A3, FUNCT_2:15 ; ::_thesis: ( (f * F) . (0,s) = f . a & (f * F) . (1,s) = f . b )
thus (f * F) . (0,s) = f . (F . (j0,s)) by Lm1, BINOP_1:18
.= f . a by A1, BORSUK_6:def_11 ; ::_thesis: (f * F) . (1,s) = f . b
thus (f * F) . (1,s) = f . (F . (j1,s)) by Lm1, BINOP_1:18
.= f . b by A1, BORSUK_6:def_11 ; ::_thesis: verum
end;

theorem Th29: :: TOPALG_3:29
for S, T being non empty TopSpace
for f being continuous Function of S,T
for a, b, c being Point of S
for P being Path of a,b
for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
proof
let S, T be non empty TopSpace; ::_thesis: for f being continuous Function of S,T
for a, b, c being Point of S
for P being Path of a,b
for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let f be continuous Function of S,T; ::_thesis: for a, b, c being Point of S
for P being Path of a,b
for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let a, b, c be Point of S; ::_thesis: for P being Path of a,b
for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let P be Path of a,b; ::_thesis: for Q being Path of b,c
for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let Q be Path of b,c; ::_thesis: for P1 being Path of f . a,f . b
for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let P1 be Path of f . a,f . b; ::_thesis: for Q1 being Path of f . b,f . c st a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q holds
P1 + Q1 = f * (P + Q)
let Q1 be Path of f . b,f . c; ::_thesis: ( a,b are_connected & b,c are_connected & P1 = f * P & Q1 = f * Q implies P1 + Q1 = f * (P + Q) )
assume that
A1: ( a,b are_connected & b,c are_connected ) and
A2: P1 = f * P and
A3: Q1 = f * Q ; ::_thesis: P1 + Q1 = f * (P + Q)
 for x being Point of I[01] holds (P1 + Q1) . x = (f * (P + Q)) . x
proof
let x be Point of I[01]; ::_thesis: (P1 + Q1) . x = (f * (P + Q)) . x
A4: ( f . a,f . b are_connected & f . b,f . c are_connected ) by A1, Th23;
percases ( x <= 1 / 2 or x >= 1 / 2 ) ;
supposeA5: x <= 1 / 2 ; ::_thesis: (P1 + Q1) . x = (f * (P + Q)) . x
then A6: 2 * x is Point of I[01] by BORSUK_6:3;
thus (P1 + Q1) . x = P1 . (2 * x) by A4, A5, BORSUK_2:def_5
.= f . (P . (2 * x)) by A2, A6, FUNCT_2:15
.= f . ((P + Q) . x) by A1, A5, BORSUK_2:def_5
.= (f * (P + Q)) . x by FUNCT_2:15 ; ::_thesis: verum
end;
supposeA7: x >= 1 / 2 ; ::_thesis: (P1 + Q1) . x = (f * (P + Q)) . x
then A8: (2 * x) - 1 is Point of I[01] by BORSUK_6:4;
thus (P1 + Q1) . x = Q1 . ((2 * x) - 1) by A4, A7, BORSUK_2:def_5
.= f . (Q . ((2 * x) - 1)) by A3, A8, FUNCT_2:15
.= f . ((P + Q) . x) by A1, A7, BORSUK_2:def_5
.= (f * (P + Q)) . x by FUNCT_2:15 ; ::_thesis: verum
end;
end;
end;
hence  P1 + Q1 = f * (P + Q) by FUNCT_2:63; ::_thesis: verum
end;

definition
let S, T be non empty TopSpace;
let s be Point of S;
let f be Function of S,T;
assume B1: f is continuous ;
set pT = pi_1 (T,(f . s));
set pS = pi_1 (S,s);
func FundGrIso (f,s) ->  Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) means :Def1: :: TOPALG_3:def 1
 for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & it . x = Class ((EqRel (T,(f . s))),(f * ls)) );
existence
 ex b1 being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st
for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b1 . x = Class ((EqRel (T,(f . s))),(f * ls)) )
proof
defpred S1[ set , set ] means  ex ls being Loop of s st
( $1 = Class ((EqRel (S,s)),ls) & $2 = Class ((EqRel (T,(f . s))),(f * ls)) );
A1: for x being Element of (pi_1 (S,s)) ex y being Element of (pi_1 (T,(f . s))) st S1[x,y]
proof
let x be Element of (pi_1 (S,s)); ::_thesis: ex y being Element of (pi_1 (T,(f . s))) st S1[x,y]
consider ls being Loop of s such that
A2: x = Class ((EqRel (S,s)),ls) by TOPALG_1:47;
reconsider lt = f * ls as Loop of f . s by B1, Th26;
reconsider y = Class ((EqRel (T,(f . s))),lt) as Element of (pi_1 (T,(f . s))) by TOPALG_1:47;
take  y ; ::_thesis: S1[x,y]
take  ls ; ::_thesis: ( x = Class ((EqRel (S,s)),ls) & y = Class ((EqRel (T,(f . s))),(f * ls)) )
thus  ( x = Class ((EqRel (S,s)),ls) & y = Class ((EqRel (T,(f . s))),(f * ls)) ) by A2; ::_thesis: verum
end;
 ex h being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st
for x being Element of (pi_1 (S,s)) holds S1[x,h . x] from FUNCT_2:sch_3(A1);
hence  ex b1 being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st
for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b1 . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) st ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b1 . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) & ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b2 . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) holds
b1 = b2
proof
let g, h be Function of (pi_1 (S,s)),(pi_1 (T,(f . s))); ::_thesis: ( ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & g . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) & ( for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & h . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ) implies g = h )
assume that
A3: for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & g . x = Class ((EqRel (T,(f . s))),(f * ls)) ) and
A4: for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & h . x = Class ((EqRel (T,(f . s))),(f * ls)) ) ; ::_thesis: g = h
now__::_thesis:_for_x_being_Element_of_(pi_1_(S,s))_holds_g_._x_=_h_._x
let x be Element of (pi_1 (S,s)); ::_thesis: g . x = h . x
consider lsg being Loop of s such that
A5: x = Class ((EqRel (S,s)),lsg) and
A6: g . x = Class ((EqRel (T,(f . s))),(f * lsg)) by A3;
consider lsh being Loop of s such that
A7: x = Class ((EqRel (S,s)),lsh) and
A8: h . x = Class ((EqRel (T,(f . s))),(f * lsh)) by A4;
reconsider ltg = f * lsg, lth = f * lsh as Loop of f . s by B1, Th26;
 lsg,lsh are_homotopic by A5, A7, TOPALG_1:46;
then  ltg,lth are_homotopic by B1, Th27;
hence  g . x = h . x by A6, A8, TOPALG_1:46; ::_thesis: verum
end;
hence  g = h by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines FundGrIso TOPALG_3:def_1_:_
 for S, T being non empty TopSpace
for s being Point of S
for f being Function of S,T st f is continuous holds
for b5 being Function of (pi_1 (S,s)),(pi_1 (T,(f . s))) holds
( b5 = FundGrIso (f,s) iff for x being Element of (pi_1 (S,s)) ex ls being Loop of s st
( x = Class ((EqRel (S,s)),ls) & b5 . x = Class ((EqRel (T,(f . s))),(f * ls)) ) );

theorem :: TOPALG_3:30
for S, T being non empty TopSpace
for s being Point of S
for f being continuous Function of S,T
for ls being Loop of s holds (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls))
proof
let S, T be non empty TopSpace; ::_thesis: for s being Point of S
for f being continuous Function of S,T
for ls being Loop of s holds (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls))
let s be Point of S; ::_thesis: for f being continuous Function of S,T
for ls being Loop of s holds (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls))
let f be continuous Function of S,T; ::_thesis: for ls being Loop of s holds (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls))
let ls be Loop of s; ::_thesis: (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls))
reconsider x = Class ((EqRel (S,s)),ls) as Element of (pi_1 (S,s)) by TOPALG_1:47;
consider ls1 being Loop of s such that
A1: x = Class ((EqRel (S,s)),ls1) and
A2: (FundGrIso (f,s)) . x = Class ((EqRel (T,(f . s))),(f * ls1)) by Def1;
 ls,ls1 are_homotopic by A1, TOPALG_1:46;
then  f * ls,f * ls1 are_homotopic by Th27;
hence  (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls)) by A2, TOPALG_1:46; ::_thesis: verum
end;

registration
let S, T be non empty TopSpace;
let s be Point of S;
let f be continuous Function of S,T;
cluster FundGrIso (f,s) ->  multiplicative ;
coherence
 FundGrIso (f,s) is multiplicative
proof
set h = FundGrIso (f,s);
set pS = pi_1 (S,s);
let a, b be Element of (pi_1 (S,s)); :: according to GROUP_6:def_6 ::_thesis: (FundGrIso (f,s)) . (a * b) = ((FundGrIso (f,s)) . a) * ((FundGrIso (f,s)) . b)
consider lsa being Loop of s such that
A1: a = Class ((EqRel (S,s)),lsa) and
A2: (FundGrIso (f,s)) . a = Class ((EqRel (T,(f . s))),(f * lsa)) by Def1;
consider lsb being Loop of s such that
A3: b = Class ((EqRel (S,s)),lsb) and
A4: (FundGrIso (f,s)) . b = Class ((EqRel (T,(f . s))),(f * lsb)) by Def1;
A5: (f * lsa) + (f * lsb) = f * (lsa + lsb) by Th29;
consider lsab being Loop of s such that
A6: a * b = Class ((EqRel (S,s)),lsab) and
A7: (FundGrIso (f,s)) . (a * b) = Class ((EqRel (T,(f . s))),(f * lsab)) by Def1;
 a * b = Class ((EqRel (S,s)),(lsa + lsb)) by A1, A3, TOPALG_1:61;
then  lsab,lsa + lsb are_homotopic by A6, TOPALG_1:46;
then  f * lsab,(f * lsa) + (f * lsb) are_homotopic by A5, Th27;
hence (FundGrIso (f,s)) . (a * b) = Class ((EqRel (T,(f . s))),((f * lsa) + (f * lsb))) by A7, TOPALG_1:46
.= ((FundGrIso (f,s)) . a) * ((FundGrIso (f,s)) . b) by A2, A4, TOPALG_1:61 ;
::_thesis: verum
end;
end;

theorem Th31: :: TOPALG_3:31
for S, T being non empty TopSpace
for s being Point of S
for f being continuous Function of S,T st f is being_homeomorphism holds
FundGrIso (f,s) is bijective
proof
let S, T be non empty TopSpace; ::_thesis: for s being Point of S
for f being continuous Function of S,T st f is being_homeomorphism holds
FundGrIso (f,s) is bijective
let s be Point of S; ::_thesis: for f being continuous Function of S,T st f is being_homeomorphism holds
FundGrIso (f,s) is bijective
set pS = pi_1 (S,s);
let f be continuous Function of S,T; ::_thesis: ( f is being_homeomorphism implies FundGrIso (f,s) is bijective )
assume A1: f is being_homeomorphism ; ::_thesis: FundGrIso (f,s) is bijective
A2: f is one-to-one by A1, TOPS_2:def_5;
then A3: (f ") . (f . s) = s by FUNCT_2:26;
set h = FundGrIso (f,s);
set pT = pi_1 (T,(f . s));
A4: f " is continuous by A1, TOPS_2:def_5;
A5: rng f = [#] T by A1, TOPS_2:def_5;
then  f is onto by FUNCT_2:def_3;
then A6: f " = f " by A2, TOPS_2:def_4;
A7: dom (FundGrIso (f,s)) = the carrier of (pi_1 (S,s)) by FUNCT_2:def_1;
A8: rng (FundGrIso (f,s)) = the carrier of (pi_1 (T,(f . s)))
proof
thus  rng (FundGrIso (f,s)) c= the carrier of (pi_1 (T,(f . s))) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (pi_1 (T,(f . s))) c= rng (FundGrIso (f,s))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of (pi_1 (T,(f . s))) or y in rng (FundGrIso (f,s)) )
assume  y in the carrier of (pi_1 (T,(f . s))) ; ::_thesis: y in rng (FundGrIso (f,s))
then consider lt being Loop of f . s such that
A9: y = Class ((EqRel (T,(f . s))),lt) by TOPALG_1:47;
reconsider ls = (f ") * lt as Loop of s by A4, A3, A6, Th26;
set x = Class ((EqRel (S,s)),ls);
A10: Class ((EqRel (S,s)),ls) in the carrier of (pi_1 (S,s)) by TOPALG_1:47;
then consider ls1 being Loop of s such that
A11: Class ((EqRel (S,s)),ls) = Class ((EqRel (S,s)),ls1) and
A12: (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = Class ((EqRel (T,(f . s))),(f * ls1)) by Def1;
A13: f * ls = (f * (f ")) * lt by RELAT_1:36
.= (id (rng f)) * lt by A5, A2, TOPS_2:52
.= lt by A5, FUNCT_2:17 ;
 ls,ls1 are_homotopic by A11, TOPALG_1:46;
then  lt,f * ls1 are_homotopic by A13, Th27;
then  (FundGrIso (f,s)) . (Class ((EqRel (S,s)),ls)) = y by A9, A12, TOPALG_1:46;
hence  y in rng (FundGrIso (f,s)) by A7, A10, FUNCT_1:def_3; ::_thesis: verum
end;
A14: dom f = [#] S by A1, TOPS_2:def_5;
 FundGrIso (f,s) is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (FundGrIso (f,s)) or not x2 in dom (FundGrIso (f,s)) or not (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 or x1 = x2 )
assume  x1 in dom (FundGrIso (f,s)) ; ::_thesis: ( not x2 in dom (FundGrIso (f,s)) or not (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 or x1 = x2 )
then consider ls1 being Loop of s such that
A15: x1 = Class ((EqRel (S,s)),ls1) and
A16: (FundGrIso (f,s)) . x1 = Class ((EqRel (T,(f . s))),(f * ls1)) by Def1;
assume  x2 in dom (FundGrIso (f,s)) ; ::_thesis: ( not (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 or x1 = x2 )
then consider ls2 being Loop of s such that
A17: x2 = Class ((EqRel (S,s)),ls2) and
A18: (FundGrIso (f,s)) . x2 = Class ((EqRel (T,(f . s))),(f * ls2)) by Def1;
reconsider a1 = (f ") * (f * ls1), a2 = (f ") * (f * ls2) as Loop of s by A4, A3, A6, Th26;
assume  (FundGrIso (f,s)) . x1 = (FundGrIso (f,s)) . x2 ; ::_thesis: x1 = x2
then  f * ls1,f * ls2 are_homotopic by A16, A18, TOPALG_1:46;
then A19: a1,a2 are_homotopic by A4, A3, A6, Th27;
A20: (f ") * f = id (dom f) by A5, A2, TOPS_2:52;
A21: (f ") * (f * ls1) = ((f ") * f) * ls1 by RELAT_1:36
.= ls1 by A14, A20, FUNCT_2:17 ;
(f ") * (f * ls2) = ((f ") * f) * ls2 by RELAT_1:36
.= ls2 by A14, A20, FUNCT_2:17 ;
hence  x1 = x2 by A15, A17, A21, A19, TOPALG_1:46; ::_thesis: verum
end;
hence  FundGrIso (f,s) is bijective by A8, GROUP_6:60; ::_thesis: verum
end;

theorem :: TOPALG_3:32
for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds
h is bijective
proof
let S, T be non empty TopSpace; ::_thesis: for s being Point of S
for t being Point of T
for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds
h is bijective
let s be Point of S; ::_thesis: for t being Point of T
for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds
h is bijective
let t be Point of T; ::_thesis: for f being continuous Function of S,T
for P being Path of t,f . s
for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds
h is bijective
let f be continuous Function of S,T; ::_thesis: for P being Path of t,f . s
for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds
h is bijective
let P be Path of t,f . s; ::_thesis: for h being Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)) st f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) holds
h is bijective
let h be Homomorphism of (pi_1 (S,s)),(pi_1 (T,t)); ::_thesis: ( f is being_homeomorphism & f . s,t are_connected & h = (pi_1-iso P) * (FundGrIso (f,s)) implies h is bijective )
assume  f is being_homeomorphism ; ::_thesis: ( not f . s,t are_connected or not h = (pi_1-iso P) * (FundGrIso (f,s)) or h is bijective )
then A1: FundGrIso (f,s) is bijective by Th31;
assume that
A2: f . s,t are_connected and
A3: h = (pi_1-iso P) * (FundGrIso (f,s)) ; ::_thesis: h is bijective
reconsider G = pi_1-iso P as Homomorphism of (pi_1 (T,(f . s))),(pi_1 (T,t)) by A2, TOPALG_1:50;
 G is bijective by A2, TOPALG_1:55;
hence  h is bijective by A1, A3, GROUP_6:64; ::_thesis: verum
end;

theorem :: TOPALG_3:33
for S being non empty TopSpace
for T being non empty pathwise_connected TopSpace
for s being Point of S
for t being Point of T st S,T are_homeomorphic holds
pi_1 (S,s), pi_1 (T,t) are_isomorphic
proof
let S be non empty TopSpace; ::_thesis: for T being non empty pathwise_connected TopSpace
for s being Point of S
for t being Point of T st S,T are_homeomorphic holds
pi_1 (S,s), pi_1 (T,t) are_isomorphic
let T be non empty pathwise_connected TopSpace; ::_thesis: for s being Point of S
for t being Point of T st S,T are_homeomorphic holds
pi_1 (S,s), pi_1 (T,t) are_isomorphic
let s be Point of S; ::_thesis: for t being Point of T st S,T are_homeomorphic holds
pi_1 (S,s), pi_1 (T,t) are_isomorphic
let t be Point of T; ::_thesis: ( S,T are_homeomorphic implies pi_1 (S,s), pi_1 (T,t) are_isomorphic )
given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: pi_1 (S,s), pi_1 (T,t) are_isomorphic
reconsider f = f as continuous Function of S,T by A1, TOPS_2:def_5;
set P = the Path of t,f . s;
take  (pi_1-iso the Path of t,f . s) * (FundGrIso (f,s)) ; :: according to GROUP_6:def_11 ::_thesis: (pi_1-iso the Path of t,f . s) * (FundGrIso (f,s)) is bijective
 FundGrIso (f,s) is bijective by A1, Th31;
hence  (pi_1-iso the Path of t,f . s) * (FundGrIso (f,s)) is bijective by GROUP_6:64; ::_thesis: verum
end;