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 A1, LCL1, RLSUB134;

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 A4, DUALSP01:def 16;

A8: the addF of W = the addF of (NLin V1) by A3, A5, DUALSP01:def 16;

the normF of W = the normF of V | the carrier of W by DUALSP01:def 16

.= the normF of (NLin V1) by A2, A3, DefNorm ;

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 A6, A7, A8, DUALSP01:def 16; :: thesis: verum

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 A1, LCL1, RLSUB134;

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 A4, DUALSP01:def 16;

A8: the addF of W = the addF of (NLin V1) by A3, A5, DUALSP01:def 16;

the normF of W = the normF of V | the carrier of W by DUALSP01:def 16

.= the normF of (NLin V1) by A2, A3, DefNorm ;

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 A6, A7, A8, DUALSP01:def 16; :: thesis: verum