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