let V be RealNormSpace; :: thesis: for V1 being Subset of V holds ClNLin V1 is SubRealNormSpace of V
let V1 be Subset of V; :: thesis: ClNLin V1 is SubRealNormSpace of V
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 CL = Cl Z as Subset of V ;
A3: 0. (ClNLin V1) = 0. V by A1, Cl01, RSSPACE:def 10;
A4: the addF of (ClNLin V1) = the addF of V || the carrier of (ClNLin V1) by A1, Cl01, RSSPACE:def 8;
A5: the Mult of (ClNLin V1) = the Mult of V | [:REAL, the carrier of (ClNLin V1):] by A1, Cl01, RSSPACE:def 9;
the normF of (ClNLin V1) = the normF of V | the carrier of (ClNLin V1) by A1, DefNorm;
hence ClNLin V1 is SubRealNormSpace of V by A1, A3, A4, A5, DUALSP01:def 16; :: thesis: verum