let E, F, G be RealNormSpace; :: thesis: for L1 being LinearOperator of E,G
for L2 being LinearOperator of F,G ex L being 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 LinearOperator of E,G; :: thesis: for L2 being LinearOperator of F,G ex L being 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 LinearOperator of F,G; :: thesis: ex L being 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] ) )
defpred S₁[ object , object ] means ex x being Point of E ex y being Point of F st
( $1 = [x,y] & $2 = (L1 . x) + (L2 . y) );
A1: for z being Element of [:E,F:] ex y being Element of G st S₁[z,y]

proof

let z be Element of [:E,F:]; :: thesis: ex y being Element of G st S₁[z,y]
consider x being Point of E, y being Point of F such that
A2: z = [x,y] by PRVECT_3:18;
take w = (L1 . x) + (L2 . y); :: thesis: S₁[z,w]
thus S₁[z,w] by A2; :: thesis: verum

end;

consider L being Function of [:E,F:],G such that
A3: for z being Element of [:E,F:] holds S₁[z,L . z] from FUNCT_2:sch 3(A1);
A4: for z, w being Point of [:E,F:] holds L . (z + w) = (L . z) + (L . w)

proof

let z, w be Point of [:E,F:]; :: thesis: L . (z + w) = (L . z) + (L . w)
consider x1 being Point of E, y1 being Point of F such that
A5: ( z = [x1,y1] & L . z = (L1 . x1) + (L2 . y1) ) by A3;
consider x2 being Point of E, y2 being Point of F such that
A6: ( w = [x2,y2] & L . w = (L1 . x2) + (L2 . y2) ) by A3;
A7: z + w = [(x1 + x2),(y1 + y2)] by A5, A6, PRVECT_3:18;
consider x3 being Point of E, y3 being Point of F such that
A8: ( z + w = [x3,y3] & L . (z + w) = (L1 . x3) + (L2 . y3) ) by A3;
A9: ( x3 = x1 + x2 & y3 = y1 + y2 ) by A7, A8, XTUPLE_0:1;
(L . z) + (L . w) = (((L1 . x1) + (L2 . y1)) + (L1 . x2)) + (L2 . y2) by A5, A6, RLVECT_1:def 3
.= (((L1 . x1) + (L1 . x2)) + (L2 . y1)) + (L2 . y2) by RLVECT_1:def 3
.= ((L1 . x1) + (L1 . x2)) + ((L2 . y1) + (L2 . y2)) by RLVECT_1:def 3
.= (L1 . (x1 + x2)) + ((L2 . y1) + (L2 . y2)) by VECTSP_1:def 20
.= L . (z + w) by A8, A9, VECTSP_1:def 20 ;
hence L . (z + w) = (L . z) + (L . w) ; :: thesis: verum

end;

for z being Element of [:E,F:]
for r being Real holds L . (r * z) = r * (L . z)

proof

let z be Element of [:E,F:]; :: thesis: for r being Real holds L . (r * z) = r * (L . z)
let r be Real; :: thesis: L . (r * z) = r * (L . z)
consider x1 being Point of E, y1 being Point of F such that
A10: ( z = [x1,y1] & L . z = (L1 . x1) + (L2 . y1) ) by A3;
A11: r * z = [(r * x1),(r * y1)] by A10, PRVECT_3:18;
consider x2 being Point of E, y2 being Point of F such that
A12: ( r * z = [x2,y2] & L . (r * z) = (L1 . x2) + (L2 . y2) ) by A3;
( x2 = r * x1 & y2 = r * y1 ) by A11, A12, XTUPLE_0:1;
hence L . (r * z) = (r * (L1 . x1)) + (L2 . (r * y1)) by A12, LOPBAN_1:def 5
.= (r * (L1 . x1)) + (r * (L2 . y1)) by LOPBAN_1:def 5
.= r * (L . z) by A10, RLVECT_1:def 5 ;
:: thesis: verum

end;

then reconsider L = L as LinearOperator of [:E,F:],G by A4, LOPBAN_1:def 5, VECTSP_1:def 20;
take L ; :: thesis: ( ( 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] ) )
thus A14: for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) :: thesis: ( ( 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] ) )

proof

let x be Point of E; :: thesis: for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y)
let y be Point of F; :: thesis: L . [x,y] = (L1 . x) + (L2 . y)
reconsider z = [x,y] as Point of [:E,F:] ;
consider x1 being Point of E, y1 being Point of F such that
A15: ( z = [x1,y1] & L . z = (L1 . x1) + (L2 . y1) ) by A3;
( x = x1 & y1 = y ) by A15, XTUPLE_0:1;
hence L . [x,y] = (L1 . x) + (L2 . y) by A15; :: thesis: verum

end;

thus for x being Point of E holds L1 . x = L /. [x,(0. F)] :: thesis: for y being Point of F holds L2 . y = L /. [(0. E),y]

proof

let x be Point of E; :: thesis: L1 . x = L /. [x,(0. F)]
thus L1 . x = (L1 . x) + (0. G) by RLVECT_1:4
.= (L1 . x) + (L2 . (0. F)) by LOPBAN_7:3
.= L /. [x,(0. F)] by A14 ; :: thesis: verum

end;

thus for y being Point of F holds L2 . y = L /. [(0. E),y] :: thesis: verum

proof

let y be Point of F; :: thesis: L2 . y = L /. [(0. E),y]
thus L2 . y = (0. G) + (L2 . y) by RLVECT_1:4
.= (L1 . (0. E)) + (L2 . y) by LOPBAN_7:3
.= L /. [(0. E),y] by A14 ; :: thesis: verum

end;