reconsider o = ~ the lmult of V as Function of [: the carrier of V, the carrier of (opp K):], the carrier of V ;

let M1, M2 be strict RightModStr over opp K; :: 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

M1 = 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

M2 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) ) implies M1 = M2 )

assume that

A1: 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

M1 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) and

A2: 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

M2 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) ; :: thesis: M1 = M2

thus M1 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) by A1

.= M2 by A2 ; :: thesis: verum

let M1, M2 be strict RightModStr over opp K; :: 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

M1 = 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

M2 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) ) implies M1 = M2 )

assume that

A1: 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

M1 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) and

A2: 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

M2 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) ; :: thesis: M1 = M2

thus M1 = RightModStr(# the carrier of V, the addF of V,(0. V),o #) by A1

.= M2 by A2 ; :: thesis: verum