theorem Th2: :: NDIFF_9:10

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