let X be RealBanachSpace; :: thesis: for Y being Subset of X ex Z being Subset of X st
( Z = the carrier of (Lin Y) & ClNLin Y = NLin (Cl Z) & Cl Z is linearly-closed & Cl Z <> {} )
let Y be Subset of X; :: thesis: ex Z being Subset of X st
( Z = the carrier of (Lin Y) & ClNLin Y = NLin (Cl Z) & Cl Z is linearly-closed & Cl Z <> {} )
consider Z being Subset of X such that
A1: ( Z = the carrier of (Lin Y) & ClNLin Y = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) by NORMSP_3:def 20;
A2: the carrier of (Lin (Cl Z)) = Cl Z by A1, NORMSP_3:13, NORMSP_3:31;
A3: NLin (Cl Z) = NORMSTR(# the carrier of (Lin (Cl Z)),(0. (Lin (Cl Z))), the addF of (Lin (Cl Z)), the Mult of (Lin (Cl Z)),(Norm_ ( the carrier of (Lin (Cl Z)),X)) #) ;
A4: Zero_ ((Cl Z),X) = 0. X by A1, NORMSP_3:13, RSSPACE:def 10
.= 0. (Lin (Cl Z)) by RLSUB_1:def 2 ;
A5: Add_ ((Cl Z),X) = the addF of X || (Cl Z) by A1, NORMSP_3:13, RSSPACE:def 8
.= the addF of (Lin (Cl Z)) by A2, RLSUB_1:def 2 ;
A6: Mult_ ((Cl Z),X) = the Mult of X | [:REAL,(Cl Z):] by A1, NORMSP_3:13, RSSPACE:def 9
.= the Mult of (Lin (Cl Z)) by A2, RLSUB_1:def 2 ;
Norm_ ((Cl Z),X) = Norm_ ( the carrier of (Lin (Cl Z)),X) by A1, NORMSP_3:13, NORMSP_3:31;
hence ex Z being Subset of X st
( Z = the carrier of (Lin Y) & ClNLin Y = NLin (Cl Z) & Cl Z is linearly-closed & Cl Z <> {} ) by A1, A3, A4, A5, A6, NORMSP_3:13; :: thesis: verum