0. S in the carrier of S ;
hence not VecSp (S,R) is empty by Def5; :: thesis: verum