theorem Th64: :: NDIFF13:63

for F being non trivial RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators (F,F) is non trivial RealBanachSpace