let X, Y, Z be RealNormSpace; 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)); 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)); 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; ( 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;
(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
;
verum
end;
for x being Point of X holds ((r * w) * u) . x = r * ((w * u) . x)
proof
let x be
Point of
X;
((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
;
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; verum