let V be RealNormSpace; 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; 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; ( 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
; 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; verum