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

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

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

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

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

the Element of { b

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

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

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

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

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

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

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

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

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

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

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

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

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

(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

(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

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

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

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

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