theorem
for
E,
F,
G being
RealNormSpace for
L being
Point of
(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) for
L11,
L12 being
Point of
(R_NormSpace_of_BoundedLinearOperators (E,G)) for
L21,
L22 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] = (L11 . x) + (L21 . y) ) & ( for
x being
Point of
E for
y being
Point of
F holds
L . [x,y] = (L12 . x) + (L22 . y) ) holds
(
L11 = L12 &
L21 = L22 )