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 #)
; 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 #)
; verum