theorem Th74A: :: DUALSP02:29

for X being RealNormSpace st not X is trivial holds
ex L being Lipschitzian LinearOperator of X,(Im (BidualFunc X)) st L is isomorphism