:: Separability of Real Normed Spaces and Its Basic Properties
:: by Kazuhisa Nakasho and Noboru Endou
::
:: Received February 26, 2015
:: Copyright (c) 2015-2018 Association of Mizar Users


definition
let X be RealLinearSpace;
let A be Subset of X;
func RAT_Sums A -> Subset of X equals :: NORMSP_4:def 1
{ (Sum l) where l is Linear_Combination of A : rng l c= RAT } ;
correctness
coherence
{ (Sum l) where l is Linear_Combination of A : rng l c= RAT } is Subset of X
;
proof end;
end;

:: deftheorem defines RAT_Sums NORMSP_4:def 1 :
for X being RealLinearSpace
for A being Subset of X holds RAT_Sums A = { (Sum l) where l is Linear_Combination of A : rng l c= RAT } ;

theorem Th1: :: NORMSP_4:1
for V being RealNormSpace
for V1 being SubRealNormSpace of V holds TopSpaceNorm V1 is SubSpace of TopSpaceNorm V
proof end;

theorem Th2: :: NORMSP_4:2
for V being RealNormSpace
for V1 being SubRealNormSpace of V holds LinearTopSpaceNorm V1 is SubSpace of LinearTopSpaceNorm V
proof end;

theorem Th3: :: NORMSP_4:3
for X being RealNormSpace
for Y, Z being SubRealNormSpace of X st ex A being Subset of X st
( A = the carrier of Y & Cl A = the carrier of Z ) holds
for D0 being Subset of Y
for D being Subset of Z st D0 is dense & D0 = D holds
D is dense
proof end;

theorem Th4: :: NORMSP_4:4
for X being addLoopStr
for A, B being Subset of X ex F being Function of (A + B),[:A,B:] st F is one-to-one
proof end;

theorem Th5: :: NORMSP_4:5
for X being addLoopStr
for A, B being Subset of X st A is countable & B is countable holds
A + B is countable
proof end;

Lm6: for X being RealLinearSpace
for v being Element of the carrier of X holds RAT_Sums {v} is countable

proof end;

theorem Th7: :: NORMSP_4:6
for X being non empty addLoopStr
for A, B being Subset of X
for l1 being Linear_Combination of A
for l2 being Linear_Combination of B st A misses B holds
ex l being Linear_Combination of A \/ B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 )
proof end;

theorem Th8: :: NORMSP_4:7
for X being non empty addLoopStr
for A, B being Subset of X
for l being Linear_Combination of A \/ B ex l1 being Linear_Combination of A st
( Carrier l1 = (Carrier l) \ B & ( for x being Element of X st x in Carrier l1 holds
l1 . x = l . x ) )
proof end;

theorem Th9: :: NORMSP_4:8
for X being non empty addLoopStr
for A, B being Subset of X
for l being Linear_Combination of A \/ B st A misses B holds
ex l1 being Linear_Combination of A ex l2 being Linear_Combination of B st
( Carrier l = (Carrier l1) \/ (Carrier l2) & l = l1 + l2 & Carrier l1 = (Carrier l) \ B & Carrier