theorem Th0X:
for
E,
F,
G being
RealNormSpace for
L being
LinearOperator of
[:E,F:],
G for
L11 being
LinearOperator of
E,
G for
L12 being
LinearOperator of
F,
G for
L21 being
LinearOperator of
E,
G for
L22 being
LinearOperator of
F,
G st ( for
x being
Point of
E for
y being
Point of
F holds
L . [x,y] = (L11 . x) + (L12 . y) ) & ( for
x being
Point of
E for
y being
Point of
F holds
L . [x,y] = (L21 . x) + (L22 . y) ) holds
(
L11 = L21 &
L12 = L22 )