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

now :: thesis: for x being Point of E holds ||.(L1 . x).|| <= K * ||.x.||

let x be Point of E; :: thesis: ||.(L1 . x).|| <= K * ||.x.||
[x,(0. F)] is set by TARSKI:1;
then reconsider z = [x,(0. F)] as Point of [:E,F:] by PRVECT_3:18;
z in the carrier of [:E,F:] ;
then A3: z in dom L by FUNCT_2:def 1;
A4: L1 . x = L /. [x,(0. F)] by A1
.= L . z by A3, PARTFUN1:def 6 ;
||.z.|| = ||.x.|| by NDIFF_8:2;
hence ||.(L1 . x).|| <= K * ||.x.|| by A2, A4; :: thesis: verum

end;

then A5: L1 is Lipschitzian by A2, LOPBAN_1:def 8;

now :: thesis: for y being Point of F holds ||.(L2 . y).|| <= K * ||.y.||

let y be Point of F; :: thesis: ||.(L2 . y).|| <= K * ||.y.||
[(0. E),y] is set by TARSKI:1;
then reconsider z = [(0. E),y] as Point of [:E,F:] by PRVECT_3:18;
z in the carrier of [:E,F:] ;
then A6: z in dom L by FUNCT_2:def 1;
A7: L2 . y = L /. [(0. E),y] by A1
.= L . z by A6, PARTFUN1:def 6 ;
||.z.|| = ||.y.|| by NDIFF_8:3;
hence ||.(L2 . y).|| <= K * ||.y.|| by A2, A7; :: thesis: verum

end;

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