let E, F, G be 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] ) )
let L1 be 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 L2 be 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] ) )
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 for z being Point of [:E,F:] holds ||.(L . z).|| <= (K1 + K2) * ||.z.||let z be
Point of
[:E,F:];
||.(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;
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; verum