theorem Th0: :: NDIFF_9:7

for E, F, G being RealNormSpace
for L being LinearOperator of [:E,F:],G ex L1 being LinearOperator of E,G ex L2 being LinearOperator of 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] ) )