let V be RealNormSpace; :: thesis: for V1 being Subset of V holds ClNLin V1 is RealNormSpace
let V1 be Subset of V; :: thesis: ClNLin V1 is RealNormSpace
set l = ClNLin V1;
consider Z being Subset of V such that
A1: ( Z = the carrier of (Lin V1) & ClNLin V1 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),V)),(Add_ ((Cl Z),V)),(Mult_ ((Cl Z),V)),(Norm_ ((Cl Z),V)) #) ) by defClN;
reconsider W = RLSStruct(# the carrier of (ClNLin V1), the ZeroF of (ClNLin V1), the addF of (ClNLin V1), the Mult of (ClNLin V1) #) as Subspace of V by A1, RSSPACE11;
W is RealLinearSpace ;
hence ClNLin V1 is RealNormSpace by RSSPACE3:2; :: thesis: verum