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

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