theorem :: NDIFF_8:8

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