:: FINTOPO5 semantic presentation

theorem Th1: :: FINTOPO5:1
for b1 being set
for b2 being non empty set
for b3 being Function of b1,b2
for b4 being Subset of b1 st b3 is one-to-one holds
(b3 " ) .: (b3 .: b4) = b4
proof end;

theorem Th2: :: FINTOPO5:2
for b1 being Nat holds
( b1 > 0 iff Seg b1 <> {} )
proof end;

definition
let c1, c2 be FT_Space_Str ;
let c3 be Function of c1,c2;
pred c3 is_homeomorphism means :Def1: :: FINTOPO5:def 1
( a3 is one-to-one & a3 is onto & ( for b1 being Element of a1 holds a3 .: (the Nbd of a1 . b1) = the Nbd of a2 . (a3 . b1) ) );
end;

:: deftheorem Def1 defines is_homeomorphism FINTOPO5:def 1 :
for b1, b2 being FT_Space_Str
for b3 being Function of b1,b2 holds
( b3 is_homeomorphism iff ( b3 is one-to-one & b3 is onto & ( for b4 being Element of b1 holds b3 .: (the Nbd of b1 . b4) = the Nbd of b2 . (b3 . b4) ) ) );

theorem Th3: :: FINTOPO5:3
for b1, b2 being non empty FT_Space_Str
for b3 being Function of b1,b2 st b3 is_homeomorphism holds
ex b4 being Function of b2,b1 st
( b4 = b3 " & b4 is_homeomorphism )
proof end;

theorem Th4: :: FINTOPO5:4
for b1, b2 being non empty FT_Space_Str
for b3 being Function of b1,b2
for b4 being Nat
for b5 being Element of b1
for b6 being Element of b2 st b3 is_homeomorphism & b6 = b3 . b5 holds
for b7 being Element of b1 holds
( b7 in U_FT b5,b4 iff b3 . b7 in U_FT b6,b4 )
proof end;

theorem Th5: :: FINTOPO5:5
for b1, b2 being non empty FT_Space_Str
for b3 being Function of b1,b2
for b4 being Nat
for b5 being Element of b1
for b6 being Element of b2 st b3 is_homeomorphism & b6 = b3 . b5 holds
for b7 being Element of b2 holds
( (b3 " ) . b7 in U_FT b5,b4 iff b7 in U_FT b6,b4 )
proof end;

theorem Th6: :: FINTOPO5:6
for b1 being non zero Nat
for b2 being Function of (FTSL1 b1),(FTSL1 b1) st b2 is_continuous 0 holds
ex b3 being Element of (FTSL1 b1) st b2 . b3 in U_FT b3,0
proof end;

theorem Th7: :: FINTOPO5:7
for b1 being non empty FT_Space_Str
for b2 being Element of b1
for b3 being Nat st b1 is filled holds
U_FT b2,b3 c= U_FT b2,(b3 + 1)
proof end;

theorem Th8: :: FINTOPO5:8
for b1 being non empty FT_Space_Str
for b2 being Element of b1
for b3 being Nat st b1 is filled holds
U_FT b2,0 c= U_FT b2,b3
proof end;

theorem Th9: :: FINTOPO5:9
for b1 being non zero Nat
for b2, b3, b4 being Nat
for b5 being Element of (FTSL1 b1) st b5 = b2 holds
( b3 in U_FT b5,b4 iff ( b3 in Seg b1 & abs (b2 - b3) <= b4 + 1 ) )
proof end;

theorem Th10: :: FINTOPO5:10
for b1, b2 being Nat
for b3 being non zero Nat
for b4 being Function of (FTSL1 b3),(FTSL1 b3) st b4 is_continuous b1 & b2 = [/(b1 / 2)\] holds
ex b5 being Element of (FTSL1 b3) st b4 . b5 in U_FT b5,b2
proof end;

definition
let c1, c2 be Nat;
func Nbdl2 c1,c2 -> Function of [:(Seg a1),(Seg a2):], bool [:(Seg a1),(Seg a2):] means :Def2: :: FINTOPO5:def 2
for b1 being set st b1 in [:(Seg a1),(Seg a2):] holds
for b2, b3 being Nat st b1 = [b2,b3] holds
a3 . b1 = [:((Nbdl1 a1) . b2),((Nbdl1 a2) . b3):];
existence
ex b1 being Function of [:(Seg c1),(Seg c2):], bool [:(Seg c1),(Seg c2):] st
for b2 being set st b2 in [:(Seg c1),(Seg c2):] holds
for b3, b4 being Nat st b2 = [b3,b4] holds
b1 . b2 = [:((Nbdl1 c1) . b3),((Nbdl1 c2) . b4):]
proof end;
uniqueness
for b1, b2 being Function of [:(Seg c1),(Seg c2):], bool [:(Seg c1),(Seg c2):] st ( for b3 being set st b3 in [:(Seg c1),(Seg c2):] holds
for b4, b5 being Nat st b3 = [b4,b5] holds
b1 . b3 = [:((Nbdl1 c1) . b4),((Nbdl1 c2) . b5):] ) & ( for b3 being set st b3 in [:(Seg c1),(Seg c2):] holds
for b4, b5 being Nat st b3 = [b4,b5] holds
b2 . b3 = [:((Nbdl1 c1) . b4),((Nbdl1 c2) . b5):] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Nbdl2 FINTOPO5:def 2 :
for b1, b2 being Nat
for b3 being Function of [:(Seg b1),(Seg b2):], bool [:(Seg b1),(Seg b2):] holds
( b3 = Nbdl2 b1,b2 iff for b4 being set st b4 in [:(Seg b1),(Seg b2):] holds
for b5, b6 being Nat st b4 = [b5,b6] holds
b3 . b4 = [:((Nbdl1 b1) . b5),((Nbdl1 b2) . b6):] );

definition
let c1, c2 be Nat;
func FTSL2 c1,c2 -> strict FT_Space_Str equals :: FINTOPO5:def 3
 FT_Space_Str(# [:(Seg a1),(Seg a2):],(Nbdl2 a1,a2) #);
coherence
FT_Space_Str(# [:(Seg c1),(Seg c2):],(Nbdl2 c1,c2) #) is strict FT_Space_Str ;
end;

:: deftheorem Def3 defines FTSL2 FINTOPO5:def 3 :
for b1, b2 being Nat holds FTSL2 b1,b2 = FT_Space_Str(# [:(Seg b1),(Seg b2):],(Nbdl2 b1,b2) #);

registration
let c1, c2 be non zero Nat;
cluster FTSL2 a1,a2 -> non empty strict ;
coherence
not FTSL2 c1,c2 is empty
proof end;
end;

theorem Th11: :: FINTOPO5:11
for b1, b2 being non zero Nat holds FTSL2 b1,b2 is filled
proof end;

theorem Th12: :: FINTOPO5:12
for b1, b2 being non zero Nat holds FTSL2 b1,b2 is symmetric
proof end;

theorem Th13: :: FINTOPO5:13
for b1 being non zero Nat ex b2 being Function of (FTSL2 b1,1),(FTSL1 b1) st b2 is_homeomorphism
proof end;

definition
let c1, c2 be Nat;
func Nbds2 c1,c2 -> Function of [:(Seg a1),(Seg a2):], bool [:(Seg a1),(Seg a2):] means :Def4: :: FINTOPO5:def 4
for b1 being set st b1 in [:(Seg a1),(Seg a2):] holds
for b2, b3 being Nat st b1 = [b2,b3] holds
a3 . b1 = [:{b2},((Nbdl1 a2) . b3):] \/ [:((Nbdl1 a1) . b2),{b3}:];
existence
ex b1 being Function of [:(Seg c1),(Seg c2):], bool [:(Seg c1),(Seg c2):] st
for b2 being set st b2 in [:(Seg c1),(Seg c2):] holds
for b3, b4 being Nat st b2 = [b3,b4] holds
b1 . b2 = [:{b3},((Nbdl1 c2) . b4):] \/ [:((Nbdl1 c1) . b3),{b4}:]
proof end;
uniqueness
for b1, b2 being Function of [:(Seg c1),(Seg c2):], bool [:(Seg c1),(Seg c2):] st ( for b3 being set st b3 in [:(Seg c1),(Seg c2):] holds
for b4, b5 being Nat st b3 = [b4,b5] holds
b1 . b3 = [:{b4},((Nbdl1 c2) . b5):] \/ [:((Nbdl1 c1) . b4),{b5}:] ) & ( for b3 being set st b3 in [:(Seg c1),(Seg c2):] holds
for b4, b5 being Nat st b3 = [b4,b5] holds
b2 . b3 = [:{b4},((Nbdl1 c2) . b5):] \/ [:((Nbdl1 c1) . b4),{b5}:] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines Nbds2 FINTOPO5:def 4 :
for b1, b2 being Nat
for b3 being Function of [:(Seg b1),(Seg b2):], bool [:(Seg b1),(Seg b2):] holds
( b3 = Nbds2 b1,b2 iff for b4 being set st b4 in [:(Seg b1),(Seg b2):] holds
for b5, b6 being Nat st b4 = [b5,b6] holds
b3 . b4 = [:{b5},((Nbdl1 b2) . b6):] \/ [:((Nbdl1 b1) . b5),{b6}:] );

definition
let c1, c2 be Nat;
func FTSS2 c1,c2 -> strict FT_Space_Str equals :: FINTOPO5:def 5
 FT_Space_Str(# [:(Seg a1),(Seg a2):],(Nbds2 a1,a2) #);
coherence
FT_Space_Str(# [:(Seg c1),(Seg c2):],(Nbds2 c1,c2) #) is strict FT_Space_Str ;
end;

:: deftheorem Def5 defines FTSS2 FINTOPO5:def 5 :
for b1, b2 being Nat holds FTSS2 b1,b2 = FT_Space_Str(# [:(Seg b1),(Seg b2):],(Nbds2 b1,b2) #);

registration
let c1, c2 be non zero Nat;
cluster FTSS2 a1,a2 -> non empty strict ;
coherence
not FTSS2 c1,c2 is empty
proof end;
end;

theorem Th14: :: FINTOPO5:14
for b1, b2 being non zero Nat holds FTSS2 b1,b2 is filled
proof end;

theorem Th15: :: FINTOPO5:15
for b1, b2 being non zero Nat holds FTSS2 b1,b2 is symmetric
proof end;

theorem Th16: :: FINTOPO5:16
for b1 being non zero Nat ex b2 being Function of (FTSS2 b1,1),(FTSL1 b1) st b2 is_homeomorphism
proof end;