let V be RealNormSpace; for W being SubRealNormSpace of V st the carrier of W = the carrier of V holds
NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #) = NORMSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the normF of V #)
let W be SubRealNormSpace of V; ( the carrier of W = the carrier of V implies NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #) = NORMSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the normF of V #) )
assume A1:
the carrier of W = the carrier of V
; NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #) = NORMSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the normF of V #)
A2:
0. W = 0. V
by DUALSP01:def 16;
A3: the addF of W =
the addF of V || the carrier of W
by DUALSP01:def 16
.=
the addF of V
by A1
;
A4: the Mult of W =
the Mult of V | [:REAL, the carrier of W:]
by DUALSP01:def 16
.=
the Mult of V
by A1
;
the normF of W =
the normF of V | the carrier of W
by DUALSP01:def 16
.=
the normF of V
by A1
;
hence
NORMSTR(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W, the normF of W #) = NORMSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the normF of V #)
by A2, A3, A4; verum