:: RLTOPSP1 semantic presentation

theorem Th1: :: RLTOPSP1:1
for b1 being non empty RLSStruct
for b2 being Subset of b1
for b3 being Point of b1
for b4 being Real st b3 in b2 holds
b4 * b3 in b4 * b2 ;

registration
cluster non zero Element of REAL ;
existence
not for b1 being Real holds b1 is empty
proof end;
end;

theorem Th2: :: RLTOPSP1:2
for b1 being non empty TopSpace
for b2 being non empty Subset of b1
for b3 being Subset-Family of b1 st b3 is_a_cover_of b2 holds
for b4 being Point of b1 st b4 in b2 holds
ex b5 being Subset of b1 st
( b4 in b5 & b5 in b3 )
proof end;

theorem Th3: :: RLTOPSP1:3
for b1 being non empty LoopStr
for b2, b3 being Subset of b1
for b4, b5 being Point of b1 st b4 in b2 & b5 in b3 holds
b4 + b5 in b2 + b3
proof end;

Lemma3: for b1 being non empty TopSpace
for b2 being open Subset of b1
for b3 being Subset of b1 st b2 misses b3 holds
b2 misses Cl b3
by TSEP_1:40;

Lemma4: for b1 being non empty LoopStr
for b2 being Subset of b1
for b3, b4 being Point of b1 st b4 in b2 holds
b3 + b4 in b3 + b2
proof end;

Lemma5: for b1 being non empty LoopStr
for b2, b3 being Subset of b1 holds { (b4 + b3) where B is Point of b1 : b4 in b2 } is Subset-Family of b1
proof end;

theorem Th4: :: RLTOPSP1:4
for b1 being non empty LoopStr
for b2, b3 being Subset of b1
for b4 being Subset-Family of b1 st b4 = { (b5 + b3) where B is Point of b1 : b5 in b2 } holds
b2 + b3 = union b4
proof end;

theorem Th5: :: RLTOPSP1:5
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2 being Subset of b1 holds (0. b1) + b2 = b2
proof end;

theorem Th6: :: RLTOPSP1:6
for b1 being non empty add-associative LoopStr
for b2, b3 being Point of b1
for b4 being Subset of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4)
proof end;

theorem Th7: :: RLTOPSP1:7
for b1 being non empty add-associative LoopStr
for b2 being Point of b1
for b3, b4 being Subset of b1 holds (b2 + b3) + b4 = b2 + (b3 + b4)
proof end;

theorem Th8: :: RLTOPSP1:8
for b1 being non empty LoopStr
for b2, b3 being Subset of b1
for b4 being Point of b1 st b2 c= b3 holds
b4 + b2 c= b4 + b3
proof end;

theorem Th9: :: RLTOPSP1:9
for b1 being non empty add-associative right_zeroed right_complementable LoopStr
for b2 being Subset of b1
for b3 being Point of b1 st b3 in b2 holds
0. b1 in (- b3) + b2
proof end;

theorem Th10: :: RLTOPSP1:10
for b1 being non empty LoopStr
for b2, b3, b4 being Subset of b1 st b2 c= b3 holds
b2 + b4 c= b3 + b4
proof end;

Lemma13: for b1 being non empty LoopStr
for b2, b3, b4 being Subset of b1 st b2 c= b3 holds
b4 + b2 c= b4 + b3
proof end;

theorem Th11: :: RLTOPSP1:11
for b1 being non empty LoopStr
for b2, b3, b4, b5 being Subset of b1 st b2 c= b4 & b3 c= b5 holds
b2 + b3 c= b4 + b5
proof end;

theorem Th12: :: RLTOPSP1:12
for b1 being non empty right_zeroed LoopStr
for b2, b3 being Subset of b1 st 0. b1 in b3 holds
b2 c= b2 + b3
proof end;

theorem Th13: :: RLTOPSP1:13
for b1 being RealLinearSpace
for b2 being Real holds b2 * {(0. b1)} = {(0. b1)}
proof end;

theorem Th14: :: RLTOPSP1:14
for b1 being RealLinearSpace
for b2 being Subset of b1
for b3 being non zero Real st 0. b1 in b3 * b2 holds
0. b1 in b2
proof end;

theorem Th15: :: RLTOPSP1:15
for b1 being RealLinearSpace
for b2, b3 being Subset of b1
for b4 being non zero Real holds (b4 * b2) /\ (b4 * b3) = b4 * (b2 /\ b3)
proof end;

theorem Th16: :: RLTOPSP1:16
for b1 being non empty TopSpace
for b2 being Point of b1
for b3 being a_neighborhood of b2
for b4 being Subset of b1 st b3 c= b4 holds
b4 is a_neighborhood of b2
proof end;

definition
let c1 be RealLinearSpace;
let c2 be Subset of c1;
redefine attr a2 is convex means :Def1: :: RLTOPSP1:def 1
for b1, b2 being Point of a1
for b3 being Real st 0 <= b3 & b3 <= 1 & b1 in a2 & b2 in a2 holds
(b3 * b1) + ((1 - b3) * b2) in a2;
compatibility
( c2 is convex iff for b1, b2 being Point of c1
for b3 being Real st 0 <= b3 & b3 <= 1 & b1 in c2 & b2 in c2 holds
(b3 * b1) + ((1 - b3) * b2) in c2 )
proof end;
end;

:: deftheorem Def1 defines convex RLTOPSP1:def 1 :
for b1 being RealLinearSpace
for b2 being Subset of b1 holds
( b2 is convex iff for b3, b4 being Point of b1
for b5 being Real st 0 <= b5 & b5 <= 1 & b3 in b2 & b4 in b2 holds
(b5 * b3) + ((1 - b5) * b4) in b2 );

Lemma19: for b1 being RealLinearSpace holds conv ({} b1) = {}
proof end;

registration
let c1 be RealLinearSpace;
let c2 be empty Subset of c1;
cluster conv a2 -> empty ;
coherence
conv c2 is empty
proof end;
end;

theorem Th17: :: RLTOPSP1:17
canceled;

theorem Th18: :: RLTOPSP1:18
for b1 being RealLinearSpace
for b2 being convex Subset of b1 holds conv b2 = b2
proof end;

theorem Th19: :: RLTOPSP1:19
for b1 being RealLinearSpace
for b2 being Subset of b1
for b3 being Real holds b3 * (conv b2) = conv (b3 * b2)
proof end;

theorem Th20: :: RLTOPSP1:20
for b1 being RealLinearSpace
for b2, b3 being Subset of b1 st b2 c= b3 holds
Convex-Family b3 c= Convex-Family b2
proof end;

theorem Th21: :: RLTOPSP1:21
for b1 being RealLinearSpace
for b2, b3 being Subset of b1 st b2 c= b3 holds
conv b2 c= conv b3
proof end;

theorem Th22: :: RLTOPSP1:22
for b1 being RealLinearSpace
for b2 being convex Subset of b1
for b3 being Real st 0 <= b3 & b3 <= 1 & 0. b1 in b2 holds
b3 * b2 c= b2
proof end;

definition
let c1 be RealLinearSpace;
let c2, c3 be Point of c1;
func LSeg c2,c3 -> Subset of a1 equals :: RLTOPSP1:def 2
{ (((1 - b1) * a2) + (b1 * a3)) where B is Real : ( 0 <= b1 & b1 <= 1 ) } ;
coherence
{ (((1 - b1) * c2) + (b1 * c3)) where B is Real : ( 0 <= b1 & b1 <= 1 ) } is Subset of c1
proof end;
end;

:: deftheorem Def2 defines LSeg RLTOPSP1:def 2 :
for b1 being RealLinearSpace
for b2, b3 being Point of b1 holds LSeg b2,b3 = { (((1 - b4) * b2) + (b4 * b3)) where B is Real : ( 0 <= b4 & b4 <= 1 ) } ;

registration
let c1 be RealLinearSpace;
let c2, c3 be Point of c1;
cluster LSeg a2,a3 -> non empty convex ;
coherence
( not LSeg c2,c3 is empty & LSeg c2,c3 is convex )
proof end;
end;

theorem Th23: :: RLTOPSP1:23
for b1 being RealLinearSpace
for b2 being Subset of b1 holds
( b2 is convex iff for b3, b4 being Point of b1 st b3 in b2 & b4 in b2 holds
LSeg b3,b4 c= b2 )
proof end;

definition
let c1 be non empty RLSStruct ;
let c2 be Subset-Family of c1;
attr a2 is convex-membered means :Def3: :: RLTOPSP1:def 3
for b1 being Subset of a1 st b1 in a2 holds
b1 is convex;
end;

:: deftheorem Def3 defines convex-membered RLTOPSP1:def 3 :
for b1 being non empty RLSStruct
for b2 being Subset-Family of b1 holds
( b2 is convex-membered iff for b3 being Subset of b1 st b3 in b2 holds
b3 is convex );

registration
let c1 be non empty RLSStruct ;
cluster non empty convex-membered Element of bool (bool the carrier of a1);
existence
ex b1 being Subset-Family of c1 st
( not b1 is empty & b1 is convex-membered )
proof end;
end;

theorem Th24: :: RLTOPSP1:24
for b1 being non empty RLSStruct
for b2 being convex-membered Subset-Family of b1 holds meet b2 is convex
proof end;

definition
let c1 be non empty RLSStruct ;
let c2 be Subset of c1;
func - c2 -> Subset of a1 equals :: RLTOPSP1:def 4
(- 1) * a2;
coherence
(- 1) * c2 is Subset of c1 ;
end;

:: deftheorem Def4 defines - RLTOPSP1:def 4 :
for b1 being non empty RLSStruct
for b2 being Subset of b1 holds - b2 = (- 1) * b2;

theorem Th25: :: RLTOPSP1:25
for b1 being RealLinearSpace
for b2, b3 being Subset of b1
for b4 being Point of b1 holds
( b4 + b2 meets b3 iff b4 in b3 + (- b2) )
proof end;

definition
let c1 be non empty RLSStruct ;
let c2 be Subset of c1;
attr a2 is symmetric means :Def5: :: RLTOPSP1:def 5
a2 = - a2;
end;

:: deftheorem Def5 defines symmetric RLTOPSP1:def 5 :
for b1 being non empty RLSStruct
for b2 being Subset of b1 holds
( b2 is symmetric iff b2 = - b2 );

registration
let c1 be RealLinearSpace;
cluster non empty symmetric Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st
( not b1 is empty & b1 is symmetric )
proof end;
end;

theorem Th26: :: RLTOPSP1:26
for b1 being RealLinearSpace
for b2 being symmetric Subset of b1
for b3 being Point of b1 st b3 in b2 holds
- b3 in b2
proof end;

definition
let c1 be non empty RLSStruct ;
let c2 be Subset of c1;
attr a2 is circled means :Def6: :: RLTOPSP1:def 6
for b1 being Real st abs b1 <= 1 holds
b1 * a2 c= a2;
end;

:: deftheorem Def6 defines circled RLTOPSP1:def 6 :
for b1 being non empty RLSStruct
for b2 being Subset of b1 holds
( b2 is circled iff for b3 being Real st abs b3 <= 1 holds
b3 * b2 c= b2 );

Lemma28: for b1 being non empty RLSStruct holds {} b1 is circled
proof end;

registration
let c1 be non empty RLSStruct ;
cluster {} a1 -> circled ;
coherence
{} c1 is circled by Lemma28;
end;

theorem Th27: :: RLTOPSP1:27
for b1 being RealLinearSpace holds {(0. b1)} is circled
proof end;

registration
let c1 be RealLinearSpace;
cluster non empty circled Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st
( not b1 is empty & b1 is circled )
proof end;
end;

theorem Th28: :: RLTOPSP1:28
for b1 being RealLinearSpace
for b2 being non empty circled Subset of b1 holds 0. b1 in b2
proof end;

Lemma31: for b1 being RealLinearSpace
for b2, b3 being circled Subset of b1 holds b2 + b3 is circled
proof end;

registration
let c1 be RealLinearSpace;
let c2, c3 be circled Subset of c1;
cluster a2 + a3 -> circled ;
coherence
c2 + c3 is circled by Lemma31;
end;

theorem Th29: :: RLTOPSP1:29
for b1 being RealLinearSpace
for b2 being circled Subset of b1
for b3 being Real st abs b3 = 1 holds
b3 * b2 = b2
proof end;

Lemma33: for b1 being RealLinearSpace
for b2 being circled Subset of b1 holds b2 is symmetric
proof end;

registration
let c1 be RealLinearSpace;
cluster circled -> symmetric Element of bool the carrier of a1;
coherence
for b1 being Subset of c1 st b1 is circled holds
b1 is symmetric by Lemma33;
end;

Lemma34: for b1 being RealLinearSpace
for b2 being circled Subset of b1 holds conv b2 is circled
proof end;

registration
let c1 be RealLinearSpace;
let c2 be circled Subset of c1;
cluster conv a2 -> symmetric circled ;
coherence
conv c2 is circled by Lemma34;
end;

definition
let c1 be non empty RLSStruct ;
let c2 be Subset-Family of c1;
attr a2 is circled-membered means :Def7: :: RLTOPSP1:def 7
for b1 being Subset of a1 st b1 in a2 holds
b1 is circled;
end;

:: deftheorem Def7 defines circled-membered RLTOPSP1:def 7 :
for b1 being non empty RLSStruct
for b2 being Subset-Family of b1 holds
( b2 is circled-membered iff for b3 being Subset of b1 st b3 in b2 holds
b3 is circled );

registration
let c1 be non empty RLSStruct ;
cluster non empty circled-membered Element of bool (bool the carrier of a1);
existence
ex b1 being Subset-Family of c1 st
( not b1 is empty & b1 is circled-membered )
proof end;
end;

theorem Th30: :: RLTOPSP1:30
for b1 being non empty RLSStruct
for b2 being circled-membered Subset-Family of b1 holds union b2 is circled
proof end;

theorem Th31: :: RLTOPSP1:31
for b1 being non empty RLSStruct
for b2 being circled-membered Subset-Family of b1 holds meet b2 is circled
proof end;

definition
attr a1 is strict;
struct RLTopStruct -> RLSStruct , TopStruct ;
aggr RLTopStruct(# carrier, Zero, add, Mult, topology #) -> RLTopStruct ;
end;

registration
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be BinOp of c1;
let c4 be Function of [:REAL ,c1:],c1;
let c5 be Subset-Family of c1;
cluster RLTopStruct(# a1,a2,a3,a4,a5 #) -> non empty ;
coherence
not RLTopStruct(# c1,c2,c3,c4,c5 #) is empty by STRUCT_0:def 1;
end;

registration
cluster non empty strict RLTopStruct ;
existence
ex b1 being RLTopStruct st
( b1 is strict & not b1 is empty )
proof end;
end;

definition
let c1 be non empty RLTopStruct ;
attr a1 is add-continuous means :Def8: :: RLTOPSP1:def 8
for b1, b2 being Point of a1
for b3 being Subset of a1 st b3 is open & b1 + b2 in b3 holds
ex b4, b5 being Subset of a1 st
( b4 is open & b5 is open & b1 in b4 & b2 in b5 & b4 + b5 c= b3 );
attr a1 is Mult-continuous means :Def9: :: RLTOPSP1:def 9
for b1 being Real
for b2 being Point of a1
for b3 being Subset of a1 st b3 is open & b1 * b2 in b3 holds
ex b4 being positive Realex b5 being Subset of a1 st
( b5 is open & b2 in b5 & ( for b6 being Real st abs (b6 - b1) < b4 holds
b6 * b5 c= b3 ) );
end;

:: deftheorem Def8 defines add-continuous RLTOPSP1:def 8 :
for b1 being non empty RLTopStruct holds
( b1 is add-continuous iff for b2, b3 being Point of b1
for b4 being Subset of b1 st b4 is open & b2 + b3 in b4 holds
ex b5, b6 being Subset of b1 st
( b5 is open & b6 is open & b2 in b5 & b3 in b6 & b5 + b6 c= b4 ) );

:: deftheorem Def9 defines Mult-continuous RLTOPSP1:def 9 :
for b1 being non empty RLTopStruct holds
( b1 is Mult-continuous iff for b2 being Real
for b3 being Point of b1
for b4 being Subset of b1 st b4 is open & b2 * b3 in b4 holds
ex b5 being positive Realex b6 being Subset of b1 st
( b6 is open & b3 in b6 & ( for b7 being Real st abs (b7 - b2) < b5 holds
b7 * b6 c= b4 ) ) );

registration
cluster non empty TopSpace-like Abelian add-associative right_zeroed right_complementable RealLinearSpace-like strict add-continuous Mult-continuous RLTopStruct ;
existence
ex b1 being non empty RLTopStruct st
( b1 is strict & b1 is add-continuous & b1 is Mult-continuous & b1 is TopSpace-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is RealLinearSpace-like )
proof end;
end;

definition
mode LinearTopSpace is non empty TopSpace-like Abelian add-associative right_zeroed right_complementable RealLinearSpace-like add-continuous Mult-continuous RLTopStruct ;
end;

theorem Th32: :: RLTOPSP1:32
for b1 being LinearTopSpace
for b2, b3 being Point of b1
for b4 being a_neighborhood of b2 + b3 ex b5 being a_neighborhood of b2ex b6 being a_neighborhood of b3 st b5 + b6 c= b4
proof end;

theorem Th33: :: RLTOPSP1:33
for b1 being LinearTopSpace
for b2 being Real
for b3 being Point of b1
for b4 being a_neighborhood of b2 * b3 ex b5 being positive Realex b6 being a_neighborhood of b3 st
for b7 being Real st abs (b7 - b2) < b5 holds
b7 * b6 c= b4
proof end;

definition
let c1 be non empty RLTopStruct ;
let c2 be Point of c1;
func transl c2,c1 -> Function of a1,a1 means :Def10: :: RLTOPSP1:def 10
for b1 being Point of a1 holds a3 . b1 = a2 + b1;
existence
ex b1 being Function of c1,c1 st
for b2 being Point of c1 holds b1 . b2 = c2 + b2
proof end;
uniqueness
for b1, b2 being Function of c1,c1 st ( for b3 being Point of c1 holds b1 . b3 = c2 + b3 ) & ( for b3 being Point of c1 holds b2 . b3 = c2 + b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines transl RLTOPSP1:def 10 :
for b1 being non empty RLTopStruct
for b2 being Point of b1
for b3 being Function of b1,b1 holds
( b3 = transl b2,b1 iff for b4 being Point of b1 holds b3 . b4 = b2 + b4 );

theorem Th34: :: RLTOPSP1:34
for b1 being non empty RLTopStruct
for b2 being Point of b1
for b3 being Subset of b1 holds (transl b2,b1) .: b3 = b2 + b3
proof end;

theorem Th35: :: RLTOPSP1:35
for b1 being LinearTopSpace
for b2 being Point of b1 holds rng (transl b2,b1) = [#] b1
proof end;

Lemma43: for b1 being LinearTopSpace
for b2 being Point of b1 holds transl b2,b1 is one-to-one
proof end;

theorem Th36: :: RLTOPSP1:36
for b1 being LinearTopSpace
for b2 being Point of b1 holds (transl b2,b1) " = transl (- b2),b1
proof end;

Lemma45: for b1 being LinearTopSpace
for b2 being Point of b1 holds transl b2,b1 is continuous
proof end;

registration
let c1 be LinearTopSpace;
let c2 be Point of c1;
cluster transl a2,a1 -> being_homeomorphism ;
coherence
transl c2,c1 is being_homeomorphism
proof end;
end;

Lemma46: for b1 being LinearTopSpace
for b2 being Subset of b1
for b3 being Point of b1 st b2 is open holds
b3 + b2 is open
proof end;

registration
let c1 be LinearTopSpace;
let c2 be open Subset of c1;
let c3 be Point of c1;
cluster a3 + a2 -> open ;
coherence
c3 + c2 is open by Lemma46;
end;

Lemma47: for b1 being LinearTopSpace
for b2 being open Subset of b1
for b3 being Subset of b1 holds b3 + b2 is open
proof end;

registration
let c1 be LinearTopSpace;
let c2 be open Subset of c1;
let c3 be Subset of c1;
cluster a3 + a2 -> open ;
coherence
c3 + c2 is open by Lemma47;
end;

Lemma48: for b1 being LinearTopSpace
for b2 being closed Subset of b1
for b3 being Point of b1 holds b3 + b2 is closed
proof end;

registration
let c1 be LinearTopSpace;
let c2 be closed Subset of c1;
let c3 be Point of c1;
cluster a3 + a2 -> closed ;
coherence
c3 + c2 is closed by Lemma48;
end;

theorem Th37: :: RLTOPSP1:37
for b1 being LinearTopSpace
for b2, b3, b4 being Subset of b1 st b2 + b3 c= b4 holds
(Int b2) + (Int b3) c= Int b4
proof end;

theorem Th38: :: RLTOPSP1:38
for b1 being LinearTopSpace
for b2 being Point of b1
for b3 being Subset of b1 holds b2 + (Int b3) = Int (b2 + b3)
proof end;

theorem Th39: :: RLTOPSP1:39
for b1 being LinearTopSpace
for b2 being Point of b1
for b3 being Subset of b1 holds b2 + (Cl b3) = Cl (b2 + b3)
proof end;

theorem Th40: :: RLTOPSP1:40
for b1 being LinearTopSpace
for b2, b3 being Point of b1
for b4 being a_neighborhood of b2 holds b3 + b4 is a_neighborhood of b3 + b2
proof end;

theorem Th41: :: RLTOPSP1:41
for b1 being LinearTopSpace
for b2 being Point of b1
for b3 being a_neighborhood of b2 holds (- b2) + b3 is a_neighborhood of 0. b1
proof end;

definition
let c1 be non empty RLTopStruct ;
mode local_base of a1 is basis of 0. a1;
end;

definition
let c1 be non empty RLTopStruct ;
attr a1 is locally-convex means :Def11: :: RLTOPSP1:def 11
ex b1 being local_base of a1 st b1 is convex-membered;
end;

:: deftheorem Def11 defines locally-convex RLTOPSP1:def 11 :
for b1 being non empty RLTopStruct holds
( b1 is locally-convex iff ex b2 being local_base of b1 st b2 is convex-membered );

definition
let c1 be LinearTopSpace;
let c2 be Subset of c1;
attr a2 is bounded means :Def12: :: RLTOPSP1:def 12
for b1 being a_neighborhood of 0. a1 ex b2 being Real st
( b2 > 0 & ( for b3 being Real st b3 > b2 holds
a2 c= b3 * b1 ) );
end;

:: deftheorem Def12 defines bounded RLTOPSP1:def 12 :
for b1 being LinearTopSpace
for b2 being Subset of b1 holds
( b2 is bounded iff for b3 being a_neighborhood of 0. b1 ex b4 being Real st
( b4 > 0 & ( for b5 being Real st b5 > b4 holds
b2 c= b5 * b3 ) ) );

registration
let c1 be LinearTopSpace;
cluster {} a1 -> symmetric circled bounded ;
coherence
{} c1 is bounded
proof end;
end;

registration
let c1 be LinearTopSpace;
cluster bounded Element of bool the carrier of a1;
existence
ex b1 being Subset of c1 st b1 is bounded
proof end;
end;

theorem Th42: :: RLTOPSP1:42
for b1 being LinearTopSpace
for b2, b3 being bounded Subset of b1 holds b2 \/ b3 is bounded
proof end;

theorem Th43: :: RLTOPSP1:43
for b1 being LinearTopSpace
for b2 being bounded Subset of b1
for b3 being Subset of b1 st b3 c= b2 holds
b3 is bounded
proof end;

theorem Th44: :: RLTOPSP1:44
for b1 being LinearTopSpace
for b2 being Subset-Family of b1 st b2 is finite & b2 = { b3 where B is bounded Subset of b1 : verum } holds
union b2 is bounded
proof end;

theorem Th45: :: RLTOPSP1:45
for b1 being LinearTopSpace
for b2 being Subset-Family of b1 st b2 = { b3 where B is a_neighborhood of 0. b1 : verum } holds
b2 is local_base of b1
proof end;

theorem Th46: :: RLTOPSP1:46
for b1 being LinearTopSpace
for b2 being local_base of b1
for b3 being Subset-Family of b1 st b3 = { (b4 + b5) where B is Point of b1, B is Subset of b1 : b5 in b2 } holds
b3 is basis of b1
proof end;

definition
let c1 be non empty RLTopStruct ;
let c2 be Real;
func mlt c2,c1 -> Function of a1,a1 means :Def13: :: RLTOPSP1:def 13
for b1 being Point of a1 holds a3 . b1 = a2 * b1;
existence
ex b1 being Function of c1,c1 st
for b2 being Point of c1 holds b1 . b2 = c2 * b2
proof end;
uniqueness
for b1, b2 being Function of c1,c1 st ( for b3 being Point of c1 holds b1 . b3 = c2 * b3 ) & ( for b3 being Point of c1 holds b2 . b3 = c2 * b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines mlt RLTOPSP1:def 13 :
for b1 being non empty RLTopStruct
for b2 being Real
for b3 being Function of b1,b1 holds
( b3 = mlt b2,b1 iff for b4 being Point of b1 holds b3 . b4 = b2 * b4 );

theorem Th47: :: RLTOPSP1:47
for b1 being non empty RLTopStruct
for b2 being Subset of b1
for b3 being non zero Real holds (mlt b3,b1) .: b2 = b3 * b2
proof end;

theorem Th48: :: RLTOPSP1:48
for b1 being LinearTopSpace
for b2 being non zero Real holds rng (mlt b2,b1) = [#] b1
proof end;

Lemma58: for b1 being LinearTopSpace
for b2 being non zero Real holds mlt b2,b1 is one-to-one
proof end;

theorem Th49: :: RLTOPSP1:49
for b1 being LinearTopSpace
for b2 being non zero Real holds (mlt b2,b1) " = mlt (b2 " ),b1
proof end;

Lemma60: for b1 being LinearTopSpace
for b2 being non zero Real holds mlt b2,b1 is continuous
proof end;

registration
let c1 be LinearTopSpace;
let c2 be non zero Real;
cluster mlt a2,a1 -> being_homeomorphism ;
coherence
mlt c2,c1 is being_homeomorphism
proof end;
end;

theorem Th50: :: RLTOPSP1:50
for b1 being LinearTopSpace
for b2 being open Subset of b1
for b3 being non zero Real holds b3 * b2 is open
proof end;

theorem Th51: :: RLTOPSP1:51
for b1 being LinearTopSpace
for b2 being closed Subset of b1
for b3 being non zero Real holds b3 * b2 is closed
proof end;

theorem Th52: :: RLTOPSP1:52
for b1 being LinearTopSpace
for b2 being Subset of b1
for b3 being non zero Real holds b3 * (Int b2) = Int (b3 * b2)
proof end;

theorem Th53: :: RLTOPSP1:53
for b1 being LinearTopSpace
for b2 being Subset of b1
for b3 being non zero Real holds b3 * (Cl b2) = Cl (b3 * b2)
proof end;

theorem Th54: :: RLTOPSP1:54
for b1 being LinearTopSpace
for b2 being Subset of b1 st b1 is being_T1 holds
0 * (Cl b2) = Cl (0 * b2)
proof end;

theorem Th55: :: RLTOPSP1:55
for b1 being LinearTopSpace
for b2 being Point of b1
for b3 being a_neighborhood of b2
for b4 being non zero Real holds b4 * b3 is a_neighborhood of b4 * b2
proof end;

theorem Th56: :: RLTOPSP1:56
for b1 being LinearTopSpace
for b2 being a_neighborhood of 0. b1
for b3 being non zero Real holds b3 * b2 is a_neighborhood of 0. b1
proof end;

Lemma67: for b1 being LinearTopSpace
for b2 being bounded Subset of b1
for b3 being Real holds b3 * b2 is bounded
proof end;

registration
let c1 be LinearTopSpace;
let c2 be bounded Subset of c1;
let c3 be Real;
cluster a3 * a2 -> bounded ;
coherence
c3 * c2 is bounded by Lemma67;
end;

theorem Th57: :: RLTOPSP1:57
for b1 being LinearTopSpace
for b2 being a_neighborhood of 0. b1 ex b3 being open a_neighborhood of 0. b1 st
( b3 is symmetric & b3 + b3 c= b2 )
proof end;

theorem Th58: :: RLTOPSP1:58
for b1 being LinearTopSpace
for b2 being compact Subset of b1
for b3 being closed Subset of b1 st b2 misses b3 holds
ex b4 being a_neighborhood of 0. b1 st b2 + b4 misses b3 + b4
proof end;

theorem Th59: :: RLTOPSP1:59
for b1 being LinearTopSpace
for b2 being local_base of b1
for b3 being a_neighborhood of 0. b1 ex b4 being a_neighborhood of 0. b1 st
( b4 in b2 & Cl b4 c= b3 )
proof end;

theorem Th60: :: RLTOPSP1:60
for b1 being LinearTopSpace
for b2 being a_neighborhood of 0. b1 ex b3 being a_neighborhood of 0. b1 st Cl b3 c= b2
proof end;

registration
cluster being_T1 -> Hausdorff RLTopStruct ;
coherence
for b1 being LinearTopSpace st b1 is being_T1 holds
b1 is being_T2
proof end;
end;

theorem Th61: :: RLTOPSP1:61
for b1 being LinearTopSpace
for b2 being Subset of b1 holds Cl b2 = meet { (b2 + b3) where B is a_neighborhood of 0. b1 : verum }
proof end;

theorem Th62: :: RLTOPSP1:62
for b1 being LinearTopSpace
for b2, b3 being Subset of b1 holds (Int b2) + (Int b3) c= Int (b2 + b3)
proof end;

theorem Th63: :: RLTOPSP1:63
for b1 being LinearTopSpace
for b2, b3 being Subset of b1 holds (Cl b2) + (Cl b3) c= Cl (b2 + b3)
proof end;

Lemma74: for b1 being LinearTopSpace
for b2 being convex Subset of b1 holds Cl b2 is convex
proof end;

registration
let c1 be LinearTopSpace;
let c2 be convex Subset of c1;
cluster Cl a2 -> convex ;
coherence
Cl c2 is convex by Lemma74;
end;

Lemma75: for b1 being LinearTopSpace
for b2 being convex Subset of b1 holds Int b2 is convex
proof end;

registration
let c1 be LinearTopSpace;
let c2 be convex Subset of c1;
cluster Int a2 -> convex ;
coherence
Int c2 is convex by Lemma75;
end;

Lemma76: for b1 being LinearTopSpace
for b2 being circled Subset of b1 holds Cl b2 is circled
proof end;

registration
let c1 be LinearTopSpace;
let c2 be circled Subset of c1;
cluster Cl a2 -> symmetric circled ;
coherence
Cl c2 is circled by Lemma76;
end;

theorem Th64: :: RLTOPSP1:64
for b1 being LinearTopSpace
for b2 being circled Subset of b1 st 0. b1 in Int b2 holds
Int b2 is circled
proof end;

Lemma77: for b1 being LinearTopSpace
for b2 being bounded Subset of b1 holds Cl b2 is bounded
proof end;

registration
let c1 be LinearTopSpace;
let c2 be bounded Subset of c1;
cluster Cl a2 -> bounded ;
coherence
Cl c2 is bounded by Lemma77;
end;

Lemma78: for b1 being LinearTopSpace
for b2, b3 being a_neighborhood of 0. b1
for b4 being Subset-Family of b1
for b5 being positive Real st ( for b6 being Real st abs b6 < b5 holds
b6 * b3 c= b2 ) & b4 = { (b6 * b3) where B is Real : abs b6 < b5 } holds
( union b4 is a_neighborhood of 0. b1 & union b4 is circled & union b4 c= b2 )
proof end;

theorem Th65: :: RLTOPSP1:65
for b1 being LinearTopSpace
for b2 being a_neighborhood of 0. b1 ex b3 being a_neighborhood of 0. b1 st
( b3 is circled & b3 c= b2 )
proof end;

theorem Th66: :: RLTOPSP1:66
for b1 being LinearTopSpace
for b2 being a_neighborhood of 0. b1 st b2 is convex holds
ex b3 being a_neighborhood of 0. b1 st
( b3 is circled & b3 is convex & b3 c= b2 )
proof end;

theorem Th67: :: RLTOPSP1:67
for b1 being LinearTopSpace ex b2 being local_base of b1 st b2 is circled-membered
proof end;

theorem Th68: :: RLTOPSP1:68
for b1 being LinearTopSpace st b1 is locally-convex holds
ex b2 being local_base of b1 st b2 is convex-membered
proof end;