let X, Y be RealNormSpace; :: thesis: for f being Element of BoundedLinearOperators (X,Y) holds
( f * (FuncUnit X) = f & (FuncUnit Y) * f = f )
let f be Element of BoundedLinearOperators (X,Y); :: thesis: ( f * (FuncUnit X) = f & (FuncUnit Y) * f = f )
id the carrier of X is Lipschitzian LinearOperator of X,X by LOPBAN_2:3;
then id the carrier of X is Element of BoundedLinearOperators (X,X) by LOPBAN_1:def 9;
then 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,Y) by LPB2Th6
.= f by LOPBAN_1:def 11 ;
:: thesis: (FuncUnit Y) * f = f
id the carrier of Y is Lipschitzian LinearOperator of Y,Y by LOPBAN_2:3;
then id the carrier of Y is Element of BoundedLinearOperators (Y,Y) by LOPBAN_1:def 9;
then modetrans ((id the carrier of Y),Y,Y) = id the carrier of Y by LOPBAN_1:def 11;
hence (FuncUnit Y) * f = modetrans (f,X,Y) by LPB2Th6
.= f by LOPBAN_1:def 11 ;
:: thesis: verum