let X be RealNormSpace; :: thesis: for Y being Subset of X holds
( the carrier of (NLin Y) c= the carrier of (ClNLin Y) & ex Z being Subset of X st
( Z = the carrier of (NLin Y) & Cl Z = the carrier of (ClNLin Y) ) )
let Y be Subset of X; :: thesis: ( the carrier of (NLin Y) c= the carrier of (ClNLin Y) & ex Z being Subset of X st
( Z = the carrier of (NLin Y) & Cl Z = the carrier of (ClNLin Y) ) )
ex Z being Subset of X st
( 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;
hence ( the carrier of (NLin Y) c= the carrier of (ClNLin Y) & ex Z being Subset of X st
( Z = the carrier of (NLin Y) & Cl Z = the carrier of (ClNLin Y) ) ) by NORMSP_3:4; :: thesis: verum