let X be ComplexNormSpace; :: thesis: for f being bounded LinearOperator of X,X holds
( f * (id the carrier of X) = f & (id the carrier of X) * f = f )
let f be bounded LinearOperator of X,X; :: thesis: ( f * (id the carrier of X) = f & (id the carrier of X) * f = f )
reconsider ii = id the carrier of X as bounded LinearOperator of X,X by Th3;

A1: now

let x be VECTOR of X; :: thesis: (f * (id the carrier of X)) . x = f . x
thus (f * (id the carrier of X)) . x = (f * ii) . x
.= f . (ii . x) by Th4
.= f . x by FUNCT_1:35 ; :: thesis: verum

end;

now

let x be VECTOR of X; :: thesis: ((id the carrier of X) * f) . x = f . x
thus ((id the carrier of X) * f) . x = (ii * f) . x
.= ii . (f . x) by Th4
.= f . x by FUNCT_1:35 ; :: thesis: verum

end;

hence ( f * (id the carrier of X) = f & (id the carrier of X) * f = f ) by A1, FUNCT_2:113; :: thesis: verum