let X be RealNormSpace; :: thesis: for V1, CL being Subset of X st CL = the carrier of (ClNLin V1) holds
RLSStruct(# CL,(Zero_ (CL,X)),(Add_ (CL,X)),(Mult_ (CL,X)) #) is Subspace of X
let V1, CL be Subset of X; :: thesis: ( CL = the carrier of (ClNLin V1) implies RLSStruct(# CL,(Zero_ (CL,X)),(Add_ (CL,X)),(Mult_ (CL,X)) #) is Subspace of X )
assume A1: CL = the carrier of (ClNLin V1) ; :: thesis: RLSStruct(# CL,(Zero_ (CL,X)),(Add_ (CL,X)),(Mult_ (CL,X)) #) is Subspace of X
consider Z being Subset of X such that
A2: ( Z = the carrier of (Lin V1) & ClNLin V1 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) by defClN;
thus RLSStruct(# CL,(Zero_ (CL,X)),(Add_ (CL,X)),(Mult_ (CL,X)) #) is Subspace of X by A1, RSSPACE:11, A2, Cl01; :: thesis: verum