:: VECTSP_6 semantic presentation

REAL is non empty V12() V34() V35() V36() V40() non finite set

NAT is V12() V28() V34() V35() V36() V37() V38() V39() V40() non finite cardinal limit_cardinal Element of K19(REAL)

K19(REAL) is non empty V12() non finite set

NAT is V12() V28() V34() V35() V36() V37() V38() V39() V40() non finite cardinal limit_cardinal set

K19(NAT) is non empty V12() non finite set

K19(NAT) is non empty V12() non finite set

K20(NAT,REAL) is V12() non finite set

K19(K20(NAT,REAL)) is non empty V12() non finite set

{} is set

the Function-like functional empty ext-real non positive non negative V28() V32() V34() V35() V36() V37() V38() V39() V40() finite V45() cardinal {} -element FinSequence-membered set is Function-like functional empty ext-real non positive non negative V28() V32() V34() V35() V36() V37() V38() V39() V40() finite V45() cardinal {} -element FinSequence-membered set

1 is non empty ext-real positive non negative V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

2 is non empty ext-real positive non negative V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

3 is non empty ext-real positive non negative V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

Seg 1 is non empty V12() V34() V35() V36() V37() V38() V39() finite 1 -element Element of K19(NAT)

{1} is non empty V12() V34() V35() V36() V37() V38() V39() finite V45() 1 -element set

Seg 2 is non empty V34() V35() V36() V37() V38() V39() finite 2 -element Element of K19(NAT)

{1,2} is V34() V35() V36() V37() V38() V39() finite V45() set

Seg 3 is non empty V34() V35() V36() V37() V38() V39() finite 3 -element Element of K19(NAT)

K44(1,2,3) is non empty V34() V35() V36() V37() V38() V39() finite set

0 is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

GF is non empty ZeroStr

V is non empty VectSpStr over GF

the carrier of V is non empty set

the carrier of GF is non empty set

Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF

K19( the carrier of V) is non empty set

0. GF is V62(GF) Element of the carrier of GF

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

the carrier of V --> (0. GF) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)

{} V is Function-like functional empty proper ext-real non positive non negative V28() V32() V34() V35() V36() V37() V38() V39() V40() finite V45() cardinal {} -element FinSequence-membered Element of K19( the carrier of V)

l is Element of the carrier of V

L2 . l is Element of the carrier of GF

GF is non empty ZeroStr

V is non empty VectSpStr over GF

the carrier of V is non empty set

the carrier of GF is non empty set

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

0. GF is V62(GF) Element of the carrier of GF

{ b

K19( the carrier of V) is non empty set

l is finite Element of K19( the carrier of V)

F is set

G is Element of the carrier of V

L1 . G is Element of the carrier of GF

V is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

L1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V

the carrier of L1 is non empty set

the carrier of V is non empty set

F is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

G is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over F

the carrier of G is non empty set

the carrier of F is non empty set

GF is set

L2 is Relation-like the carrier of L1 -defined the carrier of V -valued Function-like quasi_total (V,L1)

(V,L1,L2) is finite Element of K19( the carrier of L1)

K19( the carrier of L1) is non empty set

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

{ b

l is set

g is Element of the carrier of G

f is Relation-like the carrier of G -defined the carrier of F -valued Function-like quasi_total (F,G)

f . g is Element of the carrier of F

0. F is V62(F) Element of the carrier of F

(F,G,f) is finite Element of K19( the carrier of G)

K19( the carrier of G) is non empty set

{ b

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

0. GF is V62(GF) Element of the carrier of GF

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

L1 is Element of the carrier of V

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 . L1 is Element of the carrier of GF

(GF,V,L2) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

{ b

l is Element of the carrier of V

L2 . l is Element of the carrier of GF

GF is non empty ZeroStr

V is non empty VectSpStr over GF

the carrier of V is non empty set

the carrier of GF is non empty set

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

0. GF is V62(GF) Element of the carrier of GF

the carrier of V --> (0. GF) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)

K19( the carrier of V) is non empty set

{} V is Function-like functional empty proper ext-real non positive non negative V28() V32() V34() V35() V36() V37() V38() V39() V40() finite V45() cardinal {} -element FinSequence-membered Element of K19( the carrier of V)

l is Function-like functional empty proper ext-real non positive non negative V28() V32() V34() V35() V36() V37() V38() V39() V40() finite V45() cardinal {} -element FinSequence-membered Element of K19( the carrier of V)

F is Element of the carrier of V

L2 . F is Element of the carrier of GF

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,l) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

{ b

the Element of { b

f is Element of the carrier of V

l . f is Element of the carrier of GF

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

0. GF is V62(GF) Element of the carrier of GF

{ b

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L2) is finite Element of K19( the carrier of V)

{ b

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

G is set

f is Element of the carrier of V

L2 . f is Element of the carrier of GF

L1 . f is Element of the carrier of GF

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

l . G is set

F is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

F . G is set

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

0. GF is V62(GF) Element of the carrier of GF

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 is Element of the carrier of V

(GF,V) . L1 is Element of the carrier of GF

(GF,V,(GF,V)) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

{ b

GF is non empty ZeroStr

V is non empty VectSpStr over GF

the carrier of V is non empty set

K19( the carrier of V) is non empty set

the carrier of GF is non empty set

L1 is Element of K19( the carrier of V)

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L2) is finite Element of K19( the carrier of V)

0. GF is V62(GF) Element of the carrier of GF

{ b

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

K19( the carrier of V) is non empty set

L1 is Element of K19( the carrier of V)

L2 is Element of K19( the carrier of V)

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,L1)

(GF,V,l) is finite Element of K19( the carrier of V)

0. GF is V62(GF) Element of the carrier of GF

{ b

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

K19( the carrier of V) is non empty set

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 is Element of K19( the carrier of V)

(GF,V,(GF,V)) is finite Element of K19( the carrier of V)

0. GF is V62(GF) Element of the carrier of GF

{ b

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

{} the carrier of V is Function-like functional empty proper ext-real non positive non negative V28() V32() V34() V35() V36() V37() V38() V39() V40() finite V45() cardinal {} -element FinSequence-membered Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V, {} the carrier of V)

(GF,V,L1) is finite Element of K19( the carrier of V)

0. GF is V62(GF) Element of the carrier of GF

{ b

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

the carrier of GF is non empty set

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

0. GF is V62(GF) Element of the carrier of GF

{ b

GF is non empty addLoopStr

V is non empty VectSpStr over GF

the carrier of V is non empty set

the carrier of GF is non empty set

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

L1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

len L1 is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

l is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

len l is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom l is finite set

rng l is finite set

F is set

G is set

l . G is set

Seg (len L1) is V34() V35() V36() V37() V38() V39() finite len L1 -element Element of K19(NAT)

f is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

l . f is set

L1 /. f is Element of the carrier of V

L2 . (L1 /. f) is Element of the carrier of GF

(L2 . (L1 /. f)) * (L1 /. f) is Element of the carrier of V

F is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

len F is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom F is finite set

G is ext-real V28() V32() finite cardinal set

F . G is set

L1 /. G is Element of the carrier of V

L2 . (L1 /. G) is Element of the carrier of GF

(L2 . (L1 /. G)) * (L1 /. G) 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 V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom l is finite set

F is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

len F is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom F is finite set

G is ext-real V28() V32() finite cardinal set

Seg (len l) is V34() V35() V36() V37() V38() V39() finite len l -element Element of K19(NAT)

l . G is set

L1 /. G is Element of the carrier of V

L2 . (L1 /. G) is Element of the carrier of GF

(L2 . (L1 /. G)) * (L1 /. G) is Element of the carrier of V

F . G is set

GF is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

V is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of V is non empty set

L1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V

the carrier of L1 is non empty set

K20( the carrier of L1, the carrier of V) is non empty set

K19(K20( the carrier of L1, the carrier of V)) is non empty set

L2 is Element of the carrier of L1

l is Relation-like NAT -defined the carrier of L1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of L1

dom l is finite set

l . GF is set

F is Relation-like the carrier of L1 -defined the carrier of V -valued Function-like quasi_total Element of K19(K20( the carrier of L1, the carrier of V))

(V,L1,l,F) is Relation-like NAT -defined the carrier of L1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of L1

(V,L1,l,F) . GF is set

F . L2 is Element of the carrier of V

(F . L2) * L2 is Element of the carrier of L1

l /. GF is Element of the carrier of L1

len (V,L1,l,F) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len l is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom (V,L1,l,F) is finite set

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) 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 ext-real non positive non negative V28() V32() V34() V35() V36() V37() V38() V39() V40() finite finite-yielding V45() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of V

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

(GF,V,(<*> the carrier of V),L1) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

len (GF,V,(<*> the carrier of V),L1) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len (<*> the carrier of V) is Function-like functional empty ext-real non positive non negative V28() V32() V33() V34() V35() V36() V37() V38() V39() V40() finite V45() cardinal {} -element FinSequence-membered V52() V53() Element of NAT

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

L1 is Element of the carrier of V

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

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

(GF,V,<*L1*>,L2) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

L2 . L1 is Element of the carrier of GF

(L2 . L1) * L1 is Element of the carrier of V

<*((L2 . L1) * L1)*> 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() V34() V35() V36() V37() V38() V39() finite V45() 1 -element Element of K19(REAL)

len (GF,V,<*L1*>,L2) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len <*L1*> is non empty ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom (GF,V,<*L1*>,L2) is finite set

(GF,V,<*L1*>,L2) . 1 is set

<*L1*> /. 1 is Element of the carrier of V

L2 . (<*L1*> /. 1) is Element of the carrier of GF

(L2 . (<*L1*> /. 1)) * (<*L1*> /. 1) is Element of the carrier of V

(L2 . (<*L1*> /. 1)) * L1 is Element of the carrier of V

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

L1 is Element of the carrier of V

L2 is Element of the carrier of V

<*L1,L2*> 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

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

(GF,V,<*L1,L2*>,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 . L1 is Element of the carrier of GF

(l . L1) * L1 is Element of the carrier of V

l . L2 is Element of the carrier of GF

(l . L2) * L2 is Element of the carrier of V

<*((l . L1) * L1),((l . L2) * L2)*> 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 (GF,V,<*L1,L2*>,l) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len <*L1,L2*> is non empty ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom (GF,V,<*L1,L2*>,l) is finite set

{1,2} is V34() V35() V36() V37() V38() V39() finite V45() Element of K19(REAL)

(GF,V,<*L1,L2*>,l) . 2 is set

<*L1,L2*> /. 2 is Element of the carrier of V

l . (<*L1,L2*> /. 2) is Element of the carrier of GF

(l . (<*L1,L2*> /. 2)) * (<*L1,L2*> /. 2) is Element of the carrier of V

(l . (<*L1,L2*> /. 2)) * L2 is Element of the carrier of V

(GF,V,<*L1,L2*>,l) . 1 is set

<*L1,L2*> /. 1 is Element of the carrier of V

l . (<*L1,L2*> /. 1) is Element of the carrier of GF

(l . (<*L1,L2*> /. 1)) * (<*L1,L2*> /. 1) is Element of the carrier of V

(l . (<*L1,L2*> /. 1)) * L1 is Element of the carrier of V

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

L1 is Element of the carrier of V

L2 is Element of the carrier of V

l is Element of the carrier of V

<*L1,L2,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

F is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

(GF,V,<*L1,L2,l*>,F) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

F . L1 is Element of the carrier of GF

(F . L1) * L1 is Element of the carrier of V

F . L2 is Element of the carrier of GF

(F . L2) * L2 is Element of the carrier of V

F . l is Element of the carrier of GF

(F . l) * l is Element of the carrier of V

<*((F . L1) * L1),((F . L2) * L2),((F . l) * 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

len (GF,V,<*L1,L2,l*>,F) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len <*L1,L2,l*> is non empty ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom (GF,V,<*L1,L2,l*>,F) is finite set

{1,2,3} is non empty V34() V35() V36() V37() V38() V39() finite Element of K19(REAL)

(GF,V,<*L1,L2,l*>,F) . 3 is set

<*L1,L2,l*> /. 3 is Element of the carrier of V

F . (<*L1,L2,l*> /. 3) is Element of the carrier of GF

(F . (<*L1,L2,l*> /. 3)) * (<*L1,L2,l*> /. 3) is Element of the carrier of V

(F . (<*L1,L2,l*> /. 3)) * l is Element of the carrier of V

(GF,V,<*L1,L2,l*>,F) . 2 is set

<*L1,L2,l*> /. 2 is Element of the carrier of V

F . (<*L1,L2,l*> /. 2) is Element of the carrier of GF

(F . (<*L1,L2,l*> /. 2)) * (<*L1,L2,l*> /. 2) is Element of the carrier of V

(F . (<*L1,L2,l*> /. 2)) * L2 is Element of the carrier of V

(GF,V,<*L1,L2,l*>,F) . 1 is set

<*L1,L2,l*> /. 1 is Element of the carrier of V

F . (<*L1,L2,l*> /. 1) is Element of the carrier of GF

(F . (<*L1,L2,l*> /. 1)) * (<*L1,L2,l*> /. 1) is Element of the carrier of V

(F . (<*L1,L2,l*> /. 1)) * L1 is Element of the carrier of V

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

L1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

L2 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

L1 ^ L2 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

(GF,V,(L1 ^ L2),l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

(GF,V,L1,l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

(GF,V,L2,l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

(GF,V,L1,l) ^ (GF,V,L2,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 L1 is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len (GF,V,L1,l) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len ((GF,V,L1,l) ^ (GF,V,L2,l)) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len (GF,V,L2,l) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

(len (GF,V,L1,l)) + (len (GF,V,L2,l)) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

(len L1) + (len (GF,V,L2,l)) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len L2 is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

(len L1) + (len L2) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len (L1 ^ L2) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

f is ext-real V28() V32() finite cardinal set

dom ((GF,V,L1,l) ^ (GF,V,L2,l)) is finite set

dom (GF,V,L1,l) is finite set

dom L1 is finite set

dom (L1 ^ L2) is finite set

L1 /. f is Element of the carrier of V

L1 . f is set

(L1 ^ L2) . f is set

(L1 ^ L2) /. f is Element of the carrier of V

((GF,V,L1,l) ^ (GF,V,L2,l)) . f is set

(GF,V,L1,l) . f is set

l . ((L1 ^ L2) /. f) is Element of the carrier of GF

(l . ((L1 ^ L2) /. f)) * ((L1 ^ L2) /. f) is Element of the carrier of V

dom (GF,V,L2,l) is finite set

dom (L1 ^ L2) is finite set

g is ext-real V28() V32() finite cardinal set

(len (GF,V,L1,l)) + g is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

g is ext-real V28() V32() finite cardinal set

(len (GF,V,L1,l)) + g is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom L2 is finite set

L2 /. g is Element of the carrier of V

L2 . g is set

(L1 ^ L2) . f is set

(L1 ^ L2) /. f is Element of the carrier of V

((GF,V,L1,l) ^ (GF,V,L2,l)) . f is set

(GF,V,L2,l) . g is set

l . ((L1 ^ L2) /. f) is Element of the carrier of GF

(l . ((L1 ^ L2) /. f)) * ((L1 ^ L2) /. f) is Element of the carrier of V

dom (GF,V,L1,l) is finite set

dom (GF,V,L2,l) is finite set

((GF,V,L1,l) ^ (GF,V,L2,l)) . f is set

(L1 ^ L2) /. f is Element of the carrier of V

l . ((L1 ^ L2) /. f) is Element of the carrier of GF

(l . ((L1 ^ L2) /. f)) * ((L1 ^ L2) /. f) is Element of the carrier of V

((GF,V,L1,l) ^ (GF,V,L2,l)) . f is set

(L1 ^ L2) /. f is Element of the carrier of V

l . ((L1 ^ L2) /. f) is Element of the carrier of GF

(l . ((L1 ^ L2) /. f)) * ((L1 ^ L2) /. f) is Element of the carrier of V

GF is non empty addLoopStr

V is non empty VectSpStr over GF

the carrier of V is non empty set

the carrier of GF is non empty set

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

0. GF is V62(GF) Element of the carrier of GF

{ b

L2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

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

(GF,V,l,L1) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (GF,V,l,L1) is Element of the carrier of V

rng l is finite set

L2 is Element of the carrier of V

l is Element of the carrier of V

F is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng F is finite set

(GF,V,F,L1) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (GF,V,F,L1) is Element of the carrier of V

G is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng G is finite set

(GF,V,G,L1) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (GF,V,G,L1) is Element of the carrier of V

len F is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len G is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

dom F is finite set

Seg (len F) is V34() V35() V36() V37() V38() V39() finite len F -element Element of K19(NAT)

dom G is finite set

Seg (len G) is V34() V35() V36() V37() V38() V39() finite len G -element Element of K19(NAT)

f is set

G . f is set

{(G . f)} is non empty V12() finite 1 -element set

F " {(G . f)} is finite set

g is set

{g} is non empty V12() finite 1 -element set

K20((dom F),(dom F)) is finite set

K19(K20((dom F),(dom F))) is non empty finite V45() set

f is Relation-like dom F -defined dom F -valued Function-like quasi_total finite Element of K19(K20((dom F),(dom F)))

rng f is finite set

g is set

F . g is set

P is set

G . P is set

{(G . P)} is non empty V12() finite 1 -element set

F " {(G . P)} is finite set

Im (F,g) is set

{g} is non empty V12() finite 1 -element set

F .: {g} is finite set

F " (Im (F,g)) is finite set

f . P is set

{(f . P)} is non empty V12() finite 1 -element set

dom f is finite set

len (GF,V,F,L1) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

P is set

dom f is finite set

f . P is set

P is set

f . P is set

G . P is set

{(G . P)} is non empty V12() finite 1 -element set

F " {(G . P)} is finite set

{(f . P)} is non empty V12() finite 1 -element set

G . P is set

{(G . P)} is non empty V12() finite 1 -element set

F " {(G . P)} is finite set

{(f . P)} is non empty V12() finite 1 -element set

dom (GF,V,G,L1) is finite set

len (GF,V,G,L1) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

Seg (len (GF,V,G,L1)) is V34() V35() V36() V37() V38() V39() finite len (GF,V,G,L1) -element Element of K19(NAT)

dom (GF,V,F,L1) is finite set

Seg (len (GF,V,F,L1)) is V34() V35() V36() V37() V38() V39() finite len (GF,V,F,L1) -element Element of K19(NAT)

K20((dom (GF,V,F,L1)),(dom (GF,V,F,L1))) is finite set

K19(K20((dom (GF,V,F,L1)),(dom (GF,V,F,L1)))) is non empty finite V45() set

P is Relation-like dom F -defined dom F -valued Function-like quasi_total bijective finite Element of K19(K20((dom F),(dom F)))

P is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

(GF,V,G,L1) . P is set

G /. P is Element of the carrier of V

L1 . (G /. P) is Element of the carrier of GF

(L1 . (G /. P)) * (G /. P) is Element of the carrier of V

G . P is set

P is Relation-like dom (GF,V,F,L1) -defined dom (GF,V,F,L1) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (GF,V,F,L1)),(dom (GF,V,F,L1))))

dom P is finite set

P . P is set

k is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

F . k is set

F . (P . P) is set

{(F . (P . P))} is non empty V12() finite 1 -element set

Im (F,(P . P)) is set

{(P . P)} is non empty V12() finite 1 -element set

F .: {(P . P)} is finite set

{(G . P)} is non empty V12() finite 1 -element set

F " {(G . P)} is finite set

F .: (F " {(G . P)}) is finite set

Fp is Element of the carrier of V

v is Element of the carrier of V

F /. k is Element of the carrier of V

(GF,V,F,L1) . (P . P) is set

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

the carrier of V is non empty set

the carrier of GF is non empty set

(GF,V,(GF,V)) is Element of the carrier of V

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

(GF,V,(GF,V)) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

0. GF is V62(GF) Element of the carrier of GF

{ b

L1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng L1 is finite set

(GF,V,L1,(GF,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 (GF,V,L1,(GF,V)) is Element of the carrier of V

len L1 is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len (GF,V,L1,(GF,V)) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

0. GF is V62(GF) Element of the carrier of GF

the carrier of GF is non empty set

1. GF is Element of the carrier of GF

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

K19( the carrier of V) is non empty set

L1 is Element of K19( the carrier of V)

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,L1)

(GF,V,L2) is finite Element of K19( the carrier of V)

{ b

card (GF,V,L2) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

(GF,V,L2) is Element of the carrier of V

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

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

L2 is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

L2 + 1 is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,L1)

(GF,V,l) is finite Element of K19( the carrier of V)

{ b

card (GF,V,l) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

(GF,V,l) is Element of the carrier of V

F is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng F is finite set

(GF,V,F,l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (GF,V,F,l) is Element of the carrier of V

Seg L2 is V34() V35() V36() V37() V38() V39() finite L2 -element Element of K19(NAT)

F | (Seg L2) is Relation-like NAT -defined Function-like finite FinSubsequence-like set

len F is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

len (GF,V,F,l) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

Seg (L2 + 1) is V34() V35() V36() V37() V38() V39() finite L2 + 1 -element Element of K19(NAT)

dom F is finite set

F . (L2 + 1) is set

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

f is Element of the carrier of V

g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

g . f is Element of the carrier of GF

Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF

P is Element of the carrier of V

P is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)

P . P is Element of the carrier of GF

l . P is Element of the carrier of GF

{f} is non empty V12() finite 1 -element Element of K19( the carrier of V)

L1 \ {f} is Element of K19( the carrier of V)

l . f is Element of the carrier of GF

(l . f) * f is Element of the carrier of V

P is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,P) is finite Element of K19( the carrier of V)

{ b

(GF,V,l) \ {f} is finite Element of K19( the carrier of V)

P is set

P is Element of the carrier of V

P . P is Element of the carrier of GF

l . P is Element of the carrier of GF

P is set

P is Element of the carrier of V

l . P is Element of the carrier of GF

P . P is Element of the carrier of GF

G is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

len G is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

P is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,L1)

(GF,V,G,P) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

len (GF,V,G,P) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

rng G is finite set

(GF,V,P) is finite Element of K19( the carrier of V)

{ b

P is set

dom G is finite set

Fp is set

G . Fp is set

k is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

G . k is set

F . k is set

P is set

Fp is set

F . Fp is set

k is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

(dom F) \ (Seg L2) is finite Element of K19((dom F))

K19((dom F)) is non empty finite V45() set

(Seg (L2 + 1)) \ (Seg L2) is V34() V35() V36() V37() V38() V39() finite Element of K19(NAT)

{(L2 + 1)} is non empty V12() V34() V35() V36() V37() V38() V39() finite V45() 1 -element Element of K19(REAL)

(dom F) /\ (Seg L2) is V34() V35() V36() V37() V38() V39() finite Element of K19(NAT)

dom G is finite set

G . k is set

F . k is set

(Seg (L2 + 1)) /\ (Seg L2) is V34() V35() V36() V37() V38() V39() finite Element of K19(NAT)

dom (GF,V,G,P) is finite set

dom (GF,V,F,l) is finite set

(dom (GF,V,F,l)) /\ (Seg L2) is V34() V35() V36() V37() V38() V39() finite Element of K19(NAT)

P is set

Fp is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

F . Fp is set

dom G is finite set

G . Fp is set

v is Element of the carrier of V

(GF,V,G,P) . Fp is set

P . v is Element of the carrier of GF

(P . v) * v is Element of the carrier of V

l . v is Element of the carrier of GF

(l . v) * v is Element of the carrier of V

k is Element of the carrier of V

(GF,V,G,P) . P is set

(GF,V,F,l) . P is set

(GF,V,F,l) | (Seg L2) is Relation-like NAT -defined Function-like finite FinSubsequence-like set

(GF,V,F,l) | (dom (GF,V,G,P)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set

card (GF,V,P) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

card {f} is non empty ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

(L2 + 1) - (card {f}) is set

(L2 + 1) - 1 is set

(GF,V,P) is Element of the carrier of V

Sum (GF,V,G,P) is Element of the carrier of V

(GF,V,F,l) . (len F) is set

(Sum (GF,V,G,P)) + ((l . f) * f) is Element of the carrier of V

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,L1)

(GF,V,L2) is Element of the carrier of V

(GF,V,L2) is finite Element of K19( the carrier of V)

{ b

card (GF,V,L2) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,(GF,V)) is Element of the carrier of V

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

L2 is Element of the carrier of GF

l is Element of the carrier of V

L2 * l is Element of the carrier of V

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

F is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

F . l is Element of the carrier of GF

Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF

f is Element of the carrier of V

{l} is non empty V12() finite 1 -element Element of K19( the carrier of V)

G is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)

G . f is Element of the carrier of GF

f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,f) is finite Element of K19( the carrier of V)

{ b

g is set

P is Element of the carrier of V

f . P is Element of the carrier of GF

g is set

g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,L1)

(GF,V,g) is finite Element of K19( the carrier of V)

{ b

(GF,V,g) is Element of the carrier of V

P is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng P is finite set

(GF,V,P,g) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (GF,V,P,g) is Element of the carrier of V

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

g . l is Element of the carrier of GF

(g . l) * l is Element of the carrier of V

<*((g . l) * l)*> 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

L2 is Element of the carrier of V

l is Element of the carrier of V

L2 + l is Element of the carrier of V

(1. GF) * L2 is Element of the carrier of V

((1. GF) * L2) + L2 is Element of the carrier of V

((1. GF) * L2) + ((1. GF) * L2) is Element of the carrier of V

(1. GF) + (1. GF) is Element of the carrier of GF

((1. GF) + (1. GF)) * L2 is Element of the carrier of V

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

F is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of K19(K20( the carrier of V, the carrier of GF))

F . L2 is Element of the carrier of GF

F . l is Element of the carrier of GF

Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF

f is Element of the carrier of V

{L2,l} is finite Element of K19( the carrier of V)

G is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)

G . f is Element of the carrier of GF

f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,f) is finite Element of K19( the carrier of V)

{ b

g is set

P is Element of the carrier of V

f . P is Element of the carrier of GF

g is set

(1. GF) * l is Element of the carrier of V

(1. GF) * L2 is Element of the carrier of V

g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,L1)

(GF,V,g) is finite Element of K19( the carrier of V)

{ b

(GF,V,g) is Element of the carrier of V

P is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng P is finite set

(GF,V,P,g) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (GF,V,P,g) is Element of the carrier of V

<*L2,l*> 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

<*l,L2*> 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

<*((1. GF) * L2),((1. GF) * l)*> 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

<*((1. GF) * l),((1. GF) * L2)*> 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

l is Element of the carrier of V

L2 is Element of the carrier of GF

L2 * l is Element of the carrier of V

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

the carrier of V is non empty set

the carrier of GF is non empty set

(GF,V,(GF,V)) is Element of the carrier of V

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

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

{} the carrier of V is Function-like functional empty proper ext-real non positive non negative V28() V32() V34() V35() V36() V37() V38() V39() V40() finite V45() cardinal {} -element FinSequence-membered Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

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

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V, {} the carrier of V)

(GF,V,L1) is Element of the carrier of V

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

L1 is Element of the carrier of V

{L1} is non empty V12() finite 1 -element Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,{L1})

(GF,V,L2) is Element of the carrier of V

L2 . L1 is Element of the carrier of GF

(L2 . L1) * L1 is Element of the carrier of V

(GF,V,L2) is finite Element of K19( the carrier of V)

0. GF is V62(GF) Element of the carrier of GF

{ b

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

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

(0. GF) * L1 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

(GF,V,l,L2) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (GF,V,l,L2) is Element of the carrier of V

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

<*((L2 . L1) * L1)*> 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

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

L1 is Element of the carrier of V

L2 is Element of the carrier of V

{L1,L2} is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,{L1,L2})

(GF,V,l) is Element of the carrier of V

l . L1 is Element of the carrier of GF

(l . L1) * L1 is Element of the carrier of V

l . L2 is Element of the carrier of GF

(l . L2) * L2 is Element of the carrier of V

((l . L1) * L1) + ((l . L2) * L2) is Element of the carrier of V

(GF,V,l) is finite Element of K19( the carrier of V)

0. GF is V62(GF) Element of the carrier of GF

{ b

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

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

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

(0. GF) * L1 is Element of the carrier of V

((0. GF) * L1) + (0. V) is Element of the carrier of V

(0. GF) * L2 is Element of the carrier of V

((0. GF) * L1) + ((0. GF) * L2) is Element of the carrier of V

((l . L1) * L1) + ((0. GF) * L2) is Element of the carrier of V

{L1} is non empty V12() finite 1 -element Element of K19( the carrier of V)

F is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,{L1})

(GF,V,F) is Element of the carrier of V

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

((l . L1) * L1) + (0. V) is Element of the carrier of V

(0. GF) * L2 is Element of the carrier of V

((l . L1) * L1) + ((0. GF) * L2) is Element of the carrier of V

{L2} is non empty V12() finite 1 -element Element of K19( the carrier of V)

F is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V,{L2})

(GF,V,F) is Element of the carrier of V

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

(0. V) + ((l . L2) * L2) is Element of the carrier of V

(0. GF) * L1 is Element of the carrier of V

((0. GF) * L1) + ((l . L2) * L2) is Element of the carrier of V

F is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng F is finite set

(GF,V,F,l) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (GF,V,F,l) is Element of the carrier of V

<*L1,L2*> 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

<*L2,L1*> 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

<*((l . L1) * L1),((l . L2) * L2)*> 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

<*((l . L2) * L2),((l . L1) * L1)*> 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

{L1} is non empty V12() finite 1 -element Element of K19( the carrier of V)

{L2} is non empty V12() finite 1 -element Element of K19( the carrier of V)

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

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

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

0. GF is V62(GF) Element of the carrier of GF

{ b

(GF,V,L1) is Element of the carrier of V

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

L1 is Element of the carrier of V

{L1} is non empty V12() finite 1 -element Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L2) is finite Element of K19( the carrier of V)

0. GF is V62(GF) Element of the carrier of GF

{ b

(GF,V,L2) is Element of the carrier of V

L2 . L1 is Element of the carrier of GF

(L2 . L1) * L1 is Element of the carrier of V

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

L1 is Element of the carrier of V

L2 is Element of the carrier of V

{L1,L2} is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,l) is finite Element of K19( the carrier of V)

0. GF is V62(GF) Element of the carrier of GF

{ b

(GF,V,l) is Element of the carrier of V

l . L1 is Element of the carrier of GF

(l . L1) * L1 is Element of the carrier of V

l . L2 is Element of the carrier of GF

(l . L2) * L2 is Element of the carrier of V

((l . L1) * L1) + ((l . L2) * L2) is Element of the carrier of V

GF is non empty ZeroStr

V is non empty VectSpStr over GF

the carrier of V is non empty set

the carrier of GF is non empty set

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

l is Element of the carrier of V

L1 . l is Element of the carrier of GF

L2 . l is Element of the carrier of GF

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

the carrier of GF is non empty set

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 + L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

dom L1 is set

dom L2 is set

dom (L1 + L2) is set

(dom L1) /\ (dom L2) is set

Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF

F is Element of the carrier of V

(GF,V,L1) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

0. GF is V62(GF) Element of the carrier of GF

{ b

(GF,V,L2) is finite Element of K19( the carrier of V)

{ b

(GF,V,L1) \/ (GF,V,L2) is finite Element of K19( the carrier of V)

L2 . F is Element of the carrier of GF

L1 /. F is Element of the carrier of GF

L1 . F is Element of the carrier of GF

L2 /. F is Element of the carrier of GF

(L1 + L2) . F is set

(L1 + L2) /. F is Element of the carrier of GF

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

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

L1 is Element of the carrier of V

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 . L1 is Element of the carrier of GF

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L2,l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 + l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

(GF,V,L2,l) . L1 is Element of the carrier of GF

l . L1 is Element of the carrier of GF

(L2 . L1) + (l . L1) is Element of the carrier of GF

dom L2 is set

dom l is set

L2 /. L1 is Element of the carrier of GF

l /. L1 is Element of the carrier of GF

dom (GF,V,L2,l) is set

(GF,V,L2,l) /. L1 is Element of the carrier of GF

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1) is finite Element of K19( the carrier of V)

K19( the carrier of V) is non empty set

0. GF is V62(GF) Element of the carrier of GF

{ b

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1,L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 + L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

(GF,V,(GF,V,L1,L2)) is finite Element of K19( the carrier of V)

{ b

(GF,V,L2) is finite Element of K19( the carrier of V)

{ b

(GF,V,L1) \/ (GF,V,L2) is finite Element of K19( the carrier of V)

l is set

F is Element of the carrier of V

(GF,V,L1,L2) . F is Element of the carrier of GF

L1 . F is Element of the carrier of GF

L2 . F is Element of the carrier of GF

(L1 . F) + (L2 . F) is Element of the carrier of GF

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

K19( the carrier of V) is non empty set

L1 is Element of K19( the carrier of V)

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L2,l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 + l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

(GF,V,L2) is finite Element of K19( the carrier of V)

0. GF is V62(GF) Element of the carrier of GF

{ b

(GF,V,l) is finite Element of K19( the carrier of V)

{ b

(GF,V,L2) \/ (GF,V,l) is finite Element of K19( the carrier of V)

(GF,V,(GF,V,L2,l)) is finite Element of K19( the carrier of V)

{ b

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1,L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 + L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

(GF,V,L2,L1) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 + L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

l is Element of the carrier of V

(GF,V,L1,L2) . l is Element of the carrier of GF

(GF,V,L2,L1) . l is Element of the carrier of GF

L2 . l is Element of the carrier of GF

L1 . l is Element of the carrier of GF

(L2 . l) + (L1 . l) is Element of the carrier of GF

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1,L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 + L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L2,l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L2 + l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

(GF,V,L1,(GF,V,L2,l)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 + (GF,V,L2,l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

(GF,V,(GF,V,L1,L2),l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1,L2) + l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

F is Element of the carrier of V

(GF,V,L1,(GF,V,L2,l)) . F is Element of the carrier of GF

(GF,V,(GF,V,L1,L2),l) . F is Element of the carrier of GF

L1 . F is Element of the carrier of GF

(GF,V,L2,l) . F is Element of the carrier of GF

(L1 . F) + ((GF,V,L2,l) . F) is Element of the carrier of GF

L2 . F is Element of the carrier of GF

l . F is Element of the carrier of GF

(L2 . F) + (l . F) is Element of the carrier of GF

(L1 . F) + ((L2 . F) + (l . F)) is Element of the carrier of GF

(L1 . F) + (L2 . F) is Element of the carrier of GF

((L1 . F) + (L2 . F)) + (l . F) is Element of the carrier of GF

(GF,V,L1,L2) . F is Element of the carrier of GF

((GF,V,L1,L2) . F) + (l . F) is Element of the carrier of GF

GF is non empty right_complementable V105() associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of GF is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF

the carrier of V is non empty set

(GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V,L1,(GF,V)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

L1 + (GF,V) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

K20( the carrier of V, the carrier of GF) is non empty set

K19(K20( the carrier of V, the carrier of GF)) is non empty set

(GF,V,(GF,V),L1) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)

(GF,V) + L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like Element of K19(K20( the carrier of V, the carrier of GF))

L2 is Element of the