reconsider o = ~ the lmult of V as Function of [:the carrier of V,the carrier of (opp K):],the carrier of V ;
take RightModStr(# the carrier of V,the addF of V,(0. V),o #) ; :: thesis: for o being Function of [:the carrier of V,the carrier of (opp K):],the carrier of V st o = ~ the lmult of V holds
RightModStr(# the carrier of V,the addF of V,(0. V),o #) = RightModStr(# the carrier of V,the addF of V,(0. V),o #)
thus for o being Function of [:the carrier of V,the carrier of (opp K):],the carrier of V st o = ~ the lmult of V holds
RightModStr(# the carrier of V,the addF of V,(0. V),o #) = RightModStr(# the carrier of V,the addF of V,(0. V),o #) ; :: thesis: verum