:: deftheorem defines are_isomorphic VECTSP13:def 10 :
for R being Ring
for U, V being VectSp of R holds
( U,V are_isomorphic iff ex T being linear-transformation of U,V st T is bijective );