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