for E, F, G being RealNormSpace
for L being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) ex L1 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) ex L2 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st
( ( for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) ) & ( for x being Point of E holds L1 . x = L . [x,(0. F)] ) & ( for y being Point of F holds L2 . y = L . [(0. E),y] ) & ||.L.|| <= ||.L1.|| + ||.L2.|| & ||.L1.|| <= ||.L.|| & ||.L2.|| <= ||.L.|| )