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