:: RMOD_4 semantic presentation

REAL is set
NAT is non empty V12() V26() V27() V28() non finite cardinal limit_cardinal Element of K19(REAL)
K19(REAL) is non empty set
NAT is non empty V12() V26() V27() V28() non finite cardinal limit_cardinal set
K19(NAT) is non empty V12() non finite set
K19(NAT) is non empty V12() non finite set
COMPLEX is set
RAT is set
INT is set
{} is Function-like functional empty ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() set
the Function-like functional empty ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() set is Function-like functional empty ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() set
2 is non empty ext-real positive V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
1 is non empty ext-real positive V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
3 is non empty ext-real positive V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
Seg 1 is non empty V12() finite 1 -element Element of K19(NAT)
{1} is non empty V12() finite V38() 1 -element set
Seg 2 is non empty finite 2 -element Element of K19(NAT)
{1,2} is non empty finite V38() set
Seg 3 is non empty finite 3 -element Element of K19(NAT)
K44(1,2,3) is non empty finite set
0 is Function-like functional empty ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of NAT
dom {} is set
rng {} is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len B is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
B . (len B) is set
Sum B is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(len v) + 1 is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
Seg (len v) is finite len v -element Element of K19(NAT)
B | (Seg (len v)) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT, the carrier of V))
K20(NAT, the carrier of V) is non empty V12() non finite set
K19(K20(NAT, the carrier of V)) is non empty V12() non finite set
Sum v is Element of the carrier of V
(Sum v) + A is Element of the carrier of V
dom v is finite set
B | (dom v) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT, the carrier of V))
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of R
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len B is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom B is finite set
Sum B is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
Sum v is Element of the carrier of V
(Sum v) * A is Element of the carrier of V
l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
C is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len C is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
l + 1 is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom D is finite set
Seg l is finite l -element Element of K19(NAT)
D | (Seg l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT, the carrier of V))
K20(NAT, the carrier of V) is non empty V12() non finite set
K19(K20(NAT, the carrier of V)) is non empty V12() non finite set
C | (Seg l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT, the carrier of V))
f is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
C is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len C is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom f is finite set
f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
f is Element of the carrier of V
C . f is set
dom C is finite set
C . f is set
D . f is set
f * A is Element of the carrier of V
f . f is set
Seg (l + 1) is finite l + 1 -element Element of K19(NAT)
dom C is finite set
D . (l + 1) is set
C . (l + 1) is set
f is Element of the carrier of V
f is Element of the carrier of V
f * A is Element of the carrier of V
Sum D is Element of the carrier of V
Sum f is Element of the carrier of V
(Sum f) + f is Element of the carrier of V
Sum C is Element of the carrier of V
(Sum C) * A is Element of the carrier of V
((Sum C) * A) + (f * A) is Element of the carrier of V
(Sum C) + f is Element of the carrier of V
((Sum C) + f) * A is Element of the carrier of V
Sum C is Element of the carrier of V
(Sum C) * A is Element of the carrier of V
l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
C is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len C is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
l + 1 is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom D is finite set
Sum D is Element of the carrier of V
Sum C is Element of the carrier of V
(Sum C) * A is Element of the carrier of V
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom l is finite set
<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like one-to-one constant functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() FinSequence of the carrier of V
Sum l is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
Sum D is Element of the carrier of V
(Sum D) * A is Element of the carrier of V
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom l is finite set
Sum l is Element of the carrier of V
Sum D is Element of the carrier of V
(Sum D) * A is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of R
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len B is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom B is finite set
Sum B is Element of the carrier of V
(Sum B) * A is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
Sum v is Element of the carrier of V
l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
dom v is finite set
D is Element of the carrier of V
B . l is set
B /. l is Element of the carrier of V
v . l is set
D * A is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like one-to-one constant functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() FinSequence of the carrier of V
K20(NAT, the carrier of V) is non empty V12() non finite set
Sum (<*> the carrier of V) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
A is Element of the carrier of R
(Sum (<*> the carrier of V)) * A is Element of the carrier of V
(0. V) * A is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of R
B is Element of the carrier of V
B * A is Element of the carrier of V
v is Element of the carrier of V
<*B,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum <*B,v*> is Element of the carrier of V
(Sum <*B,v*>) * A is Element of the carrier of V
v * A is Element of the carrier of V
(B * A) + (v * A) is Element of the carrier of V
B + v is Element of the carrier of V
(B + v) * A is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of R
B is Element of the carrier of V
B * A is Element of the carrier of V
v is Element of the carrier of V
v * A is Element of the carrier of V
(B * A) + (v * A) is Element of the carrier of V
l is Element of the carrier of V
<*B,v,l*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum <*B,v,l*> is Element of the carrier of V
(Sum <*B,v,l*>) * A is Element of the carrier of V
l * A is Element of the carrier of V
((B * A) + (v * A)) + (l * A) is Element of the carrier of V
B + v is Element of the carrier of V
(B + v) + l is Element of the carrier of V
((B + v) + l) * A is Element of the carrier of V
(B + v) * A is Element of the carrier of V
((B + v) * A) + (l * A) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is finite Element of K19( the carrier of V)
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng B is finite set
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum v is Element of the carrier of V
rng v is finite set
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng l is finite set
B is Element of the carrier of V
Sum l is Element of the carrier of V
D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng D is finite set
v is Element of the carrier of V
Sum D is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
{} V is Function-like functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of K19( the carrier of V)
the carrier of V is non empty set
K19( the carrier of V) is non empty set
(R,V,({} V)) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like one-to-one constant functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() FinSequence of the carrier of V
K20(NAT, the carrier of V) is non empty V12() non finite set
Sum (<*> the carrier of V) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
{A} is non empty V12() finite 1 -element Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
(R,V,{A}) is Element of the carrier of V
<*A*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum <*A*> is Element of the carrier of V
rng <*A*> is V12() finite set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
(R,V,{A,B}) is Element of the carrier of V
A + B is Element of the carrier of V
<*A,B*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng <*A,B*> is finite set
Sum <*A,B*> is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
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
v is Element of the carrier of V
{A,B,v} is non empty finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
(R,V,{A,B,v}) is Element of the carrier of V
(A + B) + v is Element of the carrier of V
<*A,B,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng <*A,B,v*> is finite set
Sum <*A,B,v*> is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is finite Element of K19( the carrier of V)
(R,V,A) is Element of the carrier of V
B is finite Element of K19( the carrier of V)
A \/ B is finite Element of K19( the carrier of V)
(R,V,(A \/ B)) is Element of the carrier of V
(R,V,B) is Element of the carrier of V
(R,V,A) + (R,V,B) is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v is finite set
Sum v is Element of the carrier of V
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng l is finite set
Sum l is Element of the carrier of V
D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng D is finite set
Sum D is Element of the carrier of V
l ^ D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng (l ^ D) is finite set
Sum (l ^ D) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is finite Element of K19( the carrier of V)
(R,V,A) is Element of the carrier of V
B is finite Element of K19( the carrier of V)
A \/ B is finite Element of K19( the carrier of V)
(R,V,(A \/ B)) is Element of the carrier of V
(R,V,B) is Element of the carrier of V
(R,V,A) + (R,V,B) is Element of the carrier of V
A /\ B is finite Element of K19( the carrier of V)
(R,V,(A /\ B)) is Element of the carrier of V
((R,V,A) + (R,V,B)) - (R,V,(A /\ B)) is Element of the carrier of V
B \ A is finite Element of K19( the carrier of V)
A \ B is finite Element of K19( the carrier of V)
(B \ A) \/ (A \ B) is finite Element of K19( the carrier of V)
(B \ A) \/ (A /\ B) is finite Element of K19( the carrier of V)
(A \ B) \/ (A /\ B) is finite Element of K19( the carrier of V)
A \+\ B is finite Element of K19( the carrier of V)
A \ B is finite set
B \ A is finite set
(A \ B) \/ (B \ A) is finite set
((B \ A) \/ (A \ B)) \/ (A /\ B) is finite Element of K19( the carrier of V)
(R,V,(A \/ B)) + (R,V,(A /\ B)) is Element of the carrier of V
(R,V,((B \ A) \/ (A \ B))) is Element of the carrier of V
(R,V,((B \ A) \/ (A \ B))) + (R,V,(A /\ B)) is Element of the carrier of V
((R,V,((B \ A) \/ (A \ B))) + (R,V,(A /\ B))) + (R,V,(A /\ B)) is Element of the carrier of V
(R,V,(B \ A)) is Element of the carrier of V
(R,V,(A \ B)) is Element of the carrier of V
(R,V,(B \ A)) + (R,V,(A \ B)) is Element of the carrier of V
((R,V,(B \ A)) + (R,V,(A \ B))) + (R,V,(A /\ B)) is Element of the carrier of V
(((R,V,(B \ A)) + (R,V,(A \ B))) + (R,V,(A /\ B))) + (R,V,(A /\ B)) is Element of the carrier of V
(R,V,(A /\ B)) + (R,V,(A \ B)) is Element of the carrier of V
(R,V,(B \ A)) + ((R,V,(A /\ B)) + (R,V,(A \ B))) is Element of the carrier of V
((R,V,(B \ A)) + ((R,V,(A /\ B)) + (R,V,(A \ B)))) + (R,V,(A /\ B)) is Element of the carrier of V
(R,V,(B \ A)) + (R,V,(A /\ B)) is Element of the carrier of V
(R,V,(A \ B)) + (R,V,(A /\ B)) is Element of the carrier of V
((R,V,(B \ A)) + (R,V,(A /\ B))) + ((R,V,(A \ B)) + (R,V,(A /\ B))) is Element of the carrier of V
(R,V,B) + ((R,V,(A \ B)) + (R,V,(A /\ B))) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is finite Element of K19( the carrier of V)
(R,V,A) is Element of the carrier of V
B is finite Element of K19( the carrier of V)
A /\ B is finite Element of K19( the carrier of V)
(R,V,(A /\ B)) is Element of the carrier of V
(R,V,B) is Element of the carrier of V
(R,V,A) + (R,V,B) is Element of the carrier of V
A \/ B is finite Element of K19( the carrier of V)
(R,V,(A \/ B)) is Element of the carrier of V
((R,V,A) + (R,V,B)) - (R,V,(A \/ B)) is Element of the carrier of V
((R,V,A) + (R,V,B)) - (R,V,(A /\ B)) is Element of the carrier of V
(R,V,(A /\ B)) + (R,V,(A \/ B)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is finite Element of K19( the carrier of V)
B is finite Element of K19( the carrier of V)
A \ B is finite Element of K19( the carrier of V)
(R,V,(A \ B)) is Element of the carrier of V
A \/ B is finite Element of K19( the carrier of V)
(R,V,(A \/ B)) is Element of the carrier of V
(R,V,B) is Element of the carrier of V
(R,V,(A \/ B)) - (R,V,B) is Element of the carrier of V
(A \ B) /\ B is finite Element of K19( the carrier of V)
{} V is Function-like functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of K19( the carrier of V)
(A \ B) \/ B is finite Element of K19( the carrier of V)
(R,V,(A \ B)) + (R,V,B) is Element of the carrier of V
(R,V,((A \ B) /\ B)) is Element of the carrier of V
((R,V,(A \ B)) + (R,V,B)) - (R,V,((A \ B) /\ B)) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
((R,V,(A \ B)) + (R,V,B)) - (0. V) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is finite Element of K19( the carrier of V)
(R,V,A) is Element of the carrier of V
B is finite Element of K19( the carrier of V)
A \ B is finite Element of K19( the carrier of V)
(R,V,(A \ B)) is Element of the carrier of V
A /\ B is finite Element of K19( the carrier of V)
(R,V,(A /\ B)) is Element of the carrier of V
(R,V,A) - (R,V,(A /\ B)) is Element of the carrier of V
A \ (A /\ B) is finite Element of K19( the carrier of V)
A \/ (A /\ B) is finite Element of K19( the carrier of V)
(R,V,(A \/ (A /\ B))) is Element of the carrier of V
(R,V,(A \/ (A /\ B))) - (R,V,(A /\ B)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is finite Element of K19( the carrier of V)
B is finite Element of K19( the carrier of V)
A \+\ B is finite Element of K19( the carrier of V)
A \ B is finite set
B \ A is finite set
(A \ B) \/ (B \ A) is finite set
(R,V,(A \+\ B)) is Element of the carrier of V
A \/ B is finite Element of K19( the carrier of V)
(R,V,(A \/ B)) is Element of the carrier of V
A /\ B is finite Element of K19( the carrier of V)
(R,V,(A /\ B)) is Element of the carrier of V
(R,V,(A \/ B)) - (R,V,(A /\ B)) is Element of the carrier of V
(A \/ B) \ (A /\ B) is finite Element of K19( the carrier of V)
(A \/ B) /\ (A /\ B) is finite Element of K19( the carrier of V)
(R,V,((A \/ B) /\ (A /\ B))) is Element of the carrier of V
(R,V,(A \/ B)) - (R,V,((A \/ B) /\ (A /\ B))) is Element of the carrier of V
(A \/ B) /\ A is finite Element of K19( the carrier of V)
((A \/ B) /\ A) /\ B is finite Element of K19( the carrier of V)
(R,V,(((A \/ B) /\ A) /\ B)) is Element of the carrier of V
(R,V,(A \/ B)) - (R,V,(((A \/ B) /\ A) /\ B)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is finite Element of K19( the carrier of V)
B is finite Element of K19( the carrier of V)
A \+\ B is finite Element of K19( the carrier of V)
A \ B is finite set
B \ A is finite set
(A \ B) \/ (B \ A) is finite set
(R,V,(A \+\ B)) is Element of the carrier of V
A \ B is finite Element of K19( the carrier of V)
(R,V,(A \ B)) is Element of the carrier of V
B \ A is finite Element of K19( the carrier of V)
(R,V,(B \ A)) is Element of the carrier of V
(R,V,(A \ B)) + (R,V,(B \ A)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{} V is Function-like functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of K19( the carrier of V)
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
the carrier of V --> (0. R) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
A is finite Element of K19( the carrier of V)
l is Element of the carrier of V
v . l is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
K19( the carrier of V) is non empty set
v is finite Element of K19( the carrier of V)
l is set
D is Element of the carrier of V
A . D is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
v is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
l is non empty V73() V98() V99() V100() RightMod-like RightModStr over v
the carrier of l is non empty set
the carrier of v is non empty set
A is set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
D is set
f is Element of the carrier of l
C is Relation-like the carrier of l -defined the carrier of v -valued Function-like quasi_total (v,l)
C . f is Element of the carrier of v
0. v is V54(v) Element of the carrier of v
(v,l,C) is finite Element of K19( the carrier of l)
K19( the carrier of l) is non empty set
{ b₁ where b₁ is Element of the carrier of l : not C . b₁ = 0. v } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
0. R is V54(R) Element of the carrier of R
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B . A is Element of the carrier of R
(R,V,B) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
v is Element of the carrier of V
B . v is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
0. R is V54(R) Element of the carrier of R
the carrier of V --> (0. R) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
K19( the carrier of V) is non empty set
{} V is Function-like functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of K19( the carrier of V)
v is Function-like functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of K19( the carrier of V)
l is Element of the carrier of V
B . l is Element of the carrier of R
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,v) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is set
the Element of { b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is Element of { b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R }
C is Element of the carrier of V
v . C is Element of the carrier of R
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
v is set
l is Element of the carrier of V
B . l is Element of the carrier of R
A . l is Element of the carrier of R
A . v is set
B . v is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
0. R is V54(R) Element of the carrier of R
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
A is Element of the carrier of V
(R,V) . A is Element of the carrier of R
(R,V,(R,V)) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not (R,V) . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
the carrier of R is non empty set
A is Element of K19( the carrier of V)
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
B is Element of K19( the carrier of V)
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,v) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
A is Element of K19( the carrier of V)
(R,V,(R,V)) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not (R,V) . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
{} the carrier of V is Function-like functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V, {} the carrier of V)
(R,V,A) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
A is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len A is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom v is finite set
rng v is finite set
l is set
D is set
v . D is set
Seg (len A) is finite len A -element Element of K19(NAT)
C is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
v . C is set
A /. C is Element of the carrier of V
B . (A /. C) is Element of the carrier of R
(A /. C) * (B . (A /. C)) is Element of the carrier of V
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom l is finite set
D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
l . D is set
A /. D is Element of the carrier of V
B . (A /. D) is Element of the carrier of R
(A /. D) * (B . (A /. D)) is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len v is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom v is finite set
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom l is finite set
D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
Seg (len v) is finite len v -element Element of K19(NAT)
v . D is set
A /. D is Element of the carrier of V
B . (A /. D) is Element of the carrier of R
(A /. D) * (B . (A /. D)) is Element of the carrier of V
l . D is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
A is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
B is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
dom v is finite set
v . A is set
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
(R,V,v,l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(R,V,v,l) . A is set
l . B is Element of the carrier of R
B * (l . B) is Element of the carrier of V
v /. A is Element of the carrier of V
len (R,V,v,l) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len v is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom (R,V,v,l) is finite set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
<*> the carrier of V is Relation-like NAT -defined the carrier of V -valued Function-like one-to-one constant functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite finite-yielding V38() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V45() FinSequence of the carrier of V
K20(NAT, the carrier of V) is non empty V12() non finite set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
(R,V,(<*> the carrier of V),A) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (R,V,(<*> the carrier of V),A) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len (<*> the carrier of V) is Function-like functional empty ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of NAT
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
A is Element of the carrier of V
<*A*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
(R,V,<*A*>,B) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
B . A is Element of the carrier of R
A * (B . A) is Element of the carrier of V
<*(A * (B . A))*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
{1} is non empty V12() finite V38() 1 -element Element of K19(NAT)
len (R,V,<*A*>,B) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len <*A*> is non empty ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom (R,V,<*A*>,B) is finite set
(R,V,<*A*>,B) . 1 is set
<*A*> /. 1 is Element of the carrier of V
B . (<*A*> /. 1) is Element of the carrier of R
(<*A*> /. 1) * (B . (<*A*> /. 1)) is Element of the carrier of V
A * (B . (<*A*> /. 1)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
A is Element of the carrier of V
B is Element of the carrier of V
<*A,B*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
(R,V,<*A,B*>,v) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
v . A is Element of the carrier of R
A * (v . A) is Element of the carrier of V
v . B is Element of the carrier of R
B * (v . B) is Element of the carrier of V
<*(A * (v . A)),(B * (v . B))*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (R,V,<*A,B*>,v) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len <*A,B*> is non empty ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom (R,V,<*A,B*>,v) is finite set
{1,2} is non empty finite V38() Element of K19(NAT)
(R,V,<*A,B*>,v) . 2 is set
<*A,B*> /. 2 is Element of the carrier of V
v . (<*A,B*> /. 2) is Element of the carrier of R
(<*A,B*> /. 2) * (v . (<*A,B*> /. 2)) is Element of the carrier of V
B * (v . (<*A,B*> /. 2)) is Element of the carrier of V
(R,V,<*A,B*>,v) . 1 is set
<*A,B*> /. 1 is Element of the carrier of V
v . (<*A,B*> /. 1) is Element of the carrier of R
(<*A,B*> /. 1) * (v . (<*A,B*> /. 1)) is Element of the carrier of V
A * (v . (<*A,B*> /. 1)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
A is Element of the carrier of V
B is Element of the carrier of V
v is Element of the carrier of V
<*A,B,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
(R,V,<*A,B,v*>,l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
l . A is Element of the carrier of R
A * (l . A) is Element of the carrier of V
l . B is Element of the carrier of R
B * (l . B) is Element of the carrier of V
l . v is Element of the carrier of R
v * (l . v) is Element of the carrier of V
<*(A * (l . A)),(B * (l . B)),(v * (l . v))*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 3 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (R,V,<*A,B,v*>,l) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len <*A,B,v*> is non empty ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom (R,V,<*A,B,v*>,l) is finite set
{1,2,3} is non empty finite Element of K19(NAT)
(R,V,<*A,B,v*>,l) . 3 is set
<*A,B,v*> /. 3 is Element of the carrier of V
l . (<*A,B,v*> /. 3) is Element of the carrier of R
(<*A,B,v*> /. 3) * (l . (<*A,B,v*> /. 3)) is Element of the carrier of V
v * (l . (<*A,B,v*> /. 3)) is Element of the carrier of V
(R,V,<*A,B,v*>,l) . 2 is set
<*A,B,v*> /. 2 is Element of the carrier of V
l . (<*A,B,v*> /. 2) is Element of the carrier of R
(<*A,B,v*> /. 2) * (l . (<*A,B,v*> /. 2)) is Element of the carrier of V
B * (l . (<*A,B,v*> /. 2)) is Element of the carrier of V
(R,V,<*A,B,v*>,l) . 1 is set
<*A,B,v*> /. 1 is Element of the carrier of V
l . (<*A,B,v*> /. 1) is Element of the carrier of R
(<*A,B,v*> /. 1) * (l . (<*A,B,v*> /. 1)) is Element of the carrier of V
A * (l . (<*A,B,v*> /. 1)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
A is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
A ^ B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
(R,V,(A ^ B),v) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(R,V,A,v) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(R,V,B,v) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(R,V,A,v) ^ (R,V,B,v) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len A is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len (R,V,A,v) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len ((R,V,A,v) ^ (R,V,B,v)) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len (R,V,B,v) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(len (R,V,A,v)) + (len (R,V,B,v)) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(len A) + (len (R,V,B,v)) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len B is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(len A) + (len B) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len (A ^ B) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
C is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
dom ((R,V,A,v) ^ (R,V,B,v)) is finite set
dom (R,V,A,v) is finite set
dom A is finite set
dom (A ^ B) is finite set
A /. C is Element of the carrier of V
A . C is set
(A ^ B) . C is set
(A ^ B) /. C is Element of the carrier of V
((R,V,A,v) ^ (R,V,B,v)) . C is set
(R,V,A,v) . C is set
v . ((A ^ B) /. C) is Element of the carrier of R
((A ^ B) /. C) * (v . ((A ^ B) /. C)) is Element of the carrier of V
dom (R,V,B,v) is finite set
dom (A ^ B) is finite set
f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
(len (R,V,A,v)) + f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
(len (R,V,A,v)) + f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom B is finite set
B /. f is Element of the carrier of V
B . f is set
(A ^ B) . C is set
(A ^ B) /. C is Element of the carrier of V
((R,V,A,v) ^ (R,V,B,v)) . C is set
(R,V,B,v) . f is set
v . ((A ^ B) /. C) is Element of the carrier of R
((A ^ B) /. C) * (v . ((A ^ B) /. C)) is Element of the carrier of V
dom (R,V,A,v) is finite set
dom (R,V,B,v) is finite set
((R,V,A,v) ^ (R,V,B,v)) . C is set
(A ^ B) /. C is Element of the carrier of V
v . ((A ^ B) /. C) is Element of the carrier of R
((A ^ B) /. C) * (v . ((A ^ B) /. C)) is Element of the carrier of V
((R,V,A,v) ^ (R,V,B,v)) . C is set
(A ^ B) /. C is Element of the carrier of V
v . ((A ^ B) /. C) is Element of the carrier of R
((A ^ B) /. C) * (v . ((A ^ B) /. C)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
B is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng B is finite set
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(R,V,v,A) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,v,A) is Element of the carrier of V
rng v is finite set
B is Element of the carrier of V
v is Element of the carrier of V
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng l is finite set
(R,V,l,A) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,l,A) is Element of the carrier of V
D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng D is finite set
(R,V,D,A) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,D,A) is Element of the carrier of V
len l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom l is finite set
Seg (len l) is finite len l -element Element of K19(NAT)
dom D is finite set
Seg (len D) is finite len D -element Element of K19(NAT)
C is set
D . C is set
{(D . C)} is non empty V12() finite 1 -element set
l " {(D . C)} is finite set
f is set
{f} is non empty V12() finite 1 -element set
K20((dom l),(dom l)) is finite set
K19(K20((dom l),(dom l))) is non empty finite V38() set
C is Relation-like dom l -defined dom l -valued Function-like quasi_total finite Element of K19(K20((dom l),(dom l)))
rng C is finite set
f is set
l . f is set
C is set
D . C is set
{(D . C)} is non empty V12() finite 1 -element set
l " {(D . C)} is finite set
Im (l,f) is set
{f} is non empty V12() finite 1 -element set
l .: {f} is finite set
l " (Im (l,f)) is finite set
C . C is set
{(C . C)} is non empty V12() finite 1 -element set
dom C is finite set
len (R,V,l,A) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
C is set
dom C is finite set
f is set
C . C is set
C . f is set
D . f is set
{(D . f)} is non empty V12() finite 1 -element set
l " {(D . f)} is finite set
{(C . f)} is non empty V12() finite 1 -element set
D . C is set
{(D . C)} is non empty V12() finite 1 -element set
l " {(D . C)} is finite set
{(C . C)} is non empty V12() finite 1 -element set
dom (R,V,D,A) is finite set
len (R,V,D,A) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
Seg (len (R,V,D,A)) is finite len (R,V,D,A) -element Element of K19(NAT)
dom (R,V,l,A) is finite set
Seg (len (R,V,l,A)) is finite len (R,V,l,A) -element Element of K19(NAT)
K20((dom (R,V,l,A)),(dom (R,V,l,A))) is finite set
K19(K20((dom (R,V,l,A)),(dom (R,V,l,A)))) is non empty finite V38() set
f is Relation-like dom l -defined dom l -valued Function-like quasi_total bijective finite Element of K19(K20((dom l),(dom l)))
f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(R,V,D,A) . f is set
D /. f is Element of the carrier of V
A . (D /. f) is Element of the carrier of R
(D /. f) * (A . (D /. f)) is Element of the carrier of V
D . f is set
f is Relation-like dom (R,V,l,A) -defined dom (R,V,l,A) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (R,V,l,A)),(dom (R,V,l,A))))
dom f is finite set
f . f is set
D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
l . D is set
l . (f . f) is set
{(l . (f . f))} is non empty V12() finite 1 -element set
Im (l,(f . f)) is set
{(f . f)} is non empty V12() finite 1 -element set
l .: {(f . f)} is finite set
{(D . f)} is non empty V12() finite 1 -element set
l " {(D . f)} is finite set
l .: (l " {(D . f)}) is finite set
g is Element of the carrier of V
g is Element of the carrier of V
l /. D is Element of the carrier of V
(R,V,l,A) . (f . f) is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
the carrier of V is non empty set
the carrier of R is non empty set
(R,V,(R,V)) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
(R,V,(R,V)) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not (R,V) . b₁ = 0. R } is set
A is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng A is finite set
(R,V,A,(R,V)) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,A,(R,V)) is Element of the carrier of V
len A is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len (R,V,A,(R,V)) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
0. R is V54(R) Element of the carrier of R
the carrier of R is non empty set
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,B) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
card (R,V,B) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,B) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
card (R,V,B) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(R,V,B) is Element of the carrier of V
B is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,v) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is set
(R,V,v) is Element of the carrier of V
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng l is finite set
(R,V,l,v) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,l,v) is Element of the carrier of V
Seg B is finite B -element Element of K19(NAT)
l | (Seg B) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT, the carrier of V))
K20(NAT, the carrier of V) is non empty V12() non finite set
K19(K20(NAT, the carrier of V)) is non empty V12() non finite set
card (R,V,v) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
B + 1 is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len (R,V,l,v) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
Seg (B + 1) is finite B + 1 -element Element of K19(NAT)
dom l is finite set
l . (B + 1) is set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
C is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
f . C is Element of the carrier of R
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
f is Element of the carrier of V
C is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
C . f is Element of the carrier of R
v . f is Element of the carrier of R
{C} is non empty V12() finite 1 -element Element of K19( the carrier of V)
A \ {C} is Element of K19( the carrier of V)
v . C is Element of the carrier of R
C * (v . C) is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,f) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not f . b₁ = 0. R } is set
(R,V,v) \ {C} is finite Element of K19( the carrier of V)
f is set
f is Element of the carrier of V
f . f is Element of the carrier of R
v . f is Element of the carrier of R
f is set
f is Element of the carrier of V
v . f is Element of the carrier of R
f . f is Element of the carrier of R
D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,D,f) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (R,V,D,f) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
rng D is finite set
(R,V,f) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not f . b₁ = 0. R } is set
f is set
dom D is finite set
g is set
D . g is set
D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
D . D is set
l . D is set
f is set
g is set
l . g is set
D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(dom l) \ (Seg B) is finite Element of K19((dom l))
K19((dom l)) is non empty finite V38() set
(Seg (B + 1)) \ (Seg B) is finite Element of K19(NAT)
{(B + 1)} is non empty V12() finite V38() 1 -element Element of K19(NAT)
(dom l) /\ (Seg B) is finite Element of K19(NAT)
dom D is finite set
D . D is set
l . D is set
(Seg (B + 1)) /\ (Seg B) is finite Element of K19(NAT)
dom (R,V,D,f) is finite set
dom (R,V,l,v) is finite set
(dom (R,V,l,v)) /\ (Seg B) is finite Element of K19(NAT)
f is set
g is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
l . g is set
dom D is finite set
D . g is set
g is Element of the carrier of V
(R,V,D,f) . g is set
f . g is Element of the carrier of R
g * (f . g) is Element of the carrier of V
v . g is Element of the carrier of R
g * (v . g) is Element of the carrier of V
D is Element of the carrier of V
(R,V,D,f) . f is set
(R,V,l,v) . f is set
(R,V,l,v) | (Seg B) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT, the carrier of V))
(R,V,l,v) | (dom (R,V,D,f)) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSubsequence-like Element of K19(K20(NAT, the carrier of V))
card (R,V,f) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
card {C} is non empty ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(B + 1) - (card {C}) is ext-real V33() V45() set
(B + 1) - 1 is ext-real V33() V45() set
(R,V,f) is Element of the carrier of V
Sum (R,V,D,f) is Element of the carrier of V
(R,V,l,v) . (len l) is set
(Sum (R,V,D,f)) + (C * (v . C)) is Element of the carrier of V
B is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,v) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is set
card (R,V,v) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
B + 1 is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(R,V,v) is Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,B) is Element of the carrier of V
(R,V,B) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
card (R,V,B) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V)) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
B is Element of the carrier of R
v is Element of the carrier of V
v * B is Element of the carrier of V
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
l . v is Element of the carrier of R
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
C is Element of the carrier of V
{v} is non empty V12() finite 1 -element Element of K19( the carrier of V)
D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
D . C is Element of the carrier of R
C is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,C) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not C . b₁ = 0. R } is set
f is set
C is Element of the carrier of V
C . C is Element of the carrier of R
f is set
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,f) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not f . b₁ = 0. R } is set
(R,V,f) is Element of the carrier of V
C is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng C is finite set
(R,V,C,f) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,C,f) is Element of the carrier of V
<*v*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
f . v is Element of the carrier of R
v * (f . v) is Element of the carrier of V
<*(v * (f . v))*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
B is Element of the carrier of V
v is Element of the carrier of V
B + v is Element of the carrier of V
B * (1_ R) is Element of the carrier of V
(B * (1_ R)) + B is Element of the carrier of V
(B * (1_ R)) + (B * (1_ R)) is Element of the carrier of V
(1_ R) + (1_ R) is Element of the carrier of R
B * ((1_ R) + (1_ R)) is Element of the carrier of V
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
l . B is Element of the carrier of R
l . v is Element of the carrier of R
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
C is Element of the carrier of V
{B,v} is non empty finite Element of K19( the carrier of V)
D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
D . C is Element of the carrier of R
C is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,C) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not C . b₁ = 0. R } is set
f is set
C is Element of the carrier of V
C . C is Element of the carrier of R
f is set
v * (1_ R) is Element of the carrier of V
B * (1_ R) is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,f) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not f . b₁ = 0. R } is set
(R,V,f) is Element of the carrier of V
C is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng C is finite set
(R,V,C,f) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,C,f) is Element of the carrier of V
<*B,v*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*v,B*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*(B * (1_ R)),(v * (1_ R))*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*(v * (1_ R)),(B * (1_ R))*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
v is Element of the carrier of V
B is Element of the carrier of R
v * B is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
the carrier of V is non empty set
the carrier of R is non empty set
(R,V,(R,V)) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
{} the carrier of V is Function-like functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. V is V54(V) Element of the carrier of V
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V, {} the carrier of V)
(R,V,A) is Element of the carrier of V
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
{A} is non empty V12() finite 1 -element Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,{A})
(R,V,B) is Element of the carrier of V
B . A is Element of the carrier of R
A * (B . A) is Element of the carrier of V
(R,V,B) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
0. V is V54(V) Element of the carrier of V
A * (0. R) is Element of the carrier of V
v is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v is finite set
(R,V,v,B) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,v,B) is Element of the carrier of V
<*A*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*(A * (B . A))*> is Relation-like NAT -defined the carrier of V -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,{A,B})
(R,V,v) is Element of the carrier of V
v . A is Element of the carrier of R
A * (v . A) is Element of the carrier of V
v . B is Element of the carrier of R
B * (v . B) is Element of the carrier of V
(A * (v . A)) + (B * (v . B)) is Element of the carrier of V
(R,V,v) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
0. V is V54(V) Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
A * (0. R) is Element of the carrier of V
(A * (0. R)) + (0. V) is Element of the carrier of V
B * (0. R) is Element of the carrier of V
(A * (0. R)) + (B * (0. R)) is Element of the carrier of V
(A * (v . A)) + (B * (0. R)) is Element of the carrier of V
{A} is non empty V12() finite 1 -element Element of K19( the carrier of V)
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,{A})
(R,V,l) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
(A * (v . A)) + (0. V) is Element of the carrier of V
B * (0. R) is Element of the carrier of V
(A * (v . A)) + (B * (0. R)) is Element of the carrier of V
{B} is non empty V12() finite 1 -element Element of K19( the carrier of V)
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,{B})
(R,V,l) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
(0. V) + (B * (v . B)) is Element of the carrier of V
A * (0. R) is Element of the carrier of V
(A * (0. R)) + (B * (v . B)) is Element of the carrier of V
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng l is finite set
(R,V,l,v) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,l,v) is Element of the carrier of V
<*A,B*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*B,A*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*(A * (v . A)),(B * (v . B))*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*(B * (v . B)),(A * (v . A))*> is Relation-like NAT -defined the carrier of V -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
{A} is non empty V12() finite 1 -element Element of K19( the carrier of V)
{B} is non empty V12() finite 1 -element Element of K19( the carrier of V)
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
0. V is V54(V) Element of the carrier of V
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
(R,V,A) is Element of the carrier of V
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
{A} is non empty V12() finite 1 -element Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
(R,V,B) is Element of the carrier of V
B . A is Element of the carrier of R
A * (B . A) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,v) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is set
(R,V,v) is Element of the carrier of V
v . A is Element of the carrier of R
A * (v . A) is Element of the carrier of V
v . B is Element of the carrier of R
B * (v . B) is Element of the carrier of V
(A * (v . A)) + (B * (v . B)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
v is Element of the carrier of V
A . v is Element of the carrier of R
B . v is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
D is Element of the carrier of V
(R,V,A) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
(R,V,B) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
(R,V,A) \/ (R,V,B) is finite Element of K19( the carrier of V)
B . D is Element of the carrier of R
A . D is Element of the carrier of R
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
l . D is Element of the carrier of R
(0. R) + (0. R) is Element of the carrier of R
D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
C is Element of the carrier of V
D . C is Element of the carrier of R
A . C is Element of the carrier of R
B . C is Element of the carrier of R
(A . C) + (B . C) is Element of the carrier of R
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
D is Element of the carrier of V
v . D is Element of the carrier of R
l . D is Element of the carrier of R
A . D is Element of the carrier of R
B . D is Element of the carrier of R
(A . D) + (B . D) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A,B)) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (R,V,A,B) . b₁ = 0. R } is set
(R,V,B) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
(R,V,A) \/ (R,V,B) is finite Element of K19( the carrier of V)
v is set
l is Element of the carrier of V
(R,V,A,B) . l is Element of the carrier of R
A . l is Element of the carrier of R
B . l is Element of the carrier of R
(A . l) + (B . l) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
(R,V,v) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is set
(R,V,B) \/ (R,V,v) is finite Element of K19( the carrier of V)
(R,V,(R,V,B,v)) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (R,V,B,v) . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
v is Element of the carrier of V
(R,V,A,B) . v is Element of the carrier of R
(R,V,B,A) . v is Element of the carrier of R
B . v is Element of the carrier of R
A . v is Element of the carrier of R
(B . v) + (A . v) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,(R,V,B,v)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A,B),v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
l is Element of the carrier of V
(R,V,A,(R,V,B,v)) . l is Element of the carrier of R
(R,V,(R,V,A,B),v) . l is Element of the carrier of R
A . l is Element of the carrier of R
(R,V,B,v) . l is Element of the carrier of R
(A . l) + ((R,V,B,v) . l) is Element of the carrier of R
B . l is Element of the carrier of R
v . l is Element of the carrier of R
(B . l) + (v . l) is Element of the carrier of R
(A . l) + ((B . l) + (v . l)) is Element of the carrier of R
(A . l) + (B . l) is Element of the carrier of R
((A . l) + (B . l)) + (v . l) is Element of the carrier of R
(R,V,A,B) . l is Element of the carrier of R
((R,V,A,B) . l) + (v . l) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,(R,V)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V),A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Element of the carrier of V
(R,V,A,(R,V)) . B is Element of the carrier of R
A . B is Element of the carrier of R
(R,V) . B is Element of the carrier of R
(A . B) + ((R,V) . B) is Element of the carrier of R
0. R is V54(R) Element of the carrier of R
(A . B) + (0. R) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
A is Element of the carrier of R
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
D is Element of the carrier of V
(R,V,B) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
B . D is Element of the carrier of R
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
l . D is Element of the carrier of R
(0. R) * A is Element of the carrier of R
D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
C is Element of the carrier of V
D . C is Element of the carrier of R
B . C is Element of the carrier of R
(B . C) * A is Element of the carrier of R
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
D is Element of the carrier of V
v . D is Element of the carrier of R
l . D is Element of the carrier of R
B . D is Element of the carrier of R
(B . D) * A is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of R
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A,B)) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not (R,V,A,B) . b₁ = 0. R } is set
(R,V,B) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
D is set
C is Element of the carrier of V
(R,V,A,B) . C is Element of the carrier of R
B . C is Element of the carrier of R
(B . C) * A is Element of the carrier of R
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
the carrier of R is non empty V12() set
0. R is V54(R) Element of the carrier of R
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
B is Element of the carrier of R
(R,V,B,A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,B,A)) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (R,V,B,A) . b₁ = 0. R } is set
D is set
C is Element of the carrier of V
(R,V,B,A) . C is Element of the carrier of R
A . C is Element of the carrier of R
(A . C) * B is Element of the carrier of R
D is set
C is Element of the carrier of V
A . C is Element of the carrier of R
(R,V,B,A) . C is Element of the carrier of R
(A . C) * B is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
0. R is V54(R) Element of the carrier of R
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(0. R),A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Element of the carrier of V
(R,V,(0. R),A) . B is Element of the carrier of R
(R,V) . B is Element of the carrier of R
A . B is Element of the carrier of R
(A . B) * (0. R) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of the carrier of R
B is Element of K19( the carrier of V)
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,v) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is set
(R,V,(R,V,A,v)) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (R,V,A,v) . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of R
B is Element of the carrier of R
A + B is Element of the carrier of R
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(A + B),v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A,v),(R,V,B,v)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
l is Element of the carrier of V
(R,V,(A + B),v) . l is Element of the carrier of R
(R,V,(R,V,A,v),(R,V,B,v)) . l is Element of the carrier of R
v . l is Element of the carrier of R
(v . l) * (A + B) is Element of the carrier of R
(v . l) * A is Element of the carrier of R
(v . l) * B is Element of the carrier of R
((v . l) * A) + ((v . l) * B) is Element of the carrier of R
(R,V,A,v) . l is Element of the carrier of R
((R,V,A,v) . l) + ((v . l) * B) is Element of the carrier of R
(R,V,B,v) . l is Element of the carrier of R
((R,V,A,v) . l) + ((R,V,B,v) . l) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of R
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,(R,V,B,v)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A,B),(R,V,A,v)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
l is Element of the carrier of V
(R,V,A,(R,V,B,v)) . l is Element of the carrier of R
(R,V,(R,V,A,B),(R,V,A,v)) . l is Element of the carrier of R
(R,V,B,v) . l is Element of the carrier of R
((R,V,B,v) . l) * A is Element of the carrier of R
B . l is Element of the carrier of R
v . l is Element of the carrier of R
(B . l) + (v . l) is Element of the carrier of R
((B . l) + (v . l)) * A is Element of the carrier of R
(B . l) * A is Element of the carrier of R
(v . l) * A is Element of the carrier of R
((B . l) * A) + ((v . l) * A) is Element of the carrier of R
(R,V,A,B) . l is Element of the carrier of R
((R,V,A,B) . l) + ((v . l) * A) is Element of the carrier of R
(R,V,A,v) . l is Element of the carrier of R
((R,V,A,B) . l) + ((R,V,A,v) . l) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of R
B is Element of the carrier of R
A * B is Element of the carrier of R
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,(R,V,A,v)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(A * B),v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
l is Element of the carrier of V
(R,V,B,(R,V,A,v)) . l is Element of the carrier of R
(R,V,(A * B),v) . l is Element of the carrier of R
(R,V,A,v) . l is Element of the carrier of R
((R,V,A,v) . l) * B is Element of the carrier of R
v . l is Element of the carrier of R
(v . l) * A is Element of the carrier of R
((v . l) * A) * B is Element of the carrier of R
(v . l) * (A * B) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(1_ R),A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Element of the carrier of V
(R,V,(1_ R),A) . B is Element of the carrier of R
A . B is Element of the carrier of R
(A . B) * (1_ R) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(- (1_ R)),A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(- (1_ R)),v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(- (1_ R)),B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
l is Element of the carrier of V
v . l is Element of the carrier of R
(R,V,(- (1_ R)),B) . l is Element of the carrier of R
(v . l) * (1_ R) is Element of the carrier of R
(1_ R) * (1_ R) is Element of the carrier of R
(v . l) * ((1_ R) * (1_ R)) is Element of the carrier of R
(- (1_ R)) * (- (1_ R)) is Element of the carrier of R
(v . l) * ((- (1_ R)) * (- (1_ R))) is Element of the carrier of R
(R,V,((- (1_ R)) * (- (1_ R))),v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,((- (1_ R)) * (- (1_ R))),v) . l is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) . A is Element of the carrier of R
B . A is Element of the carrier of R
- (B . A) is Element of the carrier of R
(B . A) * (- (1_ R)) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
v is Element of the carrier of V
B . v is Element of the carrier of R
(R,V,A) . v is Element of the carrier of R
A . v is Element of the carrier of R
(A . v) + (B . v) is Element of the carrier of R
(R,V) . v is Element of the carrier of R
0. R is V54(R) Element of the carrier of R
- (A . v) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A)) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not (R,V,A) . b₁ = 0. R } is set
(R,V,A) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
(R,V,(R,V,(- (1_ R)),A)) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (R,V,(- (1_ R)),A) . b₁ = 0. R } is set
D is set
C is Element of the carrier of V
(R,V,(- (1_ R)),A) . C is Element of the carrier of R
A . C is Element of the carrier of R
(A . C) * (- (1_ R)) is Element of the carrier of R
D is set
C is Element of the carrier of V
A . C is Element of the carrier of R
(R,V,(- (1_ R)),A) . C is Element of the carrier of R
(A . C) * (- (1_ R)) is Element of the carrier of R
- (A . C) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
the carrier of R is non empty set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
A is Element of K19( the carrier of V)
(R,V,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
the carrier of R is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,(R,V,B)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B . A is Element of the carrier of R
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,(R,V,v)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,v) . A is Element of the carrier of R
v . A is Element of the carrier of R
(B . A) - (v . A) is Element of the carrier of R
(R,V,v) . A is Element of the carrier of R
(B . A) + ((R,V,v) . A) is Element of the carrier of R
- (v . A) is Element of the carrier of R
(B . A) + (- (v . A)) is Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,(R,V,B)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A,B)) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (R,V,A,B) . b₁ = 0. R } is set
(R,V,B) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
(R,V,A) \/ (R,V,B) is finite Element of K19( the carrier of V)
(R,V,(R,V,B)) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not (R,V,B) . b₁ = 0. R } is set
(R,V,A) \/ (R,V,(R,V,B)) is finite Element of K19( the carrier of V)
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),v) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B,(R,V,v)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,(R,V,A)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
B is Element of the carrier of V
(R,V,A,A) . B is Element of the carrier of R
(R,V) . B is Element of the carrier of R
A . B is Element of the carrier of R
(A . B) - (A . B) is Element of the carrier of R
0. R is V54(R) Element of the carrier of R
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
the carrier of R is non empty set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A,B)) is Element of the carrier of V
(R,V,B) is Element of the carrier of V
(R,V,A) + (R,V,B) is Element of the carrier of V
(R,V,(R,V,A,B)) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not (R,V,A,B) . b₁ = 0. R } is set
(R,V,A) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
(R,V,(R,V,A,B)) \/ (R,V,A) is finite Element of K19( the carrier of V)
(R,V,B) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. R } is set
((R,V,(R,V,A,B)) \/ (R,V,A)) \/ (R,V,B) is finite Element of K19( the carrier of V)
(((R,V,(R,V,A,B)) \/ (R,V,A)) \/ (R,V,B)) \ (R,V,A) is finite Element of K19( the carrier of V)
D is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng D is finite set
(R,V,(R,V,A,B)) \/ (R,V,B) is finite Element of K19( the carrier of V)
(R,V,A) \/ ((R,V,(R,V,A,B)) \/ (R,V,B)) is finite Element of K19( the carrier of V)
(((R,V,(R,V,A,B)) \/ (R,V,A)) \/ (R,V,B)) \ (R,V,(R,V,A,B)) is finite Element of K19( the carrier of V)
C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng C is finite set
(R,V,A) \/ (R,V,B) is finite Element of K19( the carrier of V)
(R,V,(R,V,A,B)) \/ ((R,V,A) \/ (R,V,B)) is finite Element of K19( the carrier of V)
(((R,V,(R,V,A,B)) \/ (R,V,A)) \/ (R,V,B)) \ (R,V,B) is finite Element of K19( the carrier of V)
f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng f is finite set
D is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng D is finite set
(R,V,D,(R,V,A,B)) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,D,(R,V,A,B)) is Element of the carrier of V
f is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
D ^ f is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
g is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng g is finite set
(R,V,g,A) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,g,A) is Element of the carrier of V
rng (D ^ f) is finite set
rng f is finite set
(rng D) \/ (rng f) is finite set
(R,V,(R,V,A,B)) \/ (((R,V,(R,V,A,B)) \/ (R,V,A)) \/ (R,V,B)) is finite Element of K19( the carrier of V)
C is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
g ^ C is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng (g ^ C) is finite set
rng C is finite set
(rng g) \/ (rng C) is finite set
(R,V,A) \/ (((R,V,(R,V,A,B)) \/ (R,V,A)) \/ (R,V,B)) is finite Element of K19( the carrier of V)
(rng D) /\ (rng f) is finite set
the Element of (rng D) /\ (rng f) is Element of (rng D) /\ (rng f)
(rng g) /\ (rng C) is finite set
the Element of (rng g) /\ (rng C) is Element of (rng g) /\ (rng C)
len (g ^ C) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len (D ^ f) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
v is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len v is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom v is finite set
Seg (len (D ^ f)) is finite len (D ^ f) -element Element of K19(NAT)
f is set
dom (g ^ C) is finite set
H is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
(g ^ C) . H is set
v . H is set
(D ^ f) . (v . H) is set
(D ^ f) <- ((g ^ C) . H) is set
(D ^ f) . ((D ^ f) <- ((g ^ C) . H)) is set
(g ^ C) . f is set
v . f is set
(D ^ f) . (v . f) is set
dom (D ^ f) is finite set
rng v is finite set
f is set
H is set
v . H is set
HH is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
(g ^ C) . HH is set
v . HH is set
(D ^ f) <- ((g ^ C) . HH) is set
f is set
v . f is set
Seg (len v) is finite len v -element Element of K19(NAT)
v (#) (D ^ f) is Relation-like Function-like finite set
(D ^ f) " is Relation-like Function-like set
(g ^ C) (#) ((D ^ f) ") is Relation-like Function-like finite set
H is set
dom ((D ^ f) ") is set
rng ((g ^ C) (#) ((D ^ f) ")) is finite set
rng ((D ^ f) ") is set
(D ^ f) (#) ((D ^ f) ") is Relation-like Function-like finite set
v (#) ((D ^ f) (#) ((D ^ f) ")) is Relation-like Function-like finite set
id (dom (D ^ f)) is Relation-like dom (D ^ f) -defined dom (D ^ f) -valued Function-like one-to-one total finite Element of K19(K20((dom (D ^ f)),(dom (D ^ f))))
K20((dom (D ^ f)),(dom (D ^ f))) is finite set
K19(K20((dom (D ^ f)),(dom (D ^ f)))) is non empty finite V38() set
v (#) (id (dom (D ^ f))) is Relation-like Function-like finite set
len f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(R,V,f,(R,V,A,B)) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (R,V,f,(R,V,A,B)) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
dom f is finite set
f /. f is Element of the carrier of V
f . f is set
dom (R,V,f,(R,V,A,B)) is finite set
(R,V,f,(R,V,A,B)) . f is set
(R,V,A,B) . (f /. f) is Element of the carrier of R
(f /. f) * ((R,V,A,B) . (f /. f)) is Element of the carrier of V
(f /. f) * (0. R) is Element of the carrier of V
Sum (R,V,f,(R,V,A,B)) is Element of the carrier of V
Sum f is Element of the carrier of V
(Sum f) * (0. R) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
len C is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(R,V,C,A) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (R,V,C,A) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
dom C is finite set
C /. f is Element of the carrier of V
C . f is set
dom (R,V,C,A) is finite set
(R,V,C,A) . f is set
A . (C /. f) is Element of the carrier of R
(C /. f) * (A . (C /. f)) is Element of the carrier of V
(C /. f) * (0. R) is Element of the carrier of V
Sum (R,V,C,A) is Element of the carrier of V
Sum C is Element of the carrier of V
(Sum C) * (0. R) is Element of the carrier of V
(R,V,(D ^ f),(R,V,A,B)) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
H is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng H is finite set
(R,V,H,B) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,H,B) is Element of the carrier of V
g is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
H ^ g is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng g is finite set
(rng H) /\ (rng g) is finite set
the Element of (rng H) /\ (rng g) is Element of (rng H) /\ (rng g)
len g is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
(R,V,g,B) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (R,V,g,B) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
g is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
dom g is finite set
g /. g is Element of the carrier of V
g . g is set
dom (R,V,g,B) is finite set
(R,V,g,B) . g is set
B . (g /. g) is Element of the carrier of R
(g /. g) * (B . (g /. g)) is Element of the carrier of V
(g /. g) * (0. R) is Element of the carrier of V
Sum (R,V,g,B) is Element of the carrier of V
Sum g is Element of the carrier of V
(Sum g) * (0. R) is Element of the carrier of V
(R,V,(g ^ C),A) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len (R,V,(g ^ C),A) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
Seg (len (g ^ C)) is finite len (g ^ C) -element Element of K19(NAT)
dom (R,V,(g ^ C),A) is finite set
rng (H ^ g) is finite set
(rng H) \/ (rng g) is finite set
(R,V,B) \/ (((R,V,(R,V,A,B)) \/ (R,V,A)) \/ (R,V,B)) is finite Element of K19( the carrier of V)
len (H ^ g) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len R is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom R is finite set
Seg (len (H ^ g)) is finite len (H ^ g) -element Element of K19(NAT)
h is set
R is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
(g ^ C) . R is set
R . R is set
(H ^ g) . (R . R) is set
(H ^ g) <- ((g ^ C) . R) is set
(H ^ g) . ((H ^ g) <- ((g ^ C) . R)) is set
(g ^ C) . h is set
R . h is set
(H ^ g) . (R . h) is set
dom (H ^ g) is finite set
rng R is finite set
h is set
R is set
R . R is set
R is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
(g ^ C) . R is set
R . R is set
(H ^ g) <- ((g ^ C) . R) is set
h is set
R . h is set
Seg (len R) is finite len R -element Element of K19(NAT)
Seg (len R) is finite len R -element Element of K19(NAT)
R (#) (H ^ g) is Relation-like Function-like finite set
(H ^ g) " is Relation-like Function-like set
(g ^ C) (#) ((H ^ g) ") is Relation-like Function-like finite set
R is set
dom ((H ^ g) ") is set
rng ((g ^ C) (#) ((H ^ g) ")) is finite set
rng ((H ^ g) ") is set
(H ^ g) (#) ((H ^ g) ") is Relation-like Function-like finite set
R (#) ((H ^ g) (#) ((H ^ g) ")) is Relation-like Function-like finite set
id (dom (H ^ g)) is Relation-like dom (H ^ g) -defined dom (H ^ g) -valued Function-like one-to-one total finite Element of K19(K20((dom (H ^ g)),(dom (H ^ g))))
K20((dom (H ^ g)),(dom (H ^ g))) is finite set
K19(K20((dom (H ^ g)),(dom (H ^ g)))) is non empty finite V38() set
R (#) (id (dom (H ^ g))) is Relation-like Function-like finite set
Sum (R,V,(g ^ C),A) is Element of the carrier of V
(R,V,g,A) ^ (R,V,C,A) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((R,V,g,A) ^ (R,V,C,A)) is Element of the carrier of V
(Sum (R,V,g,A)) + (0. V) is Element of the carrier of V
(R,V,(H ^ g),B) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,(H ^ g),B) is Element of the carrier of V
(R,V,H,B) ^ (R,V,g,B) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((R,V,H,B) ^ (R,V,g,B)) is Element of the carrier of V
(Sum (R,V,H,B)) + (0. V) is Element of the carrier of V
Sum (R,V,(D ^ f),(R,V,A,B)) is Element of the carrier of V
(R,V,D,(R,V,A,B)) ^ (R,V,f,(R,V,A,B)) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((R,V,D,(R,V,A,B)) ^ (R,V,f,(R,V,A,B))) is Element of the carrier of V
(Sum (R,V,D,(R,V,A,B))) + (0. V) is Element of the carrier of V
K20((dom (H ^ g)),(dom (H ^ g))) is finite set
K19(K20((dom (H ^ g)),(dom (H ^ g)))) is non empty finite V38() set
len (R,V,(H ^ g),B) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom (R,V,(H ^ g),B) is finite set
K20((dom (R,V,(H ^ g),B)),(dom (R,V,(H ^ g),B))) is finite set
K19(K20((dom (R,V,(H ^ g),B)),(dom (R,V,(H ^ g),B)))) is non empty finite V38() set
R is Relation-like dom (H ^ g) -defined dom (H ^ g) -valued Function-like quasi_total finite Element of K19(K20((dom (H ^ g)),(dom (H ^ g))))
R is Relation-like dom (R,V,(H ^ g),B) -defined dom (R,V,(H ^ g),B) -valued Function-like quasi_total finite Element of K19(K20((dom (R,V,(H ^ g),B)),(dom (R,V,(H ^ g),B))))
(R,V,(H ^ g),B) * R is Relation-like dom (R,V,(H ^ g),B) -defined the carrier of V -valued Function-like finite Element of K19(K20((dom (R,V,(H ^ g),B)), the carrier of V))
K20((dom (R,V,(H ^ g),B)), the carrier of V) is set
K19(K20((dom (R,V,(H ^ g),B)), the carrier of V)) is non empty set
Hp is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
R is Relation-like dom (R,V,(H ^ g),B) -defined dom (R,V,(H ^ g),B) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (R,V,(H ^ g),B)),(dom (R,V,(H ^ g),B))))
(R,V,(H ^ g),B) * R is Relation-like dom (R,V,(H ^ g),B) -defined the carrier of V -valued Function-like finite Element of K19(K20((dom (R,V,(H ^ g),B)), the carrier of V))
len Hp is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
K20((dom (D ^ f)),(dom (D ^ f))) is finite set
K19(K20((dom (D ^ f)),(dom (D ^ f)))) is non empty finite V38() set
len (R,V,(D ^ f),(R,V,A,B)) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom (R,V,(D ^ f),(R,V,A,B)) is finite set
K20((dom (R,V,(D ^ f),(R,V,A,B))),(dom (R,V,(D ^ f),(R,V,A,B)))) is finite set
K19(K20((dom (R,V,(D ^ f),(R,V,A,B))),(dom (R,V,(D ^ f),(R,V,A,B))))) is non empty finite V38() set
P is Relation-like dom (D ^ f) -defined dom (D ^ f) -valued Function-like quasi_total finite Element of K19(K20((dom (D ^ f)),(dom (D ^ f))))
P is Relation-like dom (R,V,(D ^ f),(R,V,A,B)) -defined dom (R,V,(D ^ f),(R,V,A,B)) -valued Function-like quasi_total finite Element of K19(K20((dom (R,V,(D ^ f),(R,V,A,B))),(dom (R,V,(D ^ f),(R,V,A,B)))))
(R,V,(D ^ f),(R,V,A,B)) * P is Relation-like dom (R,V,(D ^ f),(R,V,A,B)) -defined the carrier of V -valued Function-like finite Element of K19(K20((dom (R,V,(D ^ f),(R,V,A,B))), the carrier of V))
K20((dom (R,V,(D ^ f),(R,V,A,B))), the carrier of V) is set
K19(K20((dom (R,V,(D ^ f),(R,V,A,B))), the carrier of V)) is non empty set
Fp is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
P is Relation-like dom (R,V,(D ^ f),(R,V,A,B)) -defined dom (R,V,(D ^ f),(R,V,A,B)) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (R,V,(D ^ f),(R,V,A,B))),(dom (R,V,(D ^ f),(R,V,A,B)))))
(R,V,(D ^ f),(R,V,A,B)) * P is Relation-like dom (R,V,(D ^ f),(R,V,A,B)) -defined the carrier of V -valued Function-like finite Element of K19(K20((dom (R,V,(D ^ f),(R,V,A,B))), the carrier of V))
Sum Fp is Element of the carrier of V
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len I is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom I is finite set
I is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
I . I is set
(R,V,(g ^ C),A) /. I is Element of the carrier of V
Hp /. I is Element of the carrier of V
((R,V,(g ^ C),A) /. I) + (Hp /. I) is Element of the carrier of V
rng I is finite set
I is set
x is set
I . x is set
k is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
I . k is set
(R,V,(g ^ C),A) /. k is Element of the carrier of V
Hp /. k is Element of the carrier of V
((R,V,(g ^ C),A) /. k) + (Hp /. k) is Element of the carrier of V
len Fp is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
I is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len I is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
x is set
Seg (len I) is finite len I -element Element of K19(NAT)
k is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
R . k is set
dom R is finite set
j is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
(H ^ g) . j is set
(g ^ C) . k is set
(g ^ C) /. k is Element of the carrier of V
P . k is set
dom P is finite set
dom Fp is finite set
l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
(D ^ f) . l is set
(R,V,(D ^ f),(R,V,A,B)) . l is set
(R,V,A,B) . ((g ^ C) /. k) is Element of the carrier of R
((g ^ C) /. k) * ((R,V,A,B) . ((g ^ C) /. k)) is Element of the carrier of V
A . ((g ^ C) /. k) is Element of the carrier of R
B . ((g ^ C) /. k) is Element of the carrier of R
(A . ((g ^ C) /. k)) + (B . ((g ^ C) /. k)) is Element of the carrier of R
((g ^ C) /. k) * ((A . ((g ^ C) /. k)) + (B . ((g ^ C) /. k))) is Element of the carrier of V
((g ^ C) /. k) * (A . ((g ^ C) /. k)) is Element of the carrier of V
((g ^ C) /. k) * (B . ((g ^ C) /. k)) is Element of the carrier of V
(((g ^ C) /. k) * (A . ((g ^ C) /. k))) + (((g ^ C) /. k) * (B . ((g ^ C) /. k))) is Element of the carrier of V
dom Hp is finite set
Hp /. k is Element of the carrier of V
((R,V,(H ^ g),B) * R) . k is set
(R,V,(H ^ g),B) . (R . k) is set
(R,V,(H ^ g),B) . j is set
(R,V,(g ^ C),A) /. k is Element of the carrier of V
(R,V,(g ^ C),A) . k is set
I . x is set
Fp . x is set
dom I is finite set
Sum Hp is Element of the carrier of V
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
the carrier of R is non empty V12() set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is Element of the carrier of V
B is Element of the carrier of R
(R,V,B,A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,B,A)) is Element of the carrier of V
(R,V,A) * B is Element of the carrier of V
0. R is V54(R) Element of the carrier of R
(R,V,(R,V,B,A)) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b₁ where b₁ is Element of the carrier of V : not (R,V,B,A) . b₁ = 0. R } is set
(R,V,A) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
l is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng l is finite set
(R,V,l,A) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,l,A) is Element of the carrier of V
C is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng C is finite set
(R,V,C,(R,V,B,A)) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (R,V,C,(R,V,B,A)) is Element of the carrier of V
len l is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len C is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
C is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len C is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom C is finite set
Seg (len C) is finite len C -element Element of K19(NAT)
f is set
dom l is finite set
f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
l . f is set
C . f is set
C . (C . f) is set
C <- (l . f) is set
C . (C <- (l . f)) is set
l . f is set
C . f is set
C . (C . f) is set
rng C is finite set
dom C is finite set
f is set
f is set
C . f is set
f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
l . f is set
C . f is set
C <- (l . f) is set
f is set
C . f is set
Seg (len C) is finite len C -element Element of K19(NAT)
Seg (len C) is finite len C -element Element of K19(NAT)
C (#) C is Relation-like Function-like finite set
C " is Relation-like Function-like set
l (#) (C ") is Relation-like Function-like finite set
f is set
dom (C ") is set
rng (l (#) (C ")) is finite set
rng (C ") is set
C (#) (C ") is Relation-like Function-like finite set
C (#) (C (#) (C ")) is Relation-like Function-like finite set
id (dom C) is Relation-like dom C -defined dom C -valued Function-like one-to-one total finite Element of K19(K20((dom C),(dom C)))
K20((dom C),(dom C)) is finite set
K19(K20((dom C),(dom C))) is non empty finite V38() set
C (#) (id (dom C)) is Relation-like Function-like finite set
K20((dom C),(dom C)) is finite set
K19(K20((dom C),(dom C))) is non empty finite V38() set
len (R,V,C,(R,V,B,A)) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom (R,V,C,(R,V,B,A)) is finite set
K20((dom (R,V,C,(R,V,B,A))),(dom (R,V,C,(R,V,B,A)))) is finite set
K19(K20((dom (R,V,C,(R,V,B,A))),(dom (R,V,C,(R,V,B,A))))) is non empty finite V38() set
f is Relation-like dom C -defined dom C -valued Function-like quasi_total finite Element of K19(K20((dom C),(dom C)))
f is Relation-like dom (R,V,C,(R,V,B,A)) -defined dom (R,V,C,(R,V,B,A)) -valued Function-like quasi_total finite Element of K19(K20((dom (R,V,C,(R,V,B,A))),(dom (R,V,C,(R,V,B,A)))))
(R,V,C,(R,V,B,A)) * f is Relation-like dom (R,V,C,(R,V,B,A)) -defined the carrier of V -valued Function-like finite Element of K19(K20((dom (R,V,C,(R,V,B,A))), the carrier of V))
K20((dom (R,V,C,(R,V,B,A))), the carrier of V) is set
K19(K20((dom (R,V,C,(R,V,B,A))), the carrier of V)) is non empty set
f is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
g is Relation-like dom (R,V,C,(R,V,B,A)) -defined dom (R,V,C,(R,V,B,A)) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (R,V,C,(R,V,B,A))),(dom (R,V,C,(R,V,B,A)))))
(R,V,C,(R,V,B,A)) * g is Relation-like dom (R,V,C,(R,V,B,A)) -defined the carrier of V -valued Function-like finite Element of K19(K20((dom (R,V,C,(R,V,B,A))), the carrier of V))
len f is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
len (R,V,l,A) is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
D is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
dom f is finite set
g is Element of the carrier of V
(R,V,l,A) . D is set
Seg (len (R,V,l,A)) is finite len (R,V,l,A) -element Element of K19(NAT)
dom g is finite set
l . D is set
C <- (l . D) is set
l /. D is Element of the carrier of V
g . D is set
C . (g . D) is set
g is ext-real V26() V27() V28() V32() V33() finite cardinal V45() set
C . g is set
C /. g is Element of the carrier of V
dom (R,V,l,A) is finite set
Seg (len (R,V,C,(R,V,B,A))) is finite len (R,V,C,(R,V,B,A)) -element Element of K19(NAT)
f . D is set
(R,V,C,(R,V,B,A)) . (g . D) is set
(R,V,C,(R,V,B,A)) . (C <- (l . D)) is set
(R,V,B,A) . (C /. g) is Element of the carrier of R
(C /. g) * ((R,V,B,A) . (C /. g)) is Element of the carrier of V
A . (C /. g) is Element of the carrier of R
(A . (C /. g)) * B is Element of the carrier of R
(C /. g) * ((A . (C /. g)) * B) is Element of the carrier of V
(C /. g) * (A . (C /. g)) is Element of the carrier of V
((C /. g) * (A . (C /. g))) * B is Element of the carrier of V
g * B is Element of the carrier of V
Sum f is Element of the carrier of V
0. R is V54(R) Element of the carrier of R
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V)) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
0. R is V54(R) Element of the carrier of R
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
the carrier of R is non empty V12() set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is V54(R) Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),A) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A)) is Element of the carrier of V
(R,V,A) is Element of the carrier of V
- (R,V,A) is Element of the carrier of V
(R,V,A) * (- (1_ R)) is Element of the carrier of V
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
the carrier of R is non empty V12() set
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A) is Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
1_ R is Element of the carrier of R
K200(R) is V54(R) Element of the carrier of R
- (1_ R) is Element of the carrier of R
(R,V,(- (1_ R)),B) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,A,(R,V,B)) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,(R,V,A,B)) is Element of the carrier of V
(R,V,B) is Element of the carrier of V
(R,V,A) - (R,V,B) is Element of the carrier of V
(R,V,(R,V,B)) is Element of the carrier of V
(R,V,A) + (R,V,(R,V,B)) is Element of the carrier of V
- (R,V,B) is Element of the carrier of V
(R,V,A) + (- (R,V,B)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
B is Element of K19( the carrier of V)
the carrier of R is non empty set
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,v) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
(R,V,v) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not v . b₁ = 0. R } is set
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,B)
(R,V,l) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
0. R is V54(R) Element of the carrier of R
the carrier of R is non empty set
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
0. V is V54(V) Element of the carrier of V
A is Element of K19( the carrier of V)
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
B is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
B . (0. V) is Element of the carrier of R
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
{(0. V)} is non empty V12() finite 1 -element Element of K19( the carrier of V)
l is non empty V12() finite 1 -element Element of K19( the carrier of V)
D is Element of the carrier of V
v . D is Element of the carrier of R
D is finite Element of K19( the carrier of V)
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,l) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. R } is set
{(0. V)} is non empty V12() finite 1 -element Element of K19( the carrier of V)
D is set
C is Element of the carrier of V
l . C is Element of the carrier of R
D is set
D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,D) is Element of the carrier of V
D . (0. V) is Element of the carrier of R
(0. V) * (D . (0. V)) is Element of the carrier of V
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
{} the carrier of V is Function-like functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
the carrier of R is non empty set
A is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V, {} the carrier of V)
(R,V,A) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
(R,V,A) is finite Element of K19( the carrier of V)
0. R is V54(R) Element of the carrier of R
{ b₁ where b₁ is Element of the carrier of V : not A . b₁ = 0. R } is set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
0. R is V54(R) Element of the carrier of R
the carrier of R is non empty set
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
0. V is V54(V) 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 non empty finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
R is non empty V73() V98() V99() V100() unital V153() right-distributive left-distributive right_unital well-unital V161() left_unital L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
0. R is V54(R) Element of the carrier of R
the carrier of R is non empty set
1_ R is Element of the carrier of R
K200(R) is Element of the carrier of R
A is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
{A,(0. V)} is non empty finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{(0. V),A} is non empty finite Element of K19( the carrier of V)
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
the carrier of R is non empty V12() set
A is Element of K19( the carrier of V)
{ (R,V,b₁) where b₁ is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A) : verum } is set
(R,V) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
l is set
D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,D) is Element of the carrier of V
l is Element of K19( the carrier of V)
D is Element of the carrier of V
C is Element of the carrier of V
D + C is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,f) is Element of the carrier of V
C is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,C) is Element of the carrier of V
(R,V,f,C) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,f) is Element of the carrier of V
D is Element of the carrier of R
C is Element of the carrier of V
C * D is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,f) is Element of the carrier of V
(R,V,D,f) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
C is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,C) is Element of the carrier of V
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,v) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
B is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
the carrier of B is non empty set
v is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
the carrier of v is non empty set
R is set
V is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
the carrier of V is non empty V12() set
A is non empty V73() V98() V99() V100() RightMod-like RightModStr over V
the carrier of A is non empty set
K19( the carrier of A) is non empty set
B is Element of K19( the carrier of A)
(V,A,B) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of A
the carrier of (V,A,B) is non empty set
{ (V,A,b₁) where b₁ is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total (V,A,B) : verum } is set
v is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total (V,A,B)
(V,A,v) is Element of the carrier of A
{ (V,A,b₁) where b₁ is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total (V,A,B) : verum } is set
the carrier of (V,A,B) is non empty set
R is set
V is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
A is non empty V73() V98() V99() V100() RightMod-like RightModStr over V
the carrier of A is non empty set
K19( the carrier of A) is non empty set
B is Element of K19( the carrier of A)
(V,A,B) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of A
0. V is V54(V) Element of the carrier of V
the carrier of V is non empty V12() set
K20( the carrier of A, the carrier of V) is non empty set
K19(K20( the carrier of A, the carrier of V)) is non empty set
v is Element of the carrier of A
1_ V is Element of the carrier of V
K200(V) is V54(V) Element of the carrier of V
l is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of K19(K20( the carrier of A, the carrier of V))
l . v is Element of the carrier of V
Funcs ( the carrier of A, the carrier of V) is non empty FUNCTION_DOMAIN of the carrier of A, the carrier of V
D is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of Funcs ( the carrier of A, the carrier of V)
{v} is non empty V12() finite 1 -element Element of K19( the carrier of A)
C is non empty V12() finite 1 -element Element of K19( the carrier of A)
f is Element of the carrier of A
D . f is Element of the carrier of V
f is finite Element of K19( the carrier of A)
C is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total (V,A)
(V,A,C) is finite Element of K19( the carrier of A)
{ b₁ where b₁ is Element of the carrier of A : not C . b₁ = 0. V } is set
{v} is non empty V12() finite 1 -element Element of K19( the carrier of A)
f is set
C is Element of the carrier of A
C . C is Element of the carrier of V
f is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total (V,A,{v})
(V,A,f) is Element of the carrier of A
v * (1_ V) is Element of the carrier of A
(V,A,f) is finite Element of K19( the carrier of A)
{ b₁ where b₁ is Element of the carrier of A : not f . b₁ = 0. V } is set
C is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total (V,A,B)
(V,A,C) is Element of the carrier of A
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
{} the carrier of V is Function-like functional empty proper ext-real V26() V27() V28() V30() V31() V32() V33() finite V38() cardinal {} -element FinSequence-membered V45() Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
(R,V,({} the carrier of V)) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
(0). V is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
B is Element of the carrier of V
the carrier of (R,V,({} the carrier of V)) is non empty set
the carrier of R is non empty V12() set
{ (R,V,b₁) where b₁ is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V, {} the carrier of V) : verum } is set
0. V is V54(V) Element of the carrier of V
v is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V, {} the carrier of V)
(R,V,v) is Element of the carrier of V
0. V is V54(V) Element of the carrier of V
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
(0). V is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
0. V is V54(V) Element of the carrier of V
{(0. V)} is non empty V12() finite 1 -element Element of K19( the carrier of V)
A is Element of K19( the carrier of V)
(R,V,A) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
B is set
the Element of A is Element of A
v is set
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
0. R is V54(R) Element of the carrier of R
the carrier of R is non empty V12() set
1_ R is Element of the carrier of R
K200(R) is V54(R) Element of the carrier of R
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
B is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
the carrier of B is non empty set
v is Element of the carrier of V
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,l) is Element of the carrier of V
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
0. R is V54(R) Element of the carrier of R
the carrier of R is non empty V12() set
1_ R is Element of the carrier of R
K200(R) is V54(R) Element of the carrier of R
V is non empty V73() V98() V99() V100() strict RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
(Omega). V is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
the U5 of V is Relation-like K20( the carrier of V, the carrier of V) -defined the carrier of V -valued Function-like quasi_total Element of K19(K20(K20( the carrier of V, the carrier of V), the carrier of V))
K20( the carrier of V, the carrier of V) is non empty set
K20(K20( the carrier of V, the carrier of V), the carrier of V) is non empty set
K19(K20(K20( 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 K20( the carrier of V, the carrier of R) -defined the carrier of V -valued Function-like quasi_total Element of K19(K20(K20( the carrier of V, the carrier of R), the carrier of V))
K20( the carrier of V, the carrier of R) is non empty set
K20(K20( the carrier of V, the carrier of R), the carrier of V) is non empty set
K19(K20(K20( the carrier of V, the carrier of R), the carrier of V)) is non empty set
RightModStr(# the carrier of V, the U5 of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
B is Element of K19( the carrier of V)
(R,V,B) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
v is Element of the carrier of V
the carrier of R is non empty V12() set
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
(R,V,l) is Element of the carrier of V
D is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,B)
(R,V,D) is Element of the carrier of V
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
V is non empty V73() V98() V99() V100() strict RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
B is Element of K19( the carrier of V)
(R,V,B) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
B is Element of K19( the carrier of V)
A \/ B is Element of K19( the carrier of V)
(R,V,(A \/ B)) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
(R,V,B) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
(R,V,A) + (R,V,B) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
0. R is V54(R) Element of the carrier of R
the carrier of R is non empty V12() set
v is Element of the carrier of V
l is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A \/ B)
(R,V,l) is Element of the carrier of V
(R,V,l) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. R } is set
(R,V,l) \ A is finite Element of K19( the carrier of V)
(R,V,l) /\ A is finite Element of K19( the carrier of V)
f is set
K20( the carrier of V, the carrier of R) is non empty set
K19(K20( the carrier of V, the carrier of R)) is non empty set
C is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
f . C is Element of the carrier of R
l . f is set
f is set
l . f is set
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
Funcs ( the carrier of V, the carrier of R) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of R
C is finite Element of K19( the carrier of V)
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
f is Element of the carrier of V
f . f is Element of the carrier of R
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,f) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not f . b₁ = 0. R } is set
f is set
g is Element of the carrier of V
f . g is Element of the carrier of R
g is set
D is Element of the carrier of V
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
g . D is Element of the carrier of R
l . g is set
g is set
l . g is set
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of R))
D is finite Element of K19( the carrier of V)
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of R)
g is Element of the carrier of V
g . g is Element of the carrier of R
g is set
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
(R,V,g) is finite Element of K19( the carrier of V)
{ b₁ where b₁ is Element of the carrier of V : not g . b₁ = 0. R } is set
g is set
v is Element of the carrier of V
g . v is Element of the carrier of R
f is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,A)
g is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V,B)
(R,V,f,g) is Relation-like the carrier of V -defined the carrier of R -valued Function-like quasi_total (R,V)
v is Element of the carrier of V
l . v is Element of the carrier of R
(R,V,f,g) . v is Element of the carrier of R
f . v is Element of the carrier of R
g . v is Element of the carrier of R
(f . v) + (g . v) is Element of the carrier of R
(l . v) + (g . v) is Element of the carrier of R
(l . v) + (0. R) is Element of the carrier of R
f . v is Element of the carrier of R
g . v is Element of the carrier of R
(f . v) + (g . v) is Element of the carrier of R
(0. R) + (g . v) is Element of the carrier of R
f . v is Element of the carrier of R
g . v is Element of the carrier of R
(f . v) + (g . v) is Element of the carrier of R
(0. R) + (g . v) is Element of the carrier of R
(0. R) + (0. R) is Element of the carrier of R
(R,V,f) is Element of the carrier of V
(R,V,g) is Element of the carrier of V
(R,V,f) + (R,V,g) is Element of the carrier of V
R is non empty non degenerated V52() V73() V98() V99() V100() unital V153() V155() right-distributive left-distributive right_unital well-unital V161() left_unital domRing-like L11()
V is non empty V73() V98() V99() V100() RightMod-like RightModStr over R
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
(R,V,A) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
B is Element of K19( the carrier of V)
A /\ B is Element of K19( the carrier of V)
(R,V,(A /\ B)) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
(R,V,B) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V
(R,V,A) /\ (R,V,B) is non empty V73() V98() V99() V100() strict RightMod-like Submodule of V