consider J being LinearOperator of (product <*X,Y*>),[:X,Y:] such that
P3: J = f " and
( J is one-to-one & J is onto & J is isometric ) by LM020;
thus f " is LinearOperator of (product <*X,Y*>),[:X,Y:] by P3; :: thesis: verum