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

RAT is set
INT is 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

dom {} is set
rng {} is 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

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

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))

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

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

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

len D 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
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))

len f 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
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

len D 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
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

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

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

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

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

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

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

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(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

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

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

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

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

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)

rng B is finite set

Sum v is Element of the carrier of V
rng v is finite set

rng l is finite set
B is Element of the carrier of V
Sum l is Element 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

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,({} V)) is Element of the carrier of V
0. V is V54(V) Element 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

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

Sum <*A*> is Element of the carrier of V
rng <*A*> is V12() finite 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
(R,V,{A,B}) is Element of the carrier of V
A + B is Element of the carrier of V

rng <*A,B*> is finite set
Sum <*A,B*> is Element of the carrier of V

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

rng <*A,B,v*> is finite set
Sum <*A,B,v*> is Element of the carrier of V

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

rng v is finite set
Sum v is Element of the carrier of V

rng l is finite set
Sum l is Element of the carrier of V

rng D is finite set
Sum D is Element of the carrier of V

rng (l ^ D) is finite set
Sum (l ^ D) is Element of the carrier of V

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

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

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)

(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

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

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

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

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

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

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
{ b1 where b1 is Element of the carrier of V : not A . b1 = 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

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

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
{ b1 where b1 is Element of the carrier of V : not B . b1 = 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
{ b1 where b1 is Element of the carrier of l : not C . b1 = 0. v } is set

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
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0. R } is set
v is Element of the carrier of V
B . v 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
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

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
{ b1 where b1 is Element of the carrier of V : not v . b1 = 0. R } is set
the Element of { b1 where b1 is Element of the carrier of V : not v . b1 = 0. R } is Element of { b1 where b1 is Element of the carrier of V : not v . b1 = 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
{ b1 where b1 is Element of the carrier of V : not A . b1 = 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)
{ b1 where b1 is Element of the carrier of V : not B . b1 = 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

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
{ b1 where b1 is Element of the carrier of V : not (R,V) . b1 = 0. R } is 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
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
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0. R } is set

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
{ b1 where b1 is Element of the carrier of V : not v . b1 = 0. R } is set

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
{ b1 where b1 is Element of the carrier of V : not (R,V) . b1 = 0. R } is set

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
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0. R } is 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 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
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0. R } is 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 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

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))

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

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

len v is ext-real V26() V27() V28() V32() V33() finite cardinal V45() Element of NAT
dom v is finite set

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

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

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

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

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

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 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 . 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

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

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

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

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

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

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
{ b1 where b1 is Element of the carrier of V : not A . b1 = 0. R } is set

rng B is finite set

(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

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

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

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

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
{ b1 where b1 is Element of the carrier of V : not (R,V) . b1 = 0. R } is set

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

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)
{ b1 where b1 is Element of the carrier of V : not B . b1 = 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)
{ b1 where b1 is Element of the carrier of V : not B . b1 = 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)
{ b1 where b1 is Element of the carrier of V : not v . b1 = 0. R } is set
(R,V,v) is Element 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)
{ b1 where b1 is Element of the carrier of V : not f . b1 = 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

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)
{ b1 where b1 is Element of the carrier of V : not f . b1 = 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) - () 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)
{ b1 where b1 is Element of the carrier of V : not v . b1 = 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)
{ b1 where b1 is Element of the carrier of V : not B . b1 = 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)
{ b1 where b1 is Element of the carrier of V : not C . b1 = 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