let X, Y be RealNormSpace; :: thesis: for v being Lipschitzian LinearOperator of X,Y
for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real st v = w holds
a * w = a (#) v
let v be Lipschitzian LinearOperator of X,Y; :: thesis: for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real st v = w holds
a * w = a (#) v
let w be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for a being Real st v = w holds
a * w = a (#) v
let a be Real; :: thesis: ( v = w implies a * w = a (#) v )
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
assume A1: v = w ; :: thesis: a * w = a (#) v
a * w is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
then A3: dom (a * w) = the carrier of X by FUNCT_2:def 1;
A4: dom (a (#) v) = dom v by VFUNCT_1:def 4
.= the carrier of X by FUNCT_2:def 1 ;
for s being object st s in dom (a (#) v) holds
(a (#) v) . s = (a * w) . s
proof
let s be object ; :: thesis: ( s in dom (a (#) v) implies (a (#) v) . s = (a * w) . s )
assume A5: s in dom (a (#) v) ; :: thesis: (a (#) v) . s = (a * w) . s
then reconsider d = s as Point of X ;
thus (a (#) v) . s = (a (#) v) /. d by A4, PARTFUN1:def 6
.= a * (v /. d) by A5, VFUNCT_1:def 4
.= (a * w) . s by A1, LOPBAN_1:36 ; :: thesis: verum
end;
hence a (#) v = a * w by A3, A4, FUNCT_1:2; :: thesis: verum