theorem :: NDIFF_9:11

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