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

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