let X be RealNormSpace; :: thesis: 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); :: thesis: 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)); :: thesis: ( x = v & y = w implies x + y = v + w )
assume AS: ( x = v & y = w ) ; :: thesis: 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

proof

let t be object ; :: thesis: ( t in dom z implies z . t = u . t )
assume t in dom z ; :: thesis: z . t = u . t
then reconsider t = t as VECTOR of X by FUNCT_2:def 1, A1;
z . t = (x . t) + (y . t) by DUALSP01:29
.= (v . t) + (w . t) by AS, BINOP_2:def 9 ;
hence z . t = u . t by LOPBAN_1:35; :: thesis: verum

end;

hence x + y = v + w by A2, A5, FUNCT_2:def 1; :: thesis: verum