let X be RealNormSpace; :: thesis: 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; :: thesis: ( f * (FuncUnit X) = f & (FuncUnit X) * f = f )
id the carrier of X is bounded LinearOperator of X,X by Th3;
then id the carrier of X is Element of BoundedLinearOperators X,X by LOPBAN_1:def 10;
then A1: modetrans (id the carrier of X),X,X = id the carrier of X by LOPBAN_1:def 12;
hence f * (FuncUnit X) = modetrans f,X,X by Th6
.= f by LOPBAN_1:def 12 ;
:: thesis: (FuncUnit X) * f = f
thus (FuncUnit X) * f = modetrans f,X,X by A1, Th6
.= f by LOPBAN_1:def 12 ; :: thesis: verum