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