theorem Th8: :: CLOPBAN2:8

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