let X, Y, Z be RealNormSpace; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) st w = v * u holds
||.w.|| <= ||.v.|| * ||.u.||
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) st w = v * u holds
||.w.|| <= ||.v.|| * ||.u.||
let v be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) st w = v * u holds
||.w.|| <= ||.v.|| * ||.u.||
let w be Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)); :: thesis: ( w = v * u implies ||.w.|| <= ||.v.|| * ||.u.|| )
assume A2: w = v * u ; :: thesis: ||.w.|| <= ||.v.|| * ||.u.||
( modetrans (v,Y,Z) = v & modetrans (u,X,Y) = u ) by LOPBAN_1:def 11;
hence ||.w.|| <= ||.v.|| * ||.u.|| by A2, LOPBAN_2:2; :: thesis: verum