let V be RealNormSpace; :: thesis: for W being SubRealNormSpace of V
for V1 being Subset of V st the carrier of W = V1 holds
NLin V1 = NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #)

let W be SubRealNormSpace of V; :: thesis: for V1 being Subset of V st the carrier of W = V1 holds
NLin V1 = NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #)

let V1 be Subset of V; :: thesis: ( the carrier of W = V1 implies NLin V1 = NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #) )
assume A1: the carrier of W = V1 ; :: thesis: NLin V1 = NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #)
set l = NLin V1;
A2: the carrier of (NLin V1) c= the carrier of V by RLSUB_1:def 2;
A3: the carrier of (NLin V1) = the carrier of W by ;
A4: 0. (NLin V1) = 0. V by RLSUB_1:def 2;
A5: the addF of (NLin V1) = the addF of V || the carrier of (NLin V1) by RLSUB_1:def 2;
A6: the Mult of (NLin V1) = the Mult of V | [:REAL, the carrier of (NLin V1):] by RLSUB_1:def 2;
A7: 0. W = 0. (NLin V1) by ;
A8: the addF of W = the addF of (NLin V1) by ;
the normF of W = the normF of V | the carrier of W by DUALSP01:def 16
.= the normF of (NLin V1) by ;
hence NLin V1 = NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #) by ; :: thesis: verum