theorem NISOM08: :: DUALSP02:25

for X, Y being RealNormSpace
for L being Lipschitzian LinearOperator of X,Y
for y being Lipschitzian linear-Functional of Y holds y * L is Lipschitzian linear-Functional of X