let V, W be RealLinearSpace; :: thesis: 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 )
let A be Subset of V; :: thesis: for T being LinearOperator of V,W st T is bijective holds
( A is Basis of V iff T .: A is Basis of W )
let T be LinearOperator of V,W; :: thesis: ( T is bijective implies ( A is Basis of V iff T .: A is Basis of W ) )
assume A1: T is bijective ; :: thesis: ( A is Basis of V iff T .: A is Basis of W )
reconsider S = T as linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) by Th84;
reconsider B = A as Subset of (RLSp2RVSp V) ;
( B is Basis of (RLSp2RVSp V) iff S .: B is Basis of (RLSp2RVSp W) ) by VECTSP12:2, A1;
hence ( A is Basis of V iff T .: A is Basis of W ) by Th80; :: thesis: verum