reconsider o = ~ the lmult of V as Function of [:the carrier of V,the carrier of (opp K):],the carrier of V ;
opp V = RightModStr(# the carrier of V,the addF of V,(0. V),o #) by Def2;
hence not the carrier of (opp V) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum