let V be RealNormSpace; :: thesis: for V1 being Subset of V
for x, y being Point of V
for x1, y1 being Point of (NLin 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 (NLin 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 (NLin 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 (NLin 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 = NLin V1;
A2: the carrier of (NLin V1) c= the carrier of V by RLSUB_1:def 2;
reconsider x2 = x1 as Point of (Lin V1) ;
reconsider y2 = y1 as Point of (Lin V1) ;
thus ||.x1.|| = ( the normF of V | the carrier of (NLin V1)) . x1 by A2, DefNorm
.= ||.x.|| by A1, FUNCT_1:49 ; :: thesis: ( x + y = x1 + y1 & a * x = a * x1 )
thus x1 + y1 = x2 + y2
.= x + y by A1, RLSUB_1:13 ; :: thesis: a * x = a * x1
thus a * x1 = a * x2
.= a * x by A1, RLSUB_1:14 ; :: thesis: verum