let X be non trivial RealBanachSpace; :: thesis: for v1, v2 being Lipschitzian LinearOperator of X,X
for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)
for a being Real st v1 = w1 & v2 = w2 holds
( v1 * v2 = w1 * w2 & v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
let v1, v2 be Lipschitzian LinearOperator of X,X; :: thesis: for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)
for a being Real st v1 = w1 & v2 = w2 holds
( v1 * v2 = w1 * w2 & v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
let w1, w2 be Point of (R_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: for a being Real st v1 = w1 & v2 = w2 holds
( v1 * v2 = w1 * w2 & v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
let a be Real; :: thesis: ( v1 = w1 & v2 = w2 implies ( v1 * v2 = w1 * w2 & v1 + v2 = w1 + w2 & a (#) v1 = a * w1 ) )
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
assume A1: ( v1 = w1 & v2 = w2 ) ; :: thesis: ( v1 * v2 = w1 * w2 & v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
reconsider zw1 = w1, zw2 = w2 as Element of BoundedLinearOperators (X,X) ;
( v1 = modetrans (v1,X,X) & v2 = modetrans (v2,X,X) ) by LOPBAN_1:29;
hence v1 * v2 = zw1 * zw2 by A1
.= w1 * w2 by LOPBAN_2:def 4 ;
:: thesis: ( v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )
reconsider zw1 = w1, zw2 = w2 as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
reconsider zw12 = zw1 + zw2 as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
zw12 is Lipschitzian LinearOperator of X,X by LOPBAN_1:def 9;
then A4: dom zw12 = the carrier of X by FUNCT_2:def 1;
A5: dom (v1 + v2) = (dom v1) /\ (dom v2) by VFUNCT_1:def 1
.= the carrier of X /\ (dom v2) by FUNCT_2:def 1
.= the carrier of X /\ the carrier of X by FUNCT_2:def 1
.= the carrier of X ;
for s being object st s in dom (v1 + v2) holds
(v1 + v2) . s = zw12 . s hence v1 + v2 = w1 + w2 by A4, A5, FUNCT_1:2; :: thesis: a (#) v1 = a * w1
reconsider zw12 = a * zw1 as Point of (R_NormSpace_of_BoundedLinearOperators (X,X)) ;
zw12 is Lipschitzian LinearOperator of X,X by LOPBAN_1:def 9;
then A8: dom zw12 = the carrier of X by FUNCT_2:def 1;
A9: dom (a (#) v1) = dom v1 by VFUNCT_1:def 4
.= the carrier of X by FUNCT_2:def 1 ;
for s being object st s in dom (a (#) v1) holds
(a (#) v1) . s = zw12 . s hence a (#) v1 = a * w1 by A8, A9, FUNCT_1:2; :: thesis: verum