let X be non trivial RealBanachSpace; :: thesis: for v1, v2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))
for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st v1 = w1 & v2 = w2 holds
v1 * v2 = w1 * w2
let v1, v2 be Point of (R_NormSpace_of_BoundedLinearOperators (X,X)); :: thesis: for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st v1 = w1 & v2 = w2 holds
v1 * v2 = w1 * w2
let w1, w2 be Point of (R_Normed_Algebra_of_BoundedLinearOperators X); :: thesis: ( v1 = w1 & v2 = w2 implies v1 * v2 = w1 * w2 )
set S = R_Normed_Algebra_of_BoundedLinearOperators X;
assume A1: ( v1 = w1 & v2 = w2 ) ; :: thesis: v1 * v2 = w1 * w2
reconsider zw1 = w1, zw2 = w2 as Element of BoundedLinearOperators (X,X) ;
thus v1 * v2 = zw1 * zw2 by A1
.= w1 * w2 by LOPBAN_2:def 4 ; :: thesis: verum