let X, Y, Z be RealNormSpace; :: thesis: for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for g, h being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds f * (g + h) = (f * g) + (f * h)
let f be Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: for g, h being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds f * (g + h) = (f * g) + (f * h)
let g, h be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: f * (g + h) = (f * g) + (f * h)
set BLOPXY = R_NormSpace_of_BoundedLinearOperators (X,Y);
set BLOPXZ = R_NormSpace_of_BoundedLinearOperators (X,Z);
set mf = modetrans (f,Y,Z);
set mg = modetrans (g,X,Y);
set mh = modetrans (h,X,Y);
set mgh = modetrans ((g + h),X,Y);
A1: (modetrans (f,Y,Z)) * (modetrans (h,X,Y)) is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2;
then reconsider fh = (modetrans (f,Y,Z)) * (modetrans (h,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;
A3: (modetrans (f,Y,Z)) * (modetrans ((g + h),X,Y)) is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2;
then reconsider k = (modetrans (f,Y,Z)) * (modetrans ((g + h),X,Y)) as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,Z)) by LOPBAN_1:def 9;
reconsider hh = h as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
reconsider gg = g as VECTOR of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ;
A4: ( gg = modetrans (g,X,Y) & hh = modetrans (h,X,Y) ) by LOPBAN_1:def 11;
for x being VECTOR of X holds ((modetrans (f,Y,Z)) * (modetrans ((g + h),X,Y))) . x = (((modetrans (f,Y,Z)) * (modetrans (g,X,Y))) . x) + (((modetrans (f,Y,Z)) * (modetrans (h,X,Y))) . x)

proof

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

end;

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