ex J being LinearOperator of (product <*X,Y*>),[:X,Y:] st
( J = f " & J is bijective ) by LM020;
hence for b₁ being LinearOperator of (product <*X,Y*>),[:X,Y:] st b₁ = f " holds
b₁ is bijective ; :: thesis: verum