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