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

( 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