let X, Y, Z be RealNormSpace; :: thesis: for v being Lipschitzian LinearOperator of X,Y
for s being Lipschitzian LinearOperator of Y,Z
for pv being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for ps being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) st v = pv & s = ps holds
s * v = ps * pv
let v be Lipschitzian LinearOperator of X,Y; :: thesis: for s being Lipschitzian LinearOperator of Y,Z
for pv being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for ps being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) st v = pv & s = ps holds
s * v = ps * pv
let s be Lipschitzian LinearOperator of Y,Z; :: thesis: for pv being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for ps being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) st v = pv & s = ps holds
s * v = ps * pv
let pv be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for ps being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) st v = pv & s = ps holds
s * v = ps * pv
let ps be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: ( v = pv & s = ps implies s * v = ps * pv )
assume A1: ( v = pv & s = ps ) ; :: thesis: s * v = ps * pv
then modetrans (pv,X,Y) = v by LOPBAN_1:29;
hence s * v = ps * pv by A1, LOPBAN_1:29; :: thesis: verum