let E, F, G be RealNormSpace; :: thesis: for L being Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G))
for L11, L12 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G))
for L21, L22 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L21 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L12 . x) + (L22 . y) ) holds
( L11 = L12 & L21 = L22 )
let L be Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)); :: thesis: for L11, L12 being Point of (R_NormSpace_of_BoundedLinearOperators (E,G))
for L21, L22 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L21 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L12 . x) + (L22 . y) ) holds
( L11 = L12 & L21 = L22 )
let L11, L12 be Point of (R_NormSpace_of_BoundedLinearOperators (E,G)); :: thesis: for L21, L22 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) st ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L21 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L12 . x) + (L22 . y) ) holds
( L11 = L12 & L21 = L22 )
let L21, L22 be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis: ( ( for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L21 . y) ) & ( for x being Point of E
for y being Point of F holds L . [x,y] = (L12 . x) + (L22 . y) ) implies ( L11 = L12 & L21 = L22 ) )
assume A1: for x being Point of E
for y being Point of F holds L . [x,y] = (L11 . x) + (L21 . y) ; :: thesis: ( ex x being Point of E ex y being Point of F st not L . [x,y] = (L12 . x) + (L22 . y) or ( L11 = L12 & L21 = L22 ) )
assume A2: for x being Point of E
for y being Point of F holds L . [x,y] = (L12 . x) + (L22 . y) ; :: thesis: ( L11 = L12 & L21 = L22 )
reconsider LP = L as Lipschitzian LinearOperator of [:E,F:],G by LOPBAN_1:def 9;
reconsider LP11 = L11, LP12 = L12 as Lipschitzian LinearOperator of E,G by LOPBAN_1:def 9;
reconsider LP21 = L21, LP22 = L22 as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
A3: for x being Point of E
for y being Point of F holds LP . [x,y] = (LP11 . x) + (LP21 . y) by A1;
for x being Point of E
for y being Point of F holds LP . [x,y] = (LP12 . x) + (LP22 . y) by A2;
hence ( L11 = L12 & L21 = L22 ) by A3, Th0X; :: thesis: verum