reconsider o = ~ the rmult of W as Function of [:the carrier of (opp K),the carrier of W:],the carrier of W ;
opp W = VectSpStr(# 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