let X be ComplexNormSpace; :: 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 = C_NormSpace_of_BoundedLinearOperators X,X;
set ADD = Add_ (BoundedLinearOperators X,X),(C_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),(C_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 (C_NormSpace_of_BoundedLinearOperators X,X) by CLOPBAN1:def 8;
reconsider fg = (modetrans f,X,X) * (modetrans g,X,X) as VECTOR of (C_NormSpace_of_BoundedLinearOperators X,X) by CLOPBAN1:def 8;
reconsider k = (modetrans f,X,X) * (modetrans (g + h),X,X) as VECTOR of (C_NormSpace_of_BoundedLinearOperators X,X) by CLOPBAN1:def 8;
reconsider hh = h as VECTOR of (C_NormSpace_of_BoundedLinearOperators X,X) ;
reconsider gg = g as VECTOR of (C_NormSpace_of_BoundedLinearOperators X,X) ;
A1: ( gg = modetrans g,X,X & hh = modetrans h,X,X ) by CLOPBAN1:def 10;
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 CLOPBAN1:def 10;
then A2: (modetrans (g + h),X,X) . x = ((modetrans g,X,X) . x) + ((modetrans h,X,X) . x) by A1, CLOPBAN1:39;
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, CLOPBAN1:def 3
.= (((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 CLOPBAN1:39;
hence (Add_ (BoundedLinearOperators X,X),(C_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