let X be RealNormSpace; for x, y being Point of (DualSp X)
for v, w being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v & y = w holds
x + y = v + w
let x, y be Point of (DualSp X); for v, w being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v & y = w holds
x + y = v + w
let v, w be Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)); ( x = v & y = w implies x + y = v + w )
assume AS:
( x = v & y = w )
; x + y = v + w
reconsider z = x + y as Point of (DualSp X) ;
reconsider u = v + w as Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) ;
BX:
R_NormSpace_of_BoundedLinearOperators (X,RNS_Real) = NORMSTR(# (BoundedLinearOperators (X,RNS_Real)),(Zero_ ((BoundedLinearOperators (X,RNS_Real)),(R_VectorSpace_of_LinearOperators (X,RNS_Real)))),(Add_ ((BoundedLinearOperators (X,RNS_Real)),(R_VectorSpace_of_LinearOperators (X,RNS_Real)))),(Mult_ ((BoundedLinearOperators (X,RNS_Real)),(R_VectorSpace_of_LinearOperators (X,RNS_Real)))),(BoundedLinearOperatorsNorm (X,RNS_Real)) #)
by LOPBAN_1:def 14;
A1:
z is additive homogeneous Lipschitzian Function of the carrier of X,REAL
by DUALSP01:def 10;
then A5:
dom z = the carrier of X
by FUNCT_2:def 1;
A2:
u is additive homogeneous Lipschitzian Function of X,RNS_Real
by LOPBAN_1:def 9, BX;
for t being object st t in dom z holds
z . t = u . t
hence
x + y = v + w
by A2, A5, FUNCT_2:def 1; verum