let X be RealNormSpace; :: thesis: for a being Element of REAL
for x being Point of (DualSp X)
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
a * x = a * v
let a be Element of REAL ; :: thesis: for x being Point of (DualSp X)
for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
a * x = a * v
let x be Point of (DualSp X); :: thesis: for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)) st x = v holds
a * x = a * v
let v be Point of (R_NormSpace_of_BoundedLinearOperators (X,RNS_Real)); :: thesis: ( x = v implies a * x = a * v )
assume AS: x = v ; :: thesis: a * x = a * v
reconsider z = a * x as Point of (DualSp X) ;
reconsider u = a * v 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 = a * (x . t) by DUALSP01:30
.= a * (v . t) by AS, BINOP_2:def 11 ;
hence z . t = u . t by LOPBAN_1:36; :: thesis: verum
end;
hence a * x = a * v by A5, FUNCT_2:def 1, A2; :: thesis: verum