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.||
reconsider z = [x,(0. F)] as Point of [:E,F:] ;
A4: L1 . x = L /. [x,(0. F)] by A1
.= L . z ;
||.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.||
reconsider z = [(0. E),y] as Point of [:E,F:] ;
A7: L2 . y = L /. [(0. E),y] by A1
.= L . z ;
||.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