theorem Th8: :: LOPBAN_2:8

for X being RealNormSpace
for f being Element of BoundedLinearOperators (X,X) holds
( f * (FuncUnit X) = f & (FuncUnit X) * f = f )