let V be RealNormSpace; :: thesis: for V1 being SubRealNormSpace of V

for x, y being Point of V

for x1, y1 being Point of V1

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

let V1 be SubRealNormSpace of V; :: thesis: for x, y being Point of V

for x1, y1 being Point of V1

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

let x, y be Point of V; :: thesis: for x1, y1 being Point of V1

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

let x1, y1 be Point of V1; :: thesis: for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

let a be Real; :: thesis: ( x = x1 & y = y1 implies ( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 ) )

assume A1: ( x = x1 & y = y1 ) ; :: thesis: ( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

reconsider aa = a as Element of REAL by XREAL_0:def 1;

thus ||.x1.|| = ( the normF of V | the carrier of V1) . x1 by DUALSP01:def 16

.= ||.x.|| by A1, FUNCT_1:49 ; :: thesis: ( x + y = x1 + y1 & a * x = a * x1 )

thus x1 + y1 = ( the addF of V || the carrier of V1) . [x1,y1] by DUALSP01:def 16

.= x + y by A1, FUNCT_1:49 ; :: thesis: a * x = a * x1

A2: [aa,x1] in [:REAL, the carrier of V1:] ;

aa * x1 = ( the Mult of V | [:REAL, the carrier of V1:]) . [a,x1] by DUALSP01:def 16

.= aa * x by A1, A2, FUNCT_1:49 ;

hence a * x = a * x1 ; :: thesis: verum

for x, y being Point of V

for x1, y1 being Point of V1

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

let V1 be SubRealNormSpace of V; :: thesis: for x, y being Point of V

for x1, y1 being Point of V1

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

let x, y be Point of V; :: thesis: for x1, y1 being Point of V1

for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

let x1, y1 be Point of V1; :: thesis: for a being Real st x = x1 & y = y1 holds

( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

let a be Real; :: thesis: ( x = x1 & y = y1 implies ( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 ) )

assume A1: ( x = x1 & y = y1 ) ; :: thesis: ( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )

reconsider aa = a as Element of REAL by XREAL_0:def 1;

thus ||.x1.|| = ( the normF of V | the carrier of V1) . x1 by DUALSP01:def 16

.= ||.x.|| by A1, FUNCT_1:49 ; :: thesis: ( x + y = x1 + y1 & a * x = a * x1 )

thus x1 + y1 = ( the addF of V || the carrier of V1) . [x1,y1] by DUALSP01:def 16

.= x + y by A1, FUNCT_1:49 ; :: thesis: a * x = a * x1

A2: [aa,x1] in [:REAL, the carrier of V1:] ;

aa * x1 = ( the Mult of V | [:REAL, the carrier of V1:]) . [a,x1] by DUALSP01:def 16

.= aa * x by A1, A2, FUNCT_1:49 ;

hence a * x = a * x1 ; :: thesis: verum