let X, Y, Z be RealNormSpace; for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)
let f be Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)
let g be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)); for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)
let a, b be Real; (a * b) * (f * g) = (a * f) * (b * g)
set BLOPXY = R_NormSpace_of_BoundedLinearOperators (X,Y);
set BLOPXZ = R_NormSpace_of_BoundedLinearOperators (X,Z);
set BLOPYZ = R_NormSpace_of_BoundedLinearOperators (Y,Z);
set mf = modetrans (f,Y,Z);
set mg = modetrans (g,X,Y);
set maf = modetrans ((a * f),Y,Z);
set mbg = modetrans ((b * g),X,Y);
A1:
(modetrans ((a * f),Y,Z)) * (modetrans ((b * g),X,Y)) is Lipschitzian LinearOperator of X,Z
by LOPBAN_2:2;
then reconsider k = (modetrans ((a * f),Y,Z)) * (modetrans ((b * g),X,Y)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,Z)) by LOPBAN_1:def 9;
A2:
(modetrans (f,Y,Z)) * (modetrans (g,X,Y)) is Lipschitzian LinearOperator of X,Z
by LOPBAN_2:2;
then reconsider fg = (modetrans (f,Y,Z)) * (modetrans (g,X,Y)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,Z)) by LOPBAN_1:def 9;
reconsider ff = f as VECTOR of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) ;
reconsider gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
A3:
gg = modetrans (g,X,Y)
by LOPBAN_1:def 11;
A4:
ff = modetrans (f,Y,Z)
by LOPBAN_1:def 11;
for x being VECTOR of X holds ((modetrans ((a * f),Y,Z)) * (modetrans ((b * g),X,Y))) . x = (a * b) * (((modetrans (f,Y,Z)) * (modetrans (g,X,Y))) . x)
proof
let x be
VECTOR of
X;
((modetrans ((a * f),Y,Z)) * (modetrans ((b * g),X,Y))) . x = (a * b) * (((modetrans (f,Y,Z)) * (modetrans (g,X,Y))) . x)
set y =
b * ((modetrans (g,X,Y)) . x);
(
a * f = a * ff &
modetrans (
(a * f),
Y,
Z)
= a * f )
by LOPBAN_1:def 11;
then A5:
(modetrans ((a * f),Y,Z)) . (b * ((modetrans (g,X,Y)) . x)) = a * ((modetrans (f,Y,Z)) . (b * ((modetrans (g,X,Y)) . x)))
by A4, LOPBAN_1:36;
(
b * g = b * gg &
modetrans (
(b * g),
X,
Y)
= b * g )
by LOPBAN_1:def 11;
then A6:
(modetrans ((b * g),X,Y)) . x = b * ((modetrans (g,X,Y)) . x)
by A3, LOPBAN_1:36;
thus ((modetrans ((a * f),Y,Z)) * (modetrans ((b * g),X,Y))) . x =
(modetrans ((a * f),Y,Z)) . ((modetrans ((b * g),X,Y)) . x)
by A1, LPB2Th4
.=
a * (b * ((modetrans (f,Y,Z)) . ((modetrans (g,X,Y)) . x)))
by A5, A6, LOPBAN_1:def 5
.=
(a * b) * ((modetrans (f,Y,Z)) . ((modetrans (g,X,Y)) . x))
by RLVECT_1:def 7
.=
(a * b) * (((modetrans (f,Y,Z)) * (modetrans (g,X,Y))) . x)
by A2, LPB2Th4
;
verum
end;
hence
(a * b) * (f * g) = (a * f) * (b * g)
by LOPBAN_1:36; verum