for V, W being RealLinearSpace
for A being Subset of V
for T being LinearOperator of V,W st T is bijective holds
( A is Basis of V iff T .: A is Basis of W )