let X be RealNormSpace; for f being Element of BoundedLinearOperators (X,X) holds
( f * (FuncUnit X) = f & (FuncUnit X) * f = f )
let f be Element of BoundedLinearOperators (X,X); ( f * (FuncUnit X) = f & (FuncUnit X) * f = f )
id the carrier of X is Lipschitzian LinearOperator of X,X
by Th3;
then
id the carrier of X is Element of BoundedLinearOperators (X,X)
by LOPBAN_1:def 9;
then A1:
modetrans ((id the carrier of X),X,X) = id the carrier of X
by LOPBAN_1:def 11;
hence f * (FuncUnit X) =
modetrans (f,X,X)
by Th6
.=
f
by LOPBAN_1:def 11
;
(FuncUnit X) * f = f
thus (FuncUnit X) * f =
modetrans (f,X,X)
by A1, Th6
.=
f
by LOPBAN_1:def 11
; verum