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 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 ;

:: thesis: (FuncUnit X) * f = f

thus (FuncUnit X) * f = modetrans (f,X,X) by A1, Th6

.= f by LOPBAN_1:def 11 ; :: thesis: verum

( 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 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 ;

:: thesis: (FuncUnit X) * f = f

thus (FuncUnit X) * f = modetrans (f,X,X) by A1, Th6

.= f by LOPBAN_1:def 11 ; :: thesis: verum