let X be RealNormSpace; :: thesis: for f, g, h being Element of BoundedLinearOperators X,X holds (g + h) * f = (g * f) + (h * f)
let f, g, h be Element of BoundedLinearOperators X,X; :: thesis: (g + h) * f = (g * f) + (h * f)
set BLOP = R_NormSpace_of_BoundedLinearOperators X,X;
set ADD = Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X);
set mf = modetrans f,X,X;
set mg = modetrans g,X,X;
set mh = modetrans h,X,X;
set mgh = modetrans (g + h),X,X;
(Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . ((modetrans g,X,X) * (modetrans f,X,X)),((modetrans h,X,X) * (modetrans f,X,X)) = (modetrans (g + h),X,X) * (modetrans f,X,X)

proof

reconsider hf = (modetrans h,X,X) * (modetrans f,X,X) as VECTOR of (R_NormSpace_of_BoundedLinearOperators X,X) by LOPBAN_1:def 10;
reconsider gf = (modetrans g,X,X) * (modetrans f,X,X) as VECTOR of (R_NormSpace_of_BoundedLinearOperators X,X) by LOPBAN_1:def 10;
reconsider k = (modetrans (g + h),X,X) * (modetrans f,X,X) as VECTOR of (R_NormSpace_of_BoundedLinearOperators X,X) by LOPBAN_1:def 10;
reconsider hh = h as VECTOR of (R_NormSpace_of_BoundedLinearOperators X,X) ;
reconsider gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators X,X) ;
A1: ( gg = modetrans g,X,X & hh = modetrans h,X,X ) by LOPBAN_1:def 12;
for x being VECTOR of X holds ((modetrans (g + h),X,X) * (modetrans f,X,X)) . x = (((modetrans g,X,X) * (modetrans f,X,X)) . x) + (((modetrans h,X,X) * (modetrans f,X,X)) . x)

proof

let x be VECTOR of X; :: thesis: ((modetrans (g + h),X,X) * (modetrans f,X,X)) . x = (((modetrans g,X,X) * (modetrans f,X,X)) . x) + (((modetrans h,X,X) * (modetrans f,X,X)) . x)
( g + h = gg + hh & modetrans (g + h),X,X = g + h ) by LOPBAN_1:def 12;
then A2: (modetrans (g + h),X,X) . ((modetrans f,X,X) . x) = ((modetrans g,X,X) . ((modetrans f,X,X) . x)) + ((modetrans h,X,X) . ((modetrans f,X,X) . x)) by A1, LOPBAN_1:41;
thus ((modetrans (g + h),X,X) * (modetrans f,X,X)) . x = (modetrans (g + h),X,X) . ((modetrans f,X,X) . x) by Th4
.= (((modetrans g,X,X) * (modetrans f,X,X)) . x) + ((modetrans h,X,X) . ((modetrans f,X,X) . x)) by A2, Th4
.= (((modetrans g,X,X) * (modetrans f,X,X)) . x) + (((modetrans h,X,X) * (modetrans f,X,X)) . x) by Th4 ; :: thesis: verum

end;

then k = gf + hf by LOPBAN_1:41;
hence (Add_ (BoundedLinearOperators X,X),(R_VectorSpace_of_LinearOperators X,X)) . ((modetrans g,X,X) * (modetrans f,X,X)),((modetrans h,X,X) * (modetrans f,X,X)) = (modetrans (g + h),X,X) * (modetrans f,X,X) ; :: thesis: verum

end;

hence (g + h) * f = (g * f) + (h * f) ; :: thesis: verum