let E, F, G be RealNormSpace; :: thesis: 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] ) )
let L1 be Lipschitzian LinearOperator of E,G; :: thesis: 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] ) )
let L2 be Lipschitzian LinearOperator of F,G; :: thesis: 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] ) )
consider L being LinearOperator of [:E,F:],G such that
A1: ( ( 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] ) ) by Th1;
consider K1 being Real such that
A2: ( 0 <= K1 & ( for x being VECTOR of E holds ||.(L1 . x).|| <= K1 * ||.x.|| ) ) by LOPBAN_1:def 8;
consider K2 being Real such that
A3: ( 0 <= K2 & ( for y being VECTOR of F holds ||.(L2 . y).|| <= K2 * ||.y.|| ) ) by LOPBAN_1:def 8;

now :: thesis: for z being Point of [:E,F:] holds ||.(L . z).|| <= (K1 + K2) * ||.z.||

let z be Point of [:E,F:]; :: thesis: ||.(L . z).|| <= (K1 + K2) * ||.z.||
consider x being Point of E, y being Point of F such that
A5: z = [x,y] by PRVECT_3:18;
L . z = (L1 . x) + (L2 . y) by A1, A5;
then A7: ||.(L . z).|| <= ||.(L1 . x).|| + ||.(L2 . y).|| by NORMSP_1:def 1;
A8: ( ||.(L1 . x).|| <= K1 * ||.x.|| & ||.(L2 . y).|| <= K2 * ||.y.|| ) by A2, A3;
A9: K1 * ||.x.|| <= K1 * ||.z.|| by A2, A5, NDIFF_8:21, XREAL_1:64;
K2 * ||.y.|| <= K2 * ||.z.|| by A3, A5, NDIFF_8:21, XREAL_1:64;
then ( ||.(L1 . x).|| <= K1 * ||.z.|| & ||.(L2 . y).|| <= K2 * ||.z.|| ) by A8, A9, XXREAL_0:2;
then ||.(L1 . x).|| + ||.(L2 . y).|| <= (K1 * ||.z.||) + (K2 * ||.z.||) by XREAL_1:7;
hence ||.(L . z).|| <= (K1 + K2) * ||.z.|| by A7, XXREAL_0:2; :: thesis: verum

end;

then L is Lipschitzian by A2, A3, LOPBAN_1:def 8;
hence 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] ) ) by A1; :: thesis: verum