for K being Ring
for V being LeftMod of K
for A1, A2 being Subset of V st A1 <> {} & A1 c= A2 holds
for x being set st x is Vector of A1 holds
x is Vector of A2