let E, F, G be RealNormSpace; :: thesis:
let L be LinearOperator of [:E,F:],G; :: thesis:
deffunc H₁( 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 = H₁(x) from FUNCT_2:sch 4();
A4: for s, t being Element of E holds L1 . (s + t) = (L1 . s) + (L1 . t)

let s, t be Element of E; :: thesis:
reconsider z = [s,(0. F)], w = [t,(0. F)] as Point of [:E,F:] ;
z + w = [(s + t),((0. F) + (0. F))] by PRVECT_3:18
.= [(s + t),(0. F)] by RLVECT_1:4 ;
hence L1 . (s + t) = L /. (z + w) by A1
.= (L /. z) + (L /. w) by VECTSP_1:def 20
.= (L1 . s) + (L /. [t,(0. F)]) by A1
.= (L1 . s) + (L1 . t) by A1 ;
:: thesis:

end;

for s being Element of E
for r being Real holds L1 . (r * s) = r * (L1 . s)

let s be Element of E; :: thesis:
let r be Real; :: thesis:
reconsider z = [s,(0. F)] as Point of [:E,F:] ;
r * z = [(r * s),(r * (0. F))] by PRVECT_3:18
.= [(r * s),(0. F)] by RLVECT_1:10 ;
hence L1 . (r * s) = L /. (r * z) by A1
.= r * (L /. z) by LOPBAN_1:def 5
.= r * (L1 . s) by A1 ;
:: thesis:

end;

then reconsider L1 = L1 as LinearOperator of E,G by A4, LOPBAN_1:def 5, VECTSP_1:def 20;
deffunc H₂( 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 = H₂(x) from FUNCT_2:sch 4();
A10: for s, t being Element of F holds L2 . (s + t) = (L2 . s) + (L2 . t)

let s, t be Element of F; :: thesis:
reconsider z = [(0. E),s], w = [(0. E),t] as Point of [:E,F:] ;
z + w = [((0. E) + (0. E)),(s + t)] by PRVECT_3:18
.= [(0. E),(s + t)] by RLVECT_1:4 ;
hence L2 . (s + t) = L /. (z + w) by A7
.= (L /. z) + (L /. w) by VECTSP_1:def 20
.= (L2 . s) + (L /. [(0. E),t]) by A7
.= (L2 . s) + (L2 . t) by A7 ;
:: thesis:

end;

for s being Element of F
for r being Real holds L2 . (r * s) = r * (L2 . s)

let s be Element of F; :: thesis:
let r be Real; :: thesis:
reconsider z = [(0. E),s] as Point of [:E,F:] ;
r * z = [(r * (0. E)),(r * s)] by PRVECT_3:18
.= [(0. E),(r * s)] by RLVECT_1:10 ;
hence L2 . (r * s) = L /. (r * z) by A7
.= r * (L /. z) by LOPBAN_1:def 5
.= r * (L2 . s) by A7 ;
:: thesis:

end;

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)

let x be Point of E; :: thesis:
let y be Point of F; :: thesis:
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 ;
:: thesis:

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; :: thesis: