let L1, L2 be Lipschitzian LinearOperator of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])); :: thesis: ( ( for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds L1 . (f,g) = <:f,g:> ) & ( for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds L2 . (f,g) = <:f,g:> ) implies L1 = L2 )
set SE = R_NormSpace_of_BoundedLinearOperators (S,E);
set SF = R_NormSpace_of_BoundedLinearOperators (S,F);
set SEF = R_NormSpace_of_BoundedLinearOperators (S,[:E,F:]);
assume A47: for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds L1 . (f,g) = <:f,g:> ; :: thesis: ( ex f being Lipschitzian LinearOperator of S,E ex g being Lipschitzian LinearOperator of S,F st not L2 . (f,g) = <:f,g:> or L1 = L2 )
assume A48: for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds L2 . (f,g) = <:f,g:> ; :: thesis: L1 = L2
reconsider LL1 = L1 as Function of [:([#] (R_NormSpace_of_BoundedLinearOperators (S,E))),([#] (R_NormSpace_of_BoundedLinearOperators (S,F))):],([#] (R_NormSpace_of_BoundedLinearOperators (S,[:E,F:]))) ;
reconsider LL2 = L2 as Function of [:([#] (R_NormSpace_of_BoundedLinearOperators (S,E))),([#] (R_NormSpace_of_BoundedLinearOperators (S,F))):],([#] (R_NormSpace_of_BoundedLinearOperators (S,[:E,F:]))) ;
for a being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,E))
for b being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,F)) holds LL1 . (a,b) = LL2 . (a,b)

proof

let a be Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,E)); :: thesis: for b being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,F)) holds LL1 . (a,b) = LL2 . (a,b)
let b be Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,F)); :: thesis: LL1 . (a,b) = LL2 . (a,b)
reconsider a1 = a as Lipschitzian LinearOperator of S,E by LOPBAN_1:def 9;
reconsider b1 = b as Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9;
thus LL1 . (a,b) = <:a1,b1:> by A47
.= LL2 . (a,b) by A48 ; :: thesis: verum

end;

hence L1 = L2 by BINOP_1:2; :: thesis: verum