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