consider J being LinearOperator of (product <*X*>),X such that
A1: J = f " and
J is bijective by LOPBAN12:4;
thus f " is LinearOperator of (product <*X*>),X by A1; :: thesis: verum