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

proof

let s be object ; :: thesis: ( s in dom (v1 + v2) implies (v1 + v2) . s = zw12 . s )
assume A6: s in dom (v1 + v2) ; :: thesis: (v1 + v2) . s = zw12 . s
then reconsider d = s as Point of X ;
thus (v1 + v2) . s = (v1 + v2) /. d by A5, PARTFUN1:def 6
.= (v1 /. d) + (v2 /. d) by A6, VFUNCT_1:def 1
.= zw12 . s by A1, LOPBAN_1:35 ; :: thesis: verum

end;

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

proof

let s be object ; :: thesis: ( s in dom (a (#) v1) implies (a (#) v1) . s = zw12 . s )
assume A10: s in dom (a (#) v1) ; :: thesis: (a (#) v1) . s = zw12 . s
then reconsider d = s as Point of X ;
thus (a (#) v1) . s = (a (#) v1) /. d by A9, PARTFUN1:def 6
.= a * (v1 /. d) by A10, VFUNCT_1:def 4
.= zw12 . s by A1, LOPBAN_1:36 ; :: thesis: verum

end;

hence a (#) v1 = a * w1 by A8, A9, FUNCT_1:2; :: thesis: verum