let X be NormedLinearTopSpace; :: thesis: for RNS being RealNormSpace st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) holds
for x, y being Point of X
for x1, y1 being Point of RNS
for a being Real st x1 = x & y1 = y holds
( x + y = x1 + y1 & a * x = a * x1 & x - y = x1 - y1 & ||.x.|| = ||.x1.|| )
let RNS be RealNormSpace; :: thesis: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) implies for x, y being Point of X
for x1, y1 being Point of RNS
for a being Real st x1 = x & y1 = y holds
( x + y = x1 + y1 & a * x = a * x1 & x - y = x1 - y1 & ||.x.|| = ||.x1.|| ) )
assume A1: RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) ; :: thesis: for x, y being Point of X
for x1, y1 being Point of RNS
for a being Real st x1 = x & y1 = y holds
( x + y = x1 + y1 & a * x = a * x1 & x - y = x1 - y1 & ||.x.|| = ||.x1.|| )
let x, y be Point of X; :: thesis: for x1, y1 being Point of RNS
for a being Real st x1 = x & y1 = y holds
( x + y = x1 + y1 & a * x = a * x1 & x - y = x1 - y1 & ||.x.|| = ||.x1.|| )
let x1, y1 be Point of RNS; :: thesis: for a being Real st x1 = x & y1 = y holds
( x + y = x1 + y1 & a * x = a * x1 & x - y = x1 - y1 & ||.x.|| = ||.x1.|| )
let a be Real; :: thesis: ( x1 = x & y1 = y implies ( x + y = x1 + y1 & a * x = a * x1 & x - y = x1 - y1 & ||.x.|| = ||.x1.|| ) )
assume A2: ( x1 = x & y1 = y ) ; :: thesis: ( x + y = x1 + y1 & a * x = a * x1 & x - y = x1 - y1 & ||.x.|| = ||.x1.|| )
hence x + y = x1 + y1 by A1; :: thesis: ( a * x = a * x1 & x - y = x1 - y1 & ||.x.|| = ||.x1.|| )
thus a * x = a * x1 by A1, A2; :: thesis: ( x - y = x1 - y1 & ||.x.|| = ||.x1.|| )
thus x - y = x + ((- 1) * y) by RLVECT_1:16
.= x1 + ((- 1) * y1) by A1, A2
.= x1 - y1 by RLVECT_1:16 ; :: thesis: ||.x.|| = ||.x1.||
thus ||.x.|| = ||.x1.|| by A1, A2; :: thesis: verum