:: RMOD_3 semantic presentation

K144() is Element of bool K140()

K140() is set

bool K140() is non empty set

K117() is set

bool K117() is non empty set

bool K144() is non empty set

{} is set

the Relation-like non-empty empty-yielding empty set is Relation-like non-empty empty-yielding empty set

1 is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

the carrier of V is non empty set

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

{ (b

bool the carrier of V is non empty set

the carrier of S is non empty set

the carrier of A is non empty set

W3 is set

W2 is Element of the carrier of V

AB is Element of the carrier of V

W2 + AB is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

(0. V) + (0. V) is Element of the carrier of V

W3 is Element of bool the carrier of V

B is Element of bool the carrier of V

C is Element of bool the carrier of V

{ (b

W2 is set

AB is Element of the carrier of V

BC is Element of the carrier of V

AB + BC is Element of the carrier of V

W2 is set

AB is Element of the carrier of V

BC is Element of the carrier of V

AB + BC is Element of the carrier of V

B is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of B is non empty set

C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of C is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of S is non empty set

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of A is non empty set

the carrier of S /\ the carrier of A is set

the carrier of V is non empty set

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

the carrier of V /\ the carrier of V is set

bool the carrier of V is non empty set

W3 is Element of bool the carrier of V

W2 is Element of bool the carrier of V

AB is Element of bool the carrier of V

B is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of B is non empty set

C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of C is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

the carrier of V is non empty set

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is set

the carrier of (R,V,S,A) is non empty set

{ (b

C is Element of the carrier of V

W1 is Element of the carrier of V

C + W1 is Element of the carrier of V

C is Element of the carrier of V

W1 is Element of the carrier of V

C + W1 is Element of the carrier of V

{ (b

the carrier of (R,V,S,A) is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

the carrier of V is non empty set

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

B + (0. V) is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

(0. V) + B is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is set

the carrier of (R,V,S,A) is non empty set

the carrier of S is non empty set

the carrier of A is non empty set

the carrier of S /\ the carrier of A is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

{ (b

{ (b

W1 is set

W3 is Element of the carrier of V

W2 is Element of the carrier of V

W3 + W2 is Element of the carrier of V

the carrier of (R,V,S,A) is non empty set

W1 is set

W3 is Element of the carrier of V

W2 is Element of the carrier of V

W3 + W2 is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of S is non empty set

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,S,A) is non empty set

B is set

the carrier of V is non empty set

{ (b

W1 is Element of the carrier of S

W3 is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

W3 + (0. V) is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of S is non empty set

A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of A is non empty set

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,S,A) is non empty set

B is set

the carrier of V is non empty set

{ (b

C is Element of the carrier of V

W1 is Element of the carrier of V

C + W1 is Element of the carrier of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

{ (b

{ (b

{ (b

{ (b

the carrier of (R,V,S,(R,V,A,B)) is non empty set

AB is set

BC is Element of the carrier of V

u is Element of the carrier of V

BC + u is Element of the carrier of V

the carrier of (R,V,S,A) is non empty set

v21 is Element of the carrier of V

v22 is Element of the carrier of V

v21 + v22 is Element of the carrier of V

v22 + u is Element of the carrier of V

the carrier of (R,V,A,B) is non empty set

v21 + (v22 + u) is Element of the carrier of V

AB is set

BC is Element of the carrier of V

u is Element of the carrier of V

BC + u is Element of the carrier of V

the carrier of (R,V,A,B) is non empty set

v21 is Element of the carrier of V

v22 is Element of the carrier of V

v21 + v22 is Element of the carrier of V

BC + v21 is Element of the carrier of V

the carrier of (R,V,S,A) is non empty set

(BC + v21) + v22 is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of S is non empty set

the carrier of (R,V,S,A) is non empty set

the carrier of A is non empty set

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,A,S) is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of S is non empty set

the carrier of A is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

(0). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

S is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,((0). V),S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,((0). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of ((0). V) is non empty set

the carrier of S is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of S is non empty set

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of A is non empty set

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,B,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,B,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

{ (b

{ (b

C is Element of the carrier of V

the carrier of (R,V,B,S) is non empty set

W2 is Element of the carrier of V

AB is Element of the carrier of V

W2 + AB is Element of the carrier of V

the carrier of (R,V,B,A) is non empty set

the carrier of (R,V,B,A) is non empty set

W2 is Element of the carrier of V

AB is Element of the carrier of V

W2 + AB is Element of the carrier of V

the carrier of (R,V,B,S) is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of S is non empty set

the carrier of ((Omega). V) is non empty set

0. S is V47(S) Element of the carrier of S

the ZeroF of S is Element of the carrier of S

0. ((Omega). V) is V47( (Omega). V) Element of the carrier of ((Omega). V)

the ZeroF of ((Omega). V) is Element of the carrier of ((Omega). V)

the U7 of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is Relation-like non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is Relation-like non empty set

bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set

the U7 of ((Omega). V) is Relation-like [: the carrier of ((Omega). V), the carrier of ((Omega). V):] -defined the carrier of ((Omega). V) -valued Function-like V18([: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V)) Element of bool [:[: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V):]

[: the carrier of ((Omega). V), the carrier of ((Omega). V):] is Relation-like non empty set

[:[: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V):] is Relation-like non empty set

bool [:[: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V):] is non empty set

the U7 of ((Omega). V) | [: the carrier of S, the carrier of S:] is Relation-like [: the carrier of S, the carrier of S:] -defined [: the carrier of ((Omega). V), the carrier of ((Omega). V):] -defined the carrier of ((Omega). V) -valued set

the rmult of S is Relation-like [: the carrier of S, the carrier of R:] -defined the carrier of S -valued Function-like V18([: the carrier of S, the carrier of R:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of R:], the carrier of S:]

[: the carrier of S, the carrier of R:] is Relation-like non empty set

[:[: the carrier of S, the carrier of R:], the carrier of S:] is Relation-like non empty set

bool [:[: the carrier of S, the carrier of R:], the carrier of S:] is non empty set

the rmult of ((Omega). V) is Relation-like [: the carrier of ((Omega). V), the carrier of R:] -defined the carrier of ((Omega). V) -valued Function-like V18([: the carrier of ((Omega). V), the carrier of R:], the carrier of ((Omega). V)) Element of bool [:[: the carrier of ((Omega). V), the carrier of R:], the carrier of ((Omega). V):]

[: the carrier of ((Omega). V), the carrier of R:] is Relation-like non empty set

[:[: the carrier of ((Omega). V), the carrier of R:], the carrier of ((Omega). V):] is Relation-like non empty set

bool [:[: the carrier of ((Omega). V), the carrier of R:], the carrier of ((Omega). V):] is non empty set

the rmult of ((Omega). V) | [: the carrier of S, the carrier of R:] is Relation-like [: the carrier of S, the carrier of R:] -defined [: the carrier of ((Omega). V), the carrier of R:] -defined the carrier of ((Omega). V) -valued set

0. V is V47(V) Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

S is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() strict RightMod-like RightModStr over R

(0). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

(R,V,((0). V),((Omega). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() strict RightMod-like RightModStr over S

(Omega). A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of A

the carrier of A is non empty set

the U7 of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like V18([: the carrier of A, the carrier of A:], the carrier of A) Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]

[: the carrier of A, the carrier of A:] is Relation-like non empty set

[:[: the carrier of A, the carrier of A:], the carrier of A:] is Relation-like non empty set

bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set

the ZeroF of A is Element of the carrier of A

the rmult of A is Relation-like [: the carrier of A, the carrier of S:] -defined the carrier of A -valued Function-like V18([: the carrier of A, the carrier of S:], the carrier of A) Element of bool [:[: the carrier of A, the carrier of S:], the carrier of A:]

the carrier of S is non empty set

[: the carrier of A, the carrier of S:] is Relation-like non empty set

[:[: the carrier of A, the carrier of S:], the carrier of A:] is Relation-like non empty set

bool [:[: the carrier of A, the carrier of S:], the carrier of A:] is non empty set

RightModStr(# the carrier of A, the U7 of A, the ZeroF of A, the rmult of A #) is non empty strict RightModStr over S

(0). A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of A

(S,A,((Omega). A),((0). A)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of A

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,((Omega). V),S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,((Omega). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of ((Omega). V) is non empty set

A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of A is non empty set

the carrier of S is non empty set

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() strict RightMod-like RightModStr over R

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

(R,V,((Omega). V),((Omega). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of S is non empty set

the carrier of S /\ the carrier of S is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,S,A) is non empty set

the carrier of A is non empty set

the carrier of S is non empty set

the carrier of A /\ the carrier of S is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of S is non empty set

the carrier of A is non empty set

the carrier of B is non empty set

the carrier of (R,V,S,(R,V,A,B)) is non empty set

the carrier of (R,V,A,B) is non empty set

the carrier of S /\ the carrier of (R,V,A,B) is set

the carrier of A /\ the carrier of B is set

the carrier of S /\ ( the carrier of A /\ the carrier of B) is set

the carrier of S /\ the carrier of A is set

( the carrier of S /\ the carrier of A) /\ the carrier of B is set

the carrier of (R,V,S,A) is non empty set

the carrier of (R,V,S,A) /\ the carrier of B is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of S is non empty set

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,S,A) is non empty set

the carrier of A is non empty set

the carrier of S /\ the carrier of A is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,S,A) is non empty set

the carrier of S is non empty set

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,A,S) is non empty set

the carrier of A is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of A is non empty set

the carrier of S is non empty set

the carrier of (R,V,A,S) is non empty set

the carrier of A /\ the carrier of S is set

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of S is non empty set

the carrier of A is non empty set

the carrier of B is non empty set

the carrier of (R,V,S,B) is non empty set

the carrier of S /\ the carrier of B is set

the carrier of A /\ the carrier of B is set

the carrier of (R,V,A,B) is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

C is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

(0). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,((0). V),S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,((0). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

0. V is V47(V) Element of the carrier of V

the carrier of V is non empty set

the ZeroF of V is Element of the carrier of V

the carrier of S is non empty set

{(0. V)} is Element of bool the carrier of V

bool the carrier of V is non empty set

{(0. V)} /\ the carrier of S is Element of bool the carrier of V

the carrier of (R,V,((0). V),S) is non empty set

the carrier of ((0). V) is non empty set

the carrier of ((0). V) /\ the carrier of S is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

S is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,((Omega). V),S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,((Omega). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,((Omega). V),S) is non empty set

the carrier of S is non empty set

the carrier of V /\ the carrier of S is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() strict RightMod-like RightModStr over R

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

(R,V,((Omega). V),((Omega). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,S,A) is non empty set

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,S,A) is non empty set

the carrier of S is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,(R,V,S,A),A) is non empty set

the carrier of A is non empty set

B is set

the carrier of V is non empty set

{ (b

C is Element of the carrier of V

W1 is Element of the carrier of V

C + W1 is Element of the carrier of V

B is set

(R,V,A,(R,V,S,A)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,A,(R,V,S,A)) is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of S is non empty set

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,(R,V,S,A)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,S,(R,V,S,A)) is non empty set

B is set

the carrier of (R,V,S,A) is non empty set

the carrier of S /\ the carrier of (R,V,S,A) is set

B is set

the carrier of V is non empty set

C is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

C + (0. V) is Element of the carrier of V

{ (b

the carrier of (R,V,S,A) is non empty set

the carrier of S /\ the carrier of (R,V,S,A) is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,(R,V,A,S)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,(R,V,S,A),(R,V,A,B)) is non empty set

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,(R,V,S,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,A,(R,V,S,B)) is non empty set

C is set

the carrier of V is non empty set

{ (b

W1 is Element of the carrier of V

W3 is Element of the carrier of V

W1 + W3 is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,(R,V,S,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,(R,V,S,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,A,(R,V,S,B)) is non empty set

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,(R,V,S,A),(R,V,A,B)) is non empty set

C is set

the carrier of A is non empty set

the carrier of (R,V,S,B) is non empty set

the carrier of A /\ the carrier of (R,V,S,B) is set

the carrier of V is non empty set

{ (b

W1 is Element of the carrier of V

W3 is Element of the carrier of V

W1 + W3 is Element of the carrier of V

W3 + W1 is Element of the carrier of V

(W3 + W1) - W1 is Element of the carrier of V

- W1 is Element of the carrier of V

K154(V,(W3 + W1),(- W1)) is Element of the carrier of V

W1 - W1 is Element of the carrier of V

K154(V,W1,(- W1)) is Element of the carrier of V

W3 + (W1 - W1) is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

W3 + (0. V) is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,(R,V,S,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,S,(R,V,A,B)) is non empty set

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,A,S),(R,V,S,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,(R,V,A,S),(R,V,S,B)) is non empty set

C is set

the carrier of V is non empty set

{ (b

W1 is Element of the carrier of V

W3 is Element of the carrier of V

W1 + W3 is Element of the carrier of V

{ (b

the carrier of (R,V,S,B) is non empty set

{ (b

the carrier of (R,V,A,S) is non empty set

the carrier of (R,V,A,S) /\ the carrier of (R,V,S,B) is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,A,S),(R,V,S,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,(R,V,S,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,A,(R,V,S,B)) is non empty set

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of (R,V,(R,V,S,A),(R,V,A,B)) is non empty set

the carrier of V is non empty set

bool the carrier of V is non empty set

the carrier of A is non empty set

C is Element of bool the carrier of V

the carrier of S is non empty set

W1 is set

the carrier of (R,V,S,A) is non empty set

the carrier of (R,V,A,B) is non empty set

the carrier of (R,V,S,A) /\ the carrier of (R,V,A,B) is set

{ (b

W3 is Element of the carrier of V

W2 is Element of the carrier of V

W3 + W2 is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

(W3 + W2) + (0. V) is Element of the carrier of V

{ (b

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,(R,V,S,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,B,(R,V,A,S)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,B,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,B,A),S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,(R,V,B,A)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,B,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,B,S),(R,V,S,A)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,B,(R,V,S,A)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,B),(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,B,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,B),(R,V,B,A)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,B),B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,(R,V,S,B),B),A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,B,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,(R,V,B,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,(R,V,B,B)),A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,B),A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,(R,V,B,A)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,(R,V,A,B)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,(R,V,S,A),B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,A,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

B is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,B) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

C is Element of the carrier of V

W1 is Element of the carrier of V

W3 is Element of the carrier of V

W1 + W3 is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of S is non empty set

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of A is non empty set

the carrier of S \/ the carrier of A is set

W1 is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of W1 is non empty set

W2 is set

the carrier of V is non empty set

AB is Element of the carrier of A

bool the carrier of V is non empty set

u is Element of bool the carrier of V

v21 is set

v22 is Element of the carrier of S

x is Element of bool the carrier of V

v is Element of the carrier of V

BC is Element of the carrier of V

v + BC is Element of the carrier of V

(v + BC) - BC is Element of the carrier of V

- BC is Element of the carrier of V

K154(V,(v + BC),(- BC)) is Element of the carrier of V

BC - BC is Element of the carrier of V

K154(V,BC,(- BC)) is Element of the carrier of V

v + (BC - BC) is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

v + (0. V) is Element of the carrier of V

x is Element of bool the carrier of V

BC + v is Element of the carrier of V

(BC + v) - v is Element of the carrier of V

- v is Element of the carrier of V

K154(V,(BC + v),(- v)) is Element of the carrier of V

v - v is Element of the carrier of V

K154(V,v,(- v)) is Element of the carrier of V

BC + (v - v) is Element of the carrier of V

BC + (0. V) is Element of the carrier of V

W1 is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of W1 is non empty set

W3 is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of W3 is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

the carrier of V is non empty set

bool the carrier of V is non empty set

S is set

B is set

W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

A is set

the carrier of W1 is non empty set

C is set

W3 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of W3 is non empty set

A is Relation-like Function-like set

B is set

C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of C is non empty set

[B,C] is set

{B,C} is set

{B} is set

{{B,C},{B}} is set

C is set

[B,C] is set

{B,C} is set

{B} is set

{{B,C},{B}} is set

dom A is set

rng A is set

B is set

C is set

A . C is set

[C,B] is set

{C,B} is set

{C} is set

{{C,B},{C}} is set

W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of W1 is non empty set

C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

W1 is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of W1 is non empty set

W3 is set

[W3,B] is set

{W3,B} is set

{W3} is set

{{W3,B},{W3}} is set

A . W3 is set

S is set

A is set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

(R,V) is set

the non empty V89() V136() V137() V138() strict RightMod-like Submodule of V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() strict RightMod-like RightModStr over R

(R,V) is non empty set

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

the carrier of ((Omega). V) is non empty set

S is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of S is non empty set

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is Element of the carrier of V

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is Element of the carrier of V

C is Element of the carrier of V

W1 is Element of the carrier of V

C + W1 is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

the carrier of V is non empty set

S is Element of the carrier of V

A is Element of the carrier of V

B is Element of the carrier of V

A + B is Element of the carrier of V

S - B is Element of the carrier of V

- B is Element of the carrier of V

K154(V,S,(- B)) is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

(0. V) + A is Element of the carrier of V

B + A is Element of the carrier of V

- (B + A) is Element of the carrier of V

S + (- (B + A)) is Element of the carrier of V

(S + (- (B + A))) + A is Element of the carrier of V

- A is Element of the carrier of V

(- B) + (- A) is Element of the carrier of V

S + ((- B) + (- A)) is Element of the carrier of V

(S + ((- B) + (- A))) + A is Element of the carrier of V

S + (- B) is Element of the carrier of V

(S + (- B)) + (- A) is Element of the carrier of V

((S + (- B)) + (- A)) + A is Element of the carrier of V

(- A) + A is Element of the carrier of V

(S + (- B)) + ((- A) + A) is Element of the carrier of V

(S + (- B)) + (0. V) is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

S + (0. V) is Element of the carrier of V

- A is Element of the carrier of V

A + (- A) is Element of the carrier of V

S + (A + (- A)) is Element of the carrier of V

S + A is Element of the carrier of V

- (S - B) is Element of the carrier of V

(S + A) + (- (S - B)) is Element of the carrier of V

- S is Element of the carrier of V

(- S) + B is Element of the carrier of V

(S + A) + ((- S) + B) is Element of the carrier of V

(S + A) + (- S) is Element of the carrier of V

((S + A) + (- S)) + B is Element of the carrier of V

S + (- S) is Element of the carrier of V

(S + (- S)) + A is Element of the carrier of V

((S + (- S)) + A) + B is Element of the carrier of V

(0. V) + A is Element of the carrier of V

((0. V) + A) + B is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(0). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,A,S) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() strict RightMod-like RightModStr over R

(0). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the carrier of V is non empty set

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

(R,V,((0). V),((Omega). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(R,V,((0). V),((Omega). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

the carrier of V is non empty set

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

B is Coset of S

C is Coset of A

B /\ C is Element of bool the carrier of V

bool the carrier of V is non empty set

the Element of B /\ C is Element of B /\ C

W2 is Element of the carrier of V

W2 + A is Element of bool the carrier of V

{ (W2 + b

W2 + S is Element of bool the carrier of V

{ (W2 + b

W2 + (R,V,S,A) is Element of bool the carrier of V

{ (W2 + b

AB is set

BC is Element of the carrier of V

W2 + BC is Element of the carrier of V

u is Element of the carrier of V

W2 + u is Element of the carrier of V

AB is set

BC is Element of the carrier of V

W2 + BC is Element of the carrier of V

R is non empty V89() V115() V122() V123() V136() V137() V138() L14()

V is non empty V89() V136() V137() V138() RightMod-like RightModStr over R

the carrier of V is non empty set

S is non empty V89() V136() V137() V138() RightMod-like Submodule of V

A is non empty V89() V136() V137() V138() RightMod-like Submodule of V

the carrier of S is non empty set

the carrier of A is non empty set

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(Omega). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

the U7 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the ZeroF of V is Element of the carrier of V

the rmult of V is Relation-like [: the carrier of V, the carrier of R:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]

the carrier of R is non empty set

[: the carrier of V, the carrier of R:] is Relation-like non empty set

[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set

RightModStr(# the carrier of V, the U7 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R

W1 is Coset of S

W3 is Coset of A

W1 /\ W3 is Element of bool the carrier of V

bool the carrier of V is non empty set

W2 is Element of the carrier of V

W2 + S is Element of bool the carrier of V

{ (W2 + b

AB is Element of the carrier of V

BC is Element of the carrier of V

AB + BC is Element of the carrier of V

u is Element of the carrier of V

u + A is Element of bool the carrier of V

{ (u + b

v21 is Element of the carrier of V

v22 is Element of the carrier of V

v21 + v22 is Element of the carrier of V

BC + v21 is Element of the carrier of V

v is Element of the carrier of V

{v} is Element of bool the carrier of V

x is set

u - v22 is Element of the carrier of V

- v22 is Element of the carrier of V

K154(V,u,(- v22)) is Element of the carrier of V

v21 + A is Element of bool the carrier of V

{ (v21 + b

W2 - AB is Element of the carrier of V

- AB is Element of the carrier of V

K154(V,W2,(- AB)) is Element of the carrier of V

BC + S is Element of bool the carrier of V

{ (BC + b

x is set

(R,V,S,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

(0). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V

C is Coset of (R,V,S,A)

c

{c

the carrier of (R,V,S,A) is non empty set

W1 is set

W3 is Element of the carrier of V

W2 is Coset of S

W2 /\ the carrier of A is Element of bool the carrier of V

bool the carrier of V is non empty set

AB is Element of the carrier of V

{AB} is Element of bool the carrier of V

BC is Element of the carrier of V

W3 - BC is Element of the carrier of V

- BC is