let F be non trivial RealBanachSpace; :: thesis: R_NormSpace_of_BoundedLinearOperators (F,F) is non trivial RealBanachSpace
set F1 = R_NormSpace_of_BoundedLinearOperators (F,F);
ex x being object st
( x in [#] F & not x = 0. F )

proof

assume A1: for x being object st x in [#] F holds
x = 0. F ; :: thesis: contradiction
for x, y being object st x in [#] F & y in [#] F holds
x = y

proof

let x, y be object ; :: thesis: ( x in [#] F & y in [#] F implies x = y )
assume ( x in [#] F & y in [#] F ) ; :: thesis: x = y
then ( x = 0. F & y = 0. F ) by A1;
hence x = y ; :: thesis: verum

end;

hence contradiction by ZFMISC_1:def 10; :: thesis: verum

end;

then consider y being object such that
A2: ( y in [#] F & y <> 0. F ) ;
reconsider L1 = id ([#] F) as Lipschitzian LinearOperator of F,F by LOPBAN_2:3;
reconsider L2 = L1 as Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) by LOPBAN_1:def 9;
reconsider Z0 = 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) as Lipschitzian LinearOperator of F,F by LOPBAN_1:def 9;
0. (R_NormSpace_of_BoundedLinearOperators (F,F)) = ([#] F) --> (0. F) by LOPBAN_1:31;
then (0. (R_NormSpace_of_BoundedLinearOperators (F,F))) . y = 0. F by A2, FUNCOP_1:7;
then L2 <> 0. (R_NormSpace_of_BoundedLinearOperators (F,F)) by A2, FUNCT_1:17;
hence R_NormSpace_of_BoundedLinearOperators (F,F) is non trivial RealBanachSpace by ZFMISC_1:def 10; :: thesis: verum