let E, F, G be RealNormSpace; for L being LinearOperator of [:E,F:],G ex L1 being LinearOperator of E,G ex L2 being 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 LinearOperator of [:E,F:],G; ex L1 being LinearOperator of E,G ex L2 being 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] ) )
deffunc H1( Point of E) -> Element of the carrier of G = L /. [$1,(0. F)];
consider L1 being Function of the carrier of E, the carrier of G such that
A1:
for x being Point of E holds L1 . x = H1(x)
from FUNCT_2:sch 4();
A4:
for s, t being Element of E holds L1 . (s + t) = (L1 . s) + (L1 . t)
for s being Element of E
for r being Real holds L1 . (r * s) = r * (L1 . s)
then reconsider L1 = L1 as LinearOperator of E,G by A4, LOPBAN_1:def 5, VECTSP_1:def 20;
deffunc H2( Point of F) -> Element of the carrier of G = L /. [(0. E),$1];
consider L2 being Function of the carrier of F, the carrier of G such that
A7:
for x being Point of F holds L2 . x = H2(x)
from FUNCT_2:sch 4();
A10:
for s, t being Element of F holds L2 . (s + t) = (L2 . s) + (L2 . t)
for s being Element of F
for r being Real holds L2 . (r * s) = r * (L2 . s)
then reconsider L2 = L2 as LinearOperator of F,G by A10, LOPBAN_1:def 5, VECTSP_1:def 20;
for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y)
proof
let x be
Point of
E;
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y)let y be
Point of
F;
L . [x,y] = (L1 . x) + (L2 . y)
reconsider z =
[x,y],
z1 =
[x,(0. F)],
z2 =
[(0. E),y] as
Point of
[:E,F:] ;
z1 + z2 =
[(x + (0. E)),((0. F) + y)]
by PRVECT_3:18
.=
[x,((0. F) + y)]
by RLVECT_1:4
.=
z
by RLVECT_1:4
;
hence L . [x,y] =
(L /. z1) + (L /. z2)
by VECTSP_1:def 20
.=
(L1 . x) + (L /. z2)
by A1
.=
(L1 . x) + (L2 . y)
by A7
;
verum
end;
hence
ex L1 being LinearOperator of E,G ex L2 being 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, A7; verum