let E, F, G be RealNormSpace; :: thesis: for L being LinearOperator of [:E,F:],G
for L11 being LinearOperator of E,G
for L12 being LinearOperator of F,G
for L21 being LinearOperator of E,G
for L22 being LinearOperator of F,G st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ) holds
( L11 = L21 & L12 = L22 )
let L be LinearOperator of [:E,F:],G; :: thesis: for L11 being LinearOperator of E,G
for L12 being LinearOperator of F,G
for L21 being LinearOperator of E,G
for L22 being LinearOperator of F,G st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ) holds
( L11 = L21 & L12 = L22 )
let L11 be LinearOperator of E,G; :: thesis: for L12 being LinearOperator of F,G
for L21 being LinearOperator of E,G
for L22 being LinearOperator of F,G st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ) holds
( L11 = L21 & L12 = L22 )
let L12 be LinearOperator of F,G; :: thesis: for L21 being LinearOperator of E,G
for L22 being LinearOperator of F,G st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ) holds
( L11 = L21 & L12 = L22 )
let L21 be LinearOperator of E,G; :: thesis: for L22 being LinearOperator of F,G st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ) holds
( L11 = L21 & L12 = L22 )
let L22 be LinearOperator of F,G; :: thesis: ( ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ) implies ( L11 = L21 & L12 = L22 ) )
assume that
A1: for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L12 . y) and
A2: for x being Point of E
for y being Point of F holds L . [x,y] = (L21 . x) + (L22 . y) ; :: thesis: ( L11 = L21 & L12 = L22 )
now :: thesis: for x being Point of E holds L11 . x = L21 . x
let x be Point of E; :: thesis: L11 . x = L21 . x
A4: L22 . (0. F) = 0. G by LOPBAN_7:3;
L12 . (0. F) = 0. G by LOPBAN_7:3;
hence L11 . x = (L11 . x) + (L12 . (0. F)) by RLVECT_1:4
.= L . [x,(0. F)] by A1
.= (L21 . x) + (L22 . (0. F)) by A2
.= L21 . x by A4, RLVECT_1:4 ;
:: thesis: verum
end;
hence L11 = L21 by FUNCT_2:def 8; :: thesis: L12 = L22
now :: thesis: for y being Point of F holds L12 . y = L22 . y
let y be Point of F; :: thesis: L12 . y = L22 . y
A6: L21 . (0. E) = 0. G by LOPBAN_7:3;
L11 . (0. E) = 0. G by LOPBAN_7:3;
hence L12 . y = (L11 . (0. E)) + (L12 . y) by RLVECT_1:4
.= L . [(0. E),y] by A1
.= (L21 . (0. E)) + (L22 . y) by A2
.= L22 . y by A6, RLVECT_1:4 ;
:: thesis: verum
end;
hence L12 = L22 by FUNCT_2:def 8; :: thesis: verum