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