let X be RealNormSpace; :: thesis: for f, g, h being Element of BoundedLinearOperators (X,X) holds f * (g + h) = (f * g) + (f * h)
let f, g, h be Element of BoundedLinearOperators (X,X); :: thesis: f * (g + h) = (f * g) + (f * h)
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 (f,X,X)) * (modetrans (g,X,X))),((modetrans (f,X,X)) * (modetrans (h,X,X)))) = (modetrans (f,X,X)) * (modetrans ((g + h),X,X))

proof

reconsider fh = (modetrans (f,X,X)) * (modetrans (h,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def 9;
reconsider fg = (modetrans (f,X,X)) * (modetrans (g,X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def 9;
reconsider k = (modetrans (f,X,X)) * (modetrans ((g + h),X,X)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,X)) by LOPBAN_1:def 9;
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 11;
for x being VECTOR of X holds ((modetrans (f,X,X)) * (modetrans ((g + h),X,X))) . x = (((modetrans (f,X,X)) * (modetrans (g,X,X))) . x) + (((modetrans (f,X,X)) * (modetrans (h,X,X))) . x)

proof

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

end;

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

end;

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