addLoopStr(# the carrier of (n -VectSp_over F), the addF of (n -VectSp_over F), the ZeroF of (n -VectSp_over F) #) = n -Group_over F by Def5;
hence not the carrier of (n -VectSp_over F) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum