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

proof

let x be Point of X; :: thesis: (w * (u - v)) . x = ((w * u) . x) - ((w * v) . x)
A6: modetrans (w,Y,Z) is additive ;
thus (w * (u - v)) . x = (modetrans (w,Y,Z)) . ((modetrans ((u - v),X,Y)) . x) by FUNCT_2:15
.= (modetrans (w,Y,Z)) . ((u - v) . x) by LOPBAN_1:def 11
.= (modetrans (w,Y,Z)) . ((u . x) - (v . x)) by LOPBAN_1:40
.= ((modetrans (w,Y,Z)) . (u . x)) + ((modetrans (w,Y,Z)) . (- (v . x))) by A6
.= ((modetrans (w,Y,Z)) . (u . x)) + ((modetrans (w,Y,Z)) . ((- 1) * (v . x))) by RLVECT_1:16
.= ((modetrans (w,Y,Z)) . (u . x)) + ((- 1) * ((modetrans (w,Y,Z)) . (v . x))) by LOPBAN_1:def 5
.= ((modetrans (w,Y,Z)) . (u . x)) - ((modetrans (w,Y,Z)) . (v . x)) by RLVECT_1:16
.= ((modetrans (w,Y,Z)) . ((modetrans (u,X,Y)) . x)) - ((modetrans (w,Y,Z)) . ((modetrans (v,X,Y)) . x)) by A2, LOPBAN_1:def 11
.= (((modetrans (w,Y,Z)) * (modetrans (u,X,Y))) . x) - ((modetrans (w,Y,Z)) . ((modetrans (v,X,Y)) . x)) by FUNCT_2:15
.= ((w * u) . x) - ((w * v) . x) by FUNCT_2:15 ; :: thesis: verum

end;

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

proof

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

end;

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