theorem :: FIELD_4:30

for R being Ring
for S being RingExtension of R holds VecSp (S,R) is VectSp of R ;