let V be RealNormSpace; 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; 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; 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); for a being Real st x = x1 & y = y1 holds
( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 )
let a be Real; ( x = x1 & y = y1 implies ( ||.x.|| = ||.x1.|| & x + y = x1 + y1 & a * x = a * x1 ) )
assume A1:
( x = x1 & y = y1 )
; ( ||.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
; ( x + y = x1 + y1 & a * x = a * x1 )
thus x + y =
x2 + y2
by A1, RLSUB_1:13
.=
x1 + y1
; a * x = a * x1
thus a * x =
a * x2
by A1, RLSUB_1:14
.=
a * x1
; verum