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

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