for K being Ring
for M, N being LeftMod of K
for x being object st M c= N holds
( ( x in M implies x in N ) & ( x is Vector of M implies x is Vector of N ) ) by VECTSP_4:9, VECTSP_4:10;