let X, Y, Z be RealNormSpace; :: thesis: for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds
( (u - v) * w = (u * w) - (v * w) & (u + v) * w = (u * w) + (v * w) )
let w be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds
( (u - v) * w = (u * w) - (v * w) & (u + v) * w = (u * w) + (v * w) )
let u, v be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: ( (u - v) * w = (u * w) - (v * w) & (u + v) * w = (u * w) + (v * w) )
A1: modetrans (w,X,Y) = w by LOPBAN_1:def 11;
A2: modetrans (u,Y,Z) = u by LOPBAN_1:def 11;
for x being Point of X holds ((u - v) * w) . x = ((u * w) . x) - ((v * w) . x)

proof

let x be Point of X; :: thesis: ((u - v) * w) . x = ((u * w) . x) - ((v * w) . x)
thus ((u - v) * w) . x = (modetrans ((u - v),Y,Z)) . ((modetrans (w,X,Y)) . x) by FUNCT_2:15
.= (modetrans ((u - v),Y,Z)) . (w . x) by LOPBAN_1:def 11
.= (u - v) . (w . x) by LOPBAN_1:def 11
.= (u . (w . x)) - (v . (w . x)) by LOPBAN_1:40
.= ((modetrans (u,Y,Z)) . ((modetrans (w,X,Y)) . x)) - ((modetrans (v,Y,Z)) . ((modetrans (w,X,Y)) . x)) by A1, A2, LOPBAN_1:def 11
.= (((modetrans (u,Y,Z)) * (modetrans (w,X,Y))) . x) - ((modetrans (v,Y,Z)) . ((modetrans (w,X,Y)) . x)) by FUNCT_2:15
.= ((u * w) . x) - ((v * w) . x) by FUNCT_2:15 ; :: thesis: verum

end;

hence (u - v) * w = (u * w) - (v * w) by LOPBAN_1:40; :: thesis: (u + v) * w = (u * w) + (v * w)
for x being Point of X holds ((u + v) * w) . x = ((u * w) . x) + ((v * w) . x)

proof

let x be Point of X; :: thesis: ((u + v) * w) . x = ((u * w) . x) + ((v * w) . x)
thus ((u + v) * w) . x = (modetrans ((u + v),Y,Z)) . ((modetrans (w,X,Y)) . x) by FUNCT_2:15
.= (modetrans ((u + v),Y,Z)) . (w . x) by LOPBAN_1:def 11
.= (u + v) . (w . x) by LOPBAN_1:def 11
.= (u . (w . x)) + (v . (w . x)) by LOPBAN_1:35
.= ((modetrans (u,Y,Z)) . ((modetrans (w,X,Y)) . x)) + ((modetrans (v,Y,Z)) . ((modetrans (w,X,Y)) . x)) by A1, A2, LOPBAN_1:def 11
.= (((modetrans (u,Y,Z)) * (modetrans (w,X,Y))) . x) + ((modetrans (v,Y,Z)) . ((modetrans (w,X,Y)) . x)) by FUNCT_2:15
.= ((u * w) . x) + ((v * w) . x) by FUNCT_2:15 ; :: thesis: verum

end;

hence (u + v) * w = (u * w) + (v * w) by LOPBAN_1:35; :: thesis: verum