ex J being LinearOperator of (product <*X,Y*>),[:X,Y:] st
( J = f " & J is bijective ) by LM020;
hence f " is LinearOperator of (product <*X,Y*>),[:X,Y:] ; :: thesis: verum