:: 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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in A ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in B & b₂ in C ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in A ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in A ) } is set
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₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in A ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in A & b₂ in S ) } is 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
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in A ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in A ) } is set
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₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in A ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in A & b₂ in B ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in (R,V,S,A) & b₂ in B ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in (R,V,A,B) ) } is set
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₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in B & b₂ in A ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in B & b₂ in S ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in (R,V,S,A) & b₂ in A ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in A ) } 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
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in (R,V,S,A) & b₂ in (R,V,A,B) ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in B ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in (R,V,A,B) ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in B ) } is set
the carrier of (R,V,S,B) is non empty set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in A & b₂ in S ) } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in S & b₂ in A ) } 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
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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in A & b₂ in (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,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₁) where b₁ is Element of the carrier of V : b₁ in A } is set
W2 + S is Element of bool the carrier of V
{ (W2 + b₁) where b₁ is Element of the carrier of V : b₁ in S } is set
W2 + (R,V,S,A) is Element of bool the carrier of V
{ (W2 + b₁) where b₁ is Element of the carrier of V : b₁ in (R,V,S,A) } is set
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₁) where b₁ is Element of the carrier of V : b₁ in S } 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
u is Element of the carrier of V
u + A is Element of bool the carrier of V
{ (u + b₁) where b₁ is Element of the carrier of V : b₁ in A } is 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
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₁) where b₁ is Element of the carrier of V : b₁ in A } is set
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₁) where b₁ is Element of the carrier of V : b₁ in S } is set
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₁₈ is Element of the carrier of V
{c₁₈} is Element of bool 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 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 Element of the carrier of V
K154(V,W3,(- BC)) is Element of the carrier of V
BC + AB is Element of the carrier of V
the carrier of S /\ the carrier of A is set
W1 is Element of the carrier of V
{W1} is Element of bool the carrier of V
bool the carrier of V is non empty 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
0. V is V47(V) Element of the carrier of V
the carrier of ((0). V) is non empty set
{(0. V)} is Element of bool the carrier of V
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() strict RightMod-like RightModStr over R
the carrier of V is non empty set
C is non empty V89() V115() V122() V123() V136() V137() V138() L14()
W1 is non empty V89() V136() V137() V138() strict RightMod-like RightModStr over C
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
the carrier of W1 is non empty set
W3 is non empty V89() V136() V137() V138() RightMod-like Submodule of W1
W2 is non empty V89() V136() V137() V138() RightMod-like Submodule of W1
(C,W1,W3,W2) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of W1
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 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
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
C + A is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (C + b₁) where b₁ is Element of the carrier of V : b₁ in A } is set
the carrier of S is non empty set
AB is Coset of A
BC is Coset of S
BC /\ AB is Element of bool the carrier of V
u is Element of the carrier of V
{u} is Element of bool the carrier of V
W1 - W2 is Element of the carrier of V
- W2 is Element of the carrier of V
K154(V,W1,(- W2)) is Element of the carrier of V
(C + W1) - W2 is Element of the carrier of V
K154(V,(C + W1),(- W2)) is Element of the carrier of V
C + (W1 - 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
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
(0). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
the carrier of ((0). 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
{(0. V)} is Element of bool the carrier of V
bool the carrier of V 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 Element of the carrier of V
C 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
(W3 + W2) + (0. V) is Element of the carrier of V
W1 is Element of the carrier of V
W1 - W1 is Element of the carrier of V
- W1 is Element of the carrier of V
K154(V,W1,(- W1)) is Element of the carrier of V
(W3 + W2) + (W1 - W1) is Element of the carrier of V
(W3 + W2) + W1 is Element of the carrier of V
((W3 + W2) + W1) - W1 is Element of the carrier of V
K154(V,((W3 + W2) + W1),(- W1)) is Element of the carrier of V
W3 + W1 is Element of the carrier of V
(W3 + W1) + W2 is Element of the carrier of V
((W3 + W1) + W2) - W1 is Element of the carrier of V
K154(V,((W3 + W1) + W2),(- W1)) is Element of the carrier of V
W2 - W1 is Element of the carrier of V
K154(V,W2,(- W1)) is Element of the carrier of V
(W3 + W1) + (W2 - W1) is Element of the carrier of V
W2 + (- W1) is Element of the carrier of V
W2 + (0. V) is Element of the carrier of V
- (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
the carrier of V is non empty set
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
[: the carrier of V, the carrier of V:] is Relation-like non empty set
S is Element of the carrier of V
(R,V,A,B) 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:], 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
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,W1] is Element of [: the carrier of V, the carrier of V:]
{C,W1} is set
{C} is set
{{C,W1},{C}} is set
[C,W1] `1 is Element of the carrier of V
[C,W1] `2 is Element of the carrier of V
([C,W1] `1) + ([C,W1] `2) is Element of the carrier of V
C is Element of [: the carrier of V, the carrier of V:]
C `1 is Element of the carrier of V
C `2 is Element of the carrier of V
(C `1) + (C `2) is Element of the carrier of V
W1 is Element of [: the carrier of V, the carrier of V:]
W1 `1 is Element of the carrier of V
W1 `2 is Element of the carrier of V
(W1 `1) + (W1 `2) is Element of the carrier of V
[(C `1),(C `2)] is Element of [: the carrier of V, the carrier of V:]
{(C `1),(C `2)} is set
{(C `1)} is set
{{(C `1),(C `2)},{(C `1)}} 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
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 is Element of the carrier of V
(R,V,B,S,A) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
(R,V,B,S,A) `1 is Element of the carrier of V
(R,V,B,A,S) is Element of [: the carrier of V, the carrier of V:]
(R,V,B,A,S) `2 is Element of the carrier of V
(R,V,B,S,A) `2 is Element of the carrier of V
(R,V,B,A,S) `1 is Element of the carrier of V
((R,V,B,A,S) `2) + ((R,V,B,A,S) `1) is Element of the carrier of V
((R,V,B,S,A) `1) + ((R,V,B,S,A) `2) 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
B is Element of the carrier of V
(R,V,B,S,A) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
(R,V,B,S,A) `2 is Element of the carrier of V
(R,V,B,A,S) is Element of [: the carrier of V, the carrier of V:]
(R,V,B,A,S) `1 is Element of the carrier of V
(R,V,B,A,S) `2 is Element of the carrier of V
((R,V,B,A,S) `2) + ((R,V,B,A,S) `1) is Element of the carrier of V
(R,V,B,S,A) `1 is Element of the carrier of V
((R,V,B,S,A) `1) + ((R,V,B,S,A) `2) 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
(R,V) is non empty set
[:(R,V),(R,V):] is Relation-like non empty set
[:[:(R,V),(R,V):],(R,V):] is Relation-like non empty set
bool [:[:(R,V),(R,V):],(R,V):] is non empty set
S is Element of (R,V)
A is Element of (R,V)
B is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,B,C) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W1 is Element of (R,V)
W3 is non empty V89() V136() V137() V138() RightMod-like Submodule of V
W2 is non empty V89() V136() V137() V138() RightMod-like Submodule of V
(R,V,W3,W2) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
S is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
S is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
A is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
B is set
C is set
W2 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
AB is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W1 is Element of (R,V)
W3 is Element of (R,V)
S . (W1,W3) is Element of (R,V)
(R,V,W2,AB) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
S . (B,C) is set
A . (B,C) 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 non empty set
[:(R,V),(R,V):] is Relation-like non empty set
[:[:(R,V),(R,V):],(R,V):] is Relation-like non empty set
bool [:[:(R,V),(R,V):],(R,V):] is non empty set
S is Element of (R,V)
A is Element of (R,V)
B is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,B,C) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W1 is Element of (R,V)
W3 is non empty V89() V136() V137() V138() RightMod-like Submodule of V
W2 is non empty V89() V136() V137() V138() RightMod-like Submodule of V
(R,V,W3,W2) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
S is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
S is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
A is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
B is set
C is set
W2 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
AB is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W1 is Element of (R,V)
W3 is Element of (R,V)
S . (W1,W3) is Element of (R,V)
(R,V,W2,AB) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
S . (B,C) is set
A . (B,C) 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 non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
[:(R,V),(R,V):] is Relation-like non empty set
[:[:(R,V),(R,V):],(R,V):] is Relation-like non empty set
bool [:[:(R,V),(R,V):],(R,V):] is non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
LattStr(# (R,V),(R,V),(R,V) #) is non empty strict LattStr
the carrier of LattStr(# (R,V),(R,V),(R,V) #) is non empty set
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "/\" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B "/\" A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (A,B) is set
(R,V,C,W1) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W1,C) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (B,A) is set
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "/\" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(A "/\" B) "\/" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,C,W1) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . ((A "/\" B),B) is set
(R,V) . (A,B) is set
(R,V) . (((R,V) . (A,B)),B) is set
W3 is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(R,V) . (W3,B) is set
(R,V,(R,V,C,W1),W1) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B "/\" C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "/\" (B "/\" C) is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "/\" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(A "/\" B) "/\" C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W3 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W2 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W1,W3) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W3,W2) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (A,(B "/\" C)) is set
(R,V) . (B,C) is set
(R,V) . (A,((R,V) . (B,C))) is set
BC is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(R,V) . (A,BC) is set
(R,V,W1,(R,V,W3,W2)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,(R,V,W1,W3),W2) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
AB is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(R,V) . (AB,C) is set
(R,V) . (A,B) is set
(R,V) . (((R,V) . (A,B)),C) is set
(R,V) . ((A "/\" B),C) is set
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B "\/" C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "\/" (B "\/" C) is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "\/" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(A "\/" B) "\/" C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W3 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W2 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W1,W3) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W3,W2) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (A,(B "\/" C)) is set
(R,V) . (B,C) is set
(R,V) . (A,((R,V) . (B,C))) is set
BC is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(R,V) . (A,BC) is set
(R,V,W1,(R,V,W3,W2)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,(R,V,W1,W3),W2) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
AB is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(R,V) . (AB,C) is set
(R,V) . (A,B) is set
(R,V) . (((R,V) . (A,B)),C) is set
(R,V) . ((A "\/" B),C) is set
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "\/" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "/\" (A "\/" B) is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,C,W1) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (A,(A "\/" B)) is set
(R,V) . (A,B) is set
(R,V) . (A,((R,V) . (A,B))) is set
W3 is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(R,V) . (A,W3) is set
(R,V,C,(R,V,C,W1)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "\/" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B "\/" A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (A,B) is set
(R,V,C,W1) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W1,C) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (B,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 non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
[:(R,V),(R,V):] is Relation-like non empty set
[:[:(R,V),(R,V):],(R,V):] is Relation-like non empty set
bool [:[:(R,V),(R,V):],(R,V):] is non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
LattStr(# (R,V),(R,V),(R,V) #) is non empty strict LattStr
the carrier of LattStr(# (R,V),(R,V),(R,V) #) is non empty set
(0). V is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "/\" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B "/\" A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (A,B) is set
(R,V,((0). V),C) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (B,A) is set
(R,V,C,((0). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,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
(R,V) is non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
[:(R,V),(R,V):] is Relation-like non empty set
[:[:(R,V),(R,V):],(R,V):] is Relation-like non empty set
bool [:[:(R,V),(R,V):],(R,V):] is non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
LattStr(# (R,V),(R,V),(R,V) #) is non empty strict LattStr
the carrier of LattStr(# (R,V),(R,V),(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
A is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
the carrier of A is non empty set
B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B "\/" C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C "\/" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (B,C) is set
(R,V,A,W1) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,((Omega). V),W1) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (C,B) is set
(R,V,W1,A) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W1,((Omega). V)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,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
(R,V) is non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
[:(R,V),(R,V):] is Relation-like non empty set
[:[:(R,V),(R,V):],(R,V):] is Relation-like non empty set
bool [:[:(R,V),(R,V):],(R,V):] is non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
LattStr(# (R,V),(R,V),(R,V) #) is non empty strict LattStr
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 non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
[:(R,V),(R,V):] is Relation-like non empty set
[:[:(R,V),(R,V):],(R,V):] is Relation-like non empty set
bool [:[:(R,V),(R,V):],(R,V):] is non empty set
(R,V) is Relation-like [:(R,V),(R,V):] -defined (R,V) -valued Function-like V18([:(R,V),(R,V):],(R,V)) Element of bool [:[:(R,V),(R,V):],(R,V):]
LattStr(# (R,V),(R,V),(R,V) #) is non empty strict LattStr
the carrier of LattStr(# (R,V),(R,V),(R,V) #) is non empty set
A is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
B "/\" C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "\/" (B "/\" C) is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
A "\/" B is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(A "\/" B) "/\" C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
W1 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
W3 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W1,W3) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (A,C) is set
A "\/" C is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
W2 is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W1,W2) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,W2,W3) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V) . (A,(B "/\" C)) is set
(R,V) . (B,C) is set
(R,V) . (A,((R,V) . (B,C))) is set
BC is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(R,V) . (A,BC) is set
(R,V,W1,(R,V,W2,W3)) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
(R,V,(R,V,W1,W2),W3) is non empty V89() V136() V137() V138() strict RightMod-like Submodule of V
AB is Element of the carrier of LattStr(# (R,V),(R,V),(R,V) #)
(R,V) . (AB,C) is set
(R,V) . (A,B) is set
(R,V) . (((R,V) . (A,B)),C) is set
(R,V) . ((A "\/" B),C) is set