theorem Th1: :: NDIFF_9:9

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