addLoopStr(# the carrier of (n -VectSp_over F),the addF of (n -VectSp_over F),the U2 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