let V be RealNormSpace; 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; 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; 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; 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 )
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
; ( 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
; 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
; verum