consider J being LinearOperator of (product <*X*>),X such that
A1: J = I " and
A2: ( J is one-to-one & J is onto ) and
A3: J is isometric by NDIFF_7:9;
thus for b₁ being LinearOperator of (product <*X*>),X st b₁ = I " holds
( b₁ is one-to-one & b₁ is onto & b₁ is isometric ) by A1, A2, A3; :: thesis: verum