let X, Y, Z be RealNormSpace; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for r being Real holds
( w * (r * u) = (r * w) * u & (r * w) * u = (r * w) * u & (r * w) * u = r * (w * u) )
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for r being Real holds
( w * (r * u) = (r * w) * u & (r * w) * u = (r * w) * u & (r * w) * u = r * (w * u) )
let w be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: for r being Real holds
( w * (r * u) = (r * w) * u & (r * w) * u = (r * w) * u & (r * w) * u = r * (w * u) )
let r be Real; :: thesis: ( w * (r * u) = (r * w) * u & (r * w) * u = (r * w) * u & (r * w) * u = r * (w * u) )
A3: for x being Point of X holds (w * (r * u)) . x = r * ((w * u) . x)

proof

let x be Point of X; :: thesis: (w * (r * u)) . x = r * ((w * u) . x)
thus (w * (r * u)) . x = (modetrans (w,Y,Z)) . ((modetrans ((r * u),X,Y)) . x) by FUNCT_2:15
.= (modetrans (w,Y,Z)) . ((r * u) . x) by LOPBAN_1:def 11
.= (modetrans (w,Y,Z)) . (r * (u . x)) by LOPBAN_1:36
.= r * ((modetrans (w,Y,Z)) . (u . x)) by LOPBAN_1:def 5
.= r * ((modetrans (w,Y,Z)) . ((modetrans (u,X,Y)) . x)) by LOPBAN_1:def 11
.= r * ((w * u) . x) by FUNCT_2:15 ; :: thesis: verum

end;

for x being Point of X holds ((r * w) * u) . x = r * ((w * u) . x)

proof

let x be Point of X; :: thesis: ((r * w) * u) . x = r * ((w * u) . x)
thus ((r * w) * u) . x = (modetrans ((r * w),Y,Z)) . ((modetrans (u,X,Y)) . x) by FUNCT_2:15
.= (r * w) . ((modetrans (u,X,Y)) . x) by LOPBAN_1:def 11
.= r * (w . ((modetrans (u,X,Y)) . x)) by LOPBAN_1:36
.= r * ((modetrans (w,Y,Z)) . ((modetrans (u,X,Y)) . x)) by LOPBAN_1:def 11
.= r * ((w * u) . x) by FUNCT_2:15 ; :: thesis: verum

end;

then (r * w) * u = r * (w * u) by LOPBAN_1:36;
hence ( w * (r * u) = (r * w) * u & (r * w) * u = (r * w) * u & (r * w) * u = r * (w * u) ) by A3, LOPBAN_1:36; :: thesis: verum