:: TOPALG_3 semantic presentation

set c1 = the carrier of I[01] ;

set c2 = the carrier of R^1 ;

Lemma1: the carrier of [:I[01] ,I[01] :] = [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;

reconsider c3 = 0, c4 = 1 as Point of I[01] by BORSUK_1:def 17, BORSUK_1:def 18;

theorem Th1: :: TOPALG_3:1
for b1, b2, b3, b4 being set
for b5 being Function of b1,b2 st b3 in b1 & b4 in b2 holds
b5 +* (b3 .--> b4) is Function of b1,b2
proof end;

theorem Th2: :: TOPALG_3:2
for b1 being Function
for b2, b3 being set st b1 | b2 is one-to-one & b3 in rng (b1 | b2) holds
(b1 * ((b1 | b2) " )) . b3 = b3
proof end;

theorem Th3: :: TOPALG_3:3
for b1, b2, b3, b4, b5 being set
for b6 being Function of [:b3,b4:],b5
for b7 being Function st b5 <> {} & b1 in b3 & b2 in b4 holds
(b7 * b6) . b1,b2 = b7 . (b6 . b1,b2)
proof end;

theorem Th4: :: TOPALG_3:4
for b1, b2, b3 being set
for b4 being Function of b1,{b2,b3} holds b1 = (b4 " {b2}) \/ (b4 " {b3})
proof end;

theorem Th5: :: TOPALG_3:5
for b1, b2 being non empty 1-sorted
for b3 being Point of b1
for b4 being Point of b2 holds (b1 --> b4) . b3 = b4
proof end;

theorem Th6: :: TOPALG_3:6
for b1 being non empty TopStruct
for b2 being Point of b1
for b3 being Subset of b1 st b3 = {b2} holds
Sspace b2 = b1 | b3
proof end;

theorem Th7: :: TOPALG_3:7
for b1 being TopSpace
for b2, b3 being Subset of b1
for b4, b5 being Subset of TopStruct(# the carrier of b1,the topology of b1 #) st b2 = b4 & b3 = b5 holds
( b2,b3 are_separated iff b4,b5 are_separated )
proof end;

theorem Th8: :: TOPALG_3:8
for b1 being non empty TopSpace holds
( b1 is connected iff for b2 being Function of b1,(1TopSp {0,1}) holds
( not b2 is continuous or not b2 is onto ) )
proof end;

registration
cluster empty -> connected TopStruct ;
coherence
for b1 being TopStruct st b1 is empty holds
b1 is connected
proof end;
end;

theorem Th9: :: TOPALG_3:9
for b1 being TopSpace st TopStruct(# the carrier of b1,the topology of b1 #) is connected holds
b1 is connected
proof end;

registration
let c5 be connected TopSpace;
cluster TopStruct(# the carrier of a1,the topology of a1 #) -> connected ;
coherence
TopStruct(# the carrier of c5,the topology of c5 #) is connected
proof end;
end;

theorem Th10: :: TOPALG_3:10
for b1, b2 being non empty TopSpace st b1,b2 are_homeomorphic & b1 is arcwise_connected holds
b2 is arcwise_connected
proof end;

registration
cluster non empty trivial -> non empty arcwise_connected TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is trivial holds
b1 is arcwise_connected
proof end;
end;

theorem Th11: :: TOPALG_3:11
for b1 being SubSpace of TOP-REAL 2 st the carrier of b1 is Simple_closed_curve holds
b1 is arcwise_connected
proof end;

theorem Th12: :: TOPALG_3:12
for b1 being TopSpace ex b2 being Subset-Family of b1 st
( b2 = {the carrier of b1} & b2 is_a_cover_of b1 & b2 is open )
proof end;

registration
let c5 be TopSpace;
cluster non empty open closed mutually-disjoint Element of bool (bool the carrier of a1);
existence
ex b1 being Subset-Family of c5 st
( not b1 is empty & b1 is mutually-disjoint & b1 is open & b1 is closed )
proof end;
end;

theorem Th13: :: TOPALG_3:13
for b1 being TopSpace
for b2 being open mutually-disjoint Subset-Family of b1
for b3 being Subset of b1
for b4 being set st b3 is connected & b4 in b2 & b4 meets b3 & b2 is_a_cover_of b3 holds
b3 c= b4
proof end;

theorem Th14: :: TOPALG_3:14
for b1, b2 being TopSpace holds TopStruct(# the carrier of [:b1,b2:],the topology of [:b1,b2:] #) = [:TopStruct(# the carrier of b1,the topology of b1 #),TopStruct(# the carrier of b2,the topology of b2 #):]
proof end;

theorem Th15: :: TOPALG_3:15
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 holds Cl [:b3,b4:] = [:(Cl b3),(Cl b4):]
proof end;

theorem Th16: :: TOPALG_3:16
for b1, b2 being TopSpace
for b3 being closed Subset of b1
for b4 being closed Subset of b2 holds [:b3,b4:] is closed
proof end;

registration
let c5, c6 be connected TopSpace;
cluster [:a1,a2:] -> connected ;
coherence
[:c5,c6:] is connected
proof end;
end;

theorem Th17: :: TOPALG_3:17
for b1, b2 being TopSpace
for b3 being Subset of b1
for b4 being Subset of b2 st b3 is connected & b4 is connected holds
[:b3,b4:] is connected
proof end;

theorem Th18: :: TOPALG_3:18
for b1, b2 being TopSpace
for b3 being non empty TopSpace
for b4 being Subset of b1
for b5 being Function of [:b1,b2:],b3
for b6 being Function of [:(b1 | b4),b2:],b3 st b6 = b5 | [:b4,the carrier of b2:] & b5 is continuous holds
b6 is continuous
proof end;

theorem Th19: :: TOPALG_3:19
for b1, b2 being TopSpace
for b3 being non empty TopSpace
for b4 being Subset of b2
for b5 being Function of [:b1,b2:],b3
for b6 being Function of [:b1,(b2 | b4):],b3 st b6 = b5 | [:the carrier of b1,b4:] & b5 is continuous holds
b6 is continuous
proof end;

theorem Th20: :: TOPALG_3:20
for b1, b2, b3, b4, b5 being non empty TopSpace
for b6 being Function of [:b5,b3:],b1
for b7 being Function of [:b5,b4:],b1
for b8, b9 being closed Subset of b2 st b3 is SubSpace of b2 & b4 is SubSpace of b2 & b8 = [#] b3 & b9 = [#] b4 & ([#] b3) \/ ([#] b4) = [#] b2 & b6 is continuous & b7 is continuous & ( for b10 being set st b10 in ([#] [:b5,b3:]) /\ ([#] [:b5,b4:]) holds
b6 . b10 = b7 . b10 ) holds
ex b10 being Function of [:b5,b2:],b1 st
( b10 = b6 +* b7 & b10 is continuous )
proof end;

theorem Th21: :: TOPALG_3:21
for b1, b2, b3, b4, b5 being non empty TopSpace
for b6 being Function of [:b3,b5:],b1
for b7 being Function of [:b4,b5:],b1
for b8, b9 being closed Subset of b2 st b3 is SubSpace of b2 & b4 is SubSpace of b2 & b8 = [#] b3 & b9 = [#] b4 & ([#] b3) \/ ([#] b4) = [#] b2 & b6 is continuous & b7 is continuous & ( for b10 being set st b10 in ([#] [:b3,b5:]) /\ ([#] [:b4,b5:]) holds
b6 . b10 = b7 . b10 ) holds
ex b10 being Function of [:b2,b5:],b1 st
( b10 = b6 +* b7 & b10 is continuous )
proof end;

registration
let c5 be non empty TopSpace;
let c6 be Point of c5;
cluster -> continuous Path of a2,a2;
coherence
for b1 being Loop of c6 holds b1 is continuous
proof end;
end;

theorem Th22: :: TOPALG_3:22
for b1 being non empty TopSpace
for b2 being Point of b1
for b3 being Point of I[01]
for b4 being constant Loop of b2 holds b4 . b3 = b2
proof end;

theorem Th23: :: TOPALG_3:23
for b1 being non empty TopSpace
for b2 being Point of b1
for b3 being Loop of b2 holds
( b3 . 0 = b2 & b3 . 1 = b2 )
proof end;

theorem Th24: :: TOPALG_3:24
for b1, b2 being non empty TopSpace
for b3 being continuous Function of b1,b2
for b4, b5 being Point of b1 st b4,b5 are_connected holds
b3 . b4,b3 . b5 are_connected
proof end;

theorem Th25: :: TOPALG_3:25
for b1, b2 being non empty TopSpace
for b3 being continuous Function of b1,b2
for b4, b5 being Point of b1
for b6 being Path of b4,b5 st b4,b5 are_connected holds
b3 * b6 is Path of b3 . b4,b3 . b5
proof end;

theorem Th26: :: TOPALG_3:26
for b1 being non empty arcwise_connected TopSpace
for b2 being non empty TopSpace
for b3 being continuous Function of b1,b2
for b4, b5 being Point of b1
for b6 being Path of b4,b5 holds b3 * b6 is Path of b3 . b4,b3 . b5
proof end;

theorem Th27: :: TOPALG_3:27
for b1, b2 being non empty TopSpace
for b3 being continuous Function of b1,b2
for b4 being Point of b1
for b5 being Loop of b4 holds b3 * b5 is Loop of b3 . b4
proof end;

theorem Th28: :: TOPALG_3:28
for b1, b2 being non empty TopSpace
for b3 being continuous Function of b1,b2
for b4, b5 being Point of b1
for b6, b7 being Path of b4,b5
for b8, b9 being Path of b3 . b4,b3 . b5 st b6,b7 are_homotopic & b8 = b3 * b6 & b9 = b3 * b7 holds
b8,b9 are_homotopic
proof end;

theorem Th29: :: TOPALG_3:29
for b1, b2 being non empty TopSpace
for b3 being continuous Function of b1,b2
for b4, b5 being Point of b1
for b6, b7 being Path of b4,b5
for b8, b9 being Path of b3 . b4,b3 . b5
for b10 being Homotopy of b6,b7 st b6,b7 are_homotopic & b8 = b3 * b6 & b9 = b3 * b7 holds
b3 * b10 is Homotopy of b8,b9
proof end;

theorem Th30: :: TOPALG_3:30
for b1, b2 being non empty TopSpace
for b3 being continuous Function of b1,b2
for b4, b5, b6 being Point of b1
for b7 being Path of b4,b5
for b8 being Path of b5,b6
for b9 being Path of b3 . b4,b3 . b5
for b10 being Path of b3 . b5,b3 . b6 st b4,b5 are_connected & b5,b6 are_connected & b9 = b3 * b7 & b10 = b3 * b8 holds
b9 + b10 = b3 * (b7 + b8)
proof end;

theorem Th31: :: TOPALG_3:31
for b1 being non empty TopSpace
for b2 being Point of b1
for b3, b4 being Element of (pi_1 b1,b2)
for b5, b6 being Loop of b2 st b3 = Class (EqRel b1,b2),b5 & b4 = Class (EqRel b1,b2),b6 holds
b3 * b4 = Class (EqRel b1,b2),(b5 + b6)
proof end;

definition
let c5, c6 be non empty TopSpace;
let c7 be Point of c5;
let c8 be Function of c5,c6;
assume E16: c8 is continuous ;
set c9 = pi_1 c5,c7;
set c10 = pi_1 c6,(c8 . c7);
func FundGrIso c4,c3 -> Function of (pi_1 a1,a3),(pi_1 a2,(a4 . a3)) means :Def1: :: TOPALG_3:def 1
for b1 being Element of (pi_1 a1,a3) ex b2 being Loop of a3ex b3 being Loop of a4 . a3 st
( b1 = Class (EqRel a1,a3),b2 & b3 = a4 * b2 & a5 . b1 = Class (EqRel a2,(a4 . a3)),b3 );
existence
ex b1 being Function of (pi_1 c5,c7),(pi_1 c6,(c8 . c7)) st
for b2 being Element of (pi_1 c5,c7) ex b3 being Loop of c7ex b4 being Loop of c8 . c7 st
( b2 = Class (EqRel c5,c7),b3 & b4 = c8 * b3 & b1 . b2 = Class (EqRel c6,(c8 . c7)),b4 )
proof end;
uniqueness
for b1, b2 being Function of (pi_1 c5,c7),(pi_1 c6,(c8 . c7)) st ( for b3 being Element of (pi_1 c5,c7) ex b4 being Loop of c7ex b5 being Loop of c8 . c7 st
( b3 = Class (EqRel c5,c7),b4 & b5 = c8 * b4 & b1 . b3 = Class (EqRel c6,(c8 . c7)),b5 ) ) & ( for b3 being Element of (pi_1 c5,c7) ex b4 being Loop of c7ex b5 being Loop of c8 . c7 st
( b3 = Class (EqRel c5,c7),b4 & b5 = c8 * b4 & b2 . b3 = Class (EqRel c6,(c8 . c7)),b5 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines FundGrIso TOPALG_3:def 1 :
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Function of b1,b2 st b4 is continuous holds
for b5 being Function of (pi_1 b1,b3),(pi_1 b2,(b4 . b3)) holds
( b5 = FundGrIso b4,b3 iff for b6 being Element of (pi_1 b1,b3) ex b7 being Loop of b3ex b8 being Loop of b4 . b3 st
( b6 = Class (EqRel b1,b3),b7 & b8 = b4 * b7 & b5 . b6 = Class (EqRel b2,(b4 . b3)),b8 ) );

theorem Th32: :: TOPALG_3:32
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being continuous Function of b1,b2
for b5 being Element of (pi_1 b1,b3)
for b6 being Loop of b3
for b7 being Loop of b4 . b3 st b5 = Class (EqRel b1,b3),b6 & b7 = b4 * b6 holds
(FundGrIso b4,b3) . b5 = Class (EqRel b2,(b4 . b3)),b7
proof end;

definition
let c5, c6 be non empty TopSpace;
let c7 be Point of c5;
let c8 be continuous Function of c5,c6;
redefine func FundGrIso as FundGrIso c4,c3 -> Homomorphism of (pi_1 a1,a3),(pi_1 a2,(a4 . a3));
coherence
FundGrIso c8,c7 is Homomorphism of (pi_1 c5,c7),(pi_1 c6,(c8 . c7))
proof end;
end;

theorem Th33: :: TOPALG_3:33
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being continuous Function of b1,b2 st b4 is_homeomorphism holds
FundGrIso b4,b3 is_isomorphism
proof end;

theorem Th34: :: TOPALG_3:34
for b1, b2 being non empty TopSpace
for b3 being Point of b1
for b4 being Point of b2
for b5 being continuous Function of b1,b2
for b6 being Path of b4,b5 . b3
for b7 being Homomorphism of (pi_1 b1,b3),(pi_1 b2,b4) st b5 is_homeomorphism & b5 . b3,b4 are_connected & b7 = (pi_1-iso b6) * (FundGrIso b5,b3) holds
b7 is_isomorphism
proof end;

theorem Th35: :: TOPALG_3:35
for b1 being non empty TopSpace
for b2 being non empty arcwise_connected TopSpace
for b3 being Point of b1
for b4 being Point of b2 st b1,b2 are_homeomorphic holds
pi_1 b1,b3, pi_1 b2,b4 are_isomorphic
proof end;