Lin (Base (R,n)) = ModuleStr(# the carrier of (R ^* n), the addF of (R ^* n), the ZeroF of (R ^* n), the lmult of (R ^* n) #) by lemspan;
hence Base (R,n) is base by VECTSP_7:def 3; :: thesis: verum