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

for x, y being Point of V

for x1, y1 being Point of (ClNLin V1)

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

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

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

for x1, y1 being Point of (ClNLin 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 (ClNLin 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 (ClNLin 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 )

set l = ClNLin V1;

consider Z being Subset of V such that

A2: ( Z = the carrier of (Lin V1) & ClNLin V1 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),V)),(Add_ ((Cl Z),V)),(Mult_ ((Cl Z),V)),(Norm_ ((Cl Z),V)) #) ) by defClN;

reconsider W = RLSStruct(# the carrier of (ClNLin V1), the ZeroF of (ClNLin V1), the addF of (ClNLin V1), the Mult of (ClNLin V1) #) as Subspace of V by A2, RSSPACE11;

reconsider x2 = x1, y2 = y1 as Point of W ;

thus ||.x1.|| = ( the normF of V | (Cl Z)) . x1 by A2, DefNorm

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

thus x + y = x2 + y2 by A1, RLSUB_1:13

.= x1 + y1 ; :: thesis: a * x = a * x1

thus a * x = a * x2 by A1, RLSUB_1:14

.= a * x1 ; :: thesis: verum

for x, y being Point of V

for x1, y1 being Point of (ClNLin V1)

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

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

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

for x1, y1 being Point of (ClNLin 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 (ClNLin 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 (ClNLin 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 )

set l = ClNLin V1;

consider Z being Subset of V such that

A2: ( Z = the carrier of (Lin V1) & ClNLin V1 = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),V)),(Add_ ((Cl Z),V)),(Mult_ ((Cl Z),V)),(Norm_ ((Cl Z),V)) #) ) by defClN;

reconsider W = RLSStruct(# the carrier of (ClNLin V1), the ZeroF of (ClNLin V1), the addF of (ClNLin V1), the Mult of (ClNLin V1) #) as Subspace of V by A2, RSSPACE11;

reconsider x2 = x1, y2 = y1 as Point of W ;

thus ||.x1.|| = ( the normF of V | (Cl Z)) . x1 by A2, DefNorm

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

thus x + y = x2 + y2 by A1, RLSUB_1:13

.= x1 + y1 ; :: thesis: a * x = a * x1

thus a * x = a * x2 by A1, RLSUB_1:14

.= a * x1 ; :: thesis: verum