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
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is set
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
{ b1 where b1 is Element of the carrier of L1 : not L2 . b1 = 0. V } is set
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
{ b1 where b1 is Element of the carrier of G : not f . b1 = 0. F } 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
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
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
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
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is set
the Element of { b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is Element of { b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF }
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
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is 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)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } 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
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
{ b1 where b1 is Element of the carrier of V : not (GF,V) . b1 = 0. GF } is set
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
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } 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
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
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } 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
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
{ b1 where b1 is Element of the carrier of V : not (GF,V) . b1 = 0. GF } 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
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
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } 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
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
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is set
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
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is set
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
{ b1 where b1 is Element of the carrier of V : not (GF,V) . b1 = 0. GF } is 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
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)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
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)
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is set
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)
{ b1 where b1 is Element of the carrier of V : not P . b1 = 0. GF } is set
(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)
{ b1 where b1 is Element of the carrier of V : not P . b1 = 0. GF } is set
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)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
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)
{ b1 where b1 is Element of the carrier of V : not f . b1 = 0. GF } is set
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)
{ b1 where b1 is Element of the carrier of V : not g . b1 = 0. GF } is set
(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)
{ b1 where b1 is Element of the carrier of V : not f . b1 = 0. GF } is set
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)
{ b1 where b1 is Element of the carrier of V : not g . b1 = 0. GF } is set
(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
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
(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
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is set
(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
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is set
(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
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
(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
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is set
(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
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is set
(GF,V,L2) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
(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
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is set
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)
{ b1 where b1 is Element of the carrier of V : not (GF,V,L1,L2) . b1 = 0. GF } is set
(GF,V,L2) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
(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
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
(GF,V,l) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is set
(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)
{ b1 where b1 is Element of the carrier of V : not (GF,V,L2,l) . b1 = 0. GF } 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
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 carrier of V
(GF,V,L1,(GF,V)) . L2 is Element of the carrier of GF
L1 . L2 is Element of the carrier of GF
(GF,V) . L2 is Element of the carrier of GF
(L1 . L2) + ((GF,V) . L2) is Element of the carrier of GF
0. GF is V62(GF) Element of the carrier of GF
(L1 . L2) + (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 GF
L2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,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
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))
Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF
G is Element of the carrier of V
(GF,V,L2) 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
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
L2 . G 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 Element of Funcs ( the carrier of V, the carrier of GF)
F . G is Element of the carrier of GF
L1 * (0. GF) is Element of the carrier of GF
G is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
f is Element of the carrier of V
G . f is Element of the carrier of GF
L2 . f is Element of the carrier of GF
L1 * (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)
F is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
G is Element of the carrier of V
l . G is Element of the carrier of GF
F . G is Element of the carrier of GF
L2 . G is Element of the carrier of GF
L1 * (L2 . G) 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 GF
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)
(GF,V,(GF,V,L1,L2)) 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
{ b1 where b1 is Element of the carrier of V : not (GF,V,L1,L2) . b1 = 0. GF } is set
(GF,V,L2) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
G is set
f is Element of the carrier of V
(GF,V,L1,L2) . f is Element of the carrier of GF
L2 . f is Element of the carrier of GF
L1 * (L2 . f) is Element of the carrier of GF
GF is non empty non degenerated V60() right_complementable almost_left_invertible V105() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of GF is non empty V12() 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 GF
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)
(GF,V,(GF,V,L1,L2)) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b1 where b1 is Element of the carrier of V : not (GF,V,L1,L2) . b1 = 0. GF } is set
(GF,V,L2) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
G is set
f is Element of the carrier of V
(GF,V,L1,L2) . f is Element of the carrier of GF
L2 . f is Element of the carrier of GF
L1 * (L2 . f) is Element of the carrier of GF
G is set
f is Element of the carrier of V
L2 . f is Element of the carrier of GF
(GF,V,L1,L2) . f is Element of the carrier of GF
L1 * (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
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 Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,(0. GF),L1) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
L2 is Element of the carrier of V
(GF,V,(0. GF),L1) . L2 is Element of the carrier of GF
(GF,V) . L2 is Element of the carrier of GF
L1 . L2 is Element of the carrier of GF
(0. GF) * (L1 . L2) 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 the carrier of GF
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)
(GF,V,L1,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
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is set
(GF,V,(GF,V,L1,l)) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not (GF,V,L1,l) . b1 = 0. GF } 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
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 GF
L2 is Element of the carrier of GF
L1 + L2 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,(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,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)
(GF,V,(GF,V,L1,l),(GF,V,L2,l)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L1,l) + (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
F is Element of the carrier of V
(GF,V,(L1 + L2),l) . F is Element of the carrier of GF
(GF,V,(GF,V,L1,l),(GF,V,L2,l)) . F is Element of the carrier of GF
l . F is Element of the carrier of GF
(L1 + L2) * (l . F) is Element of the carrier of GF
L1 * (l . F) is Element of the carrier of GF
L2 * (l . F) is Element of the carrier of GF
(L1 * (l . F)) + (L2 * (l . F)) is Element of the carrier of GF
(GF,V,L1,l) . F is Element of the carrier of GF
((GF,V,L1,l) . F) + (L2 * (l . F)) is Element of the carrier of GF
(GF,V,L2,l) . F is Element of the carrier of GF
((GF,V,L1,l) . F) + ((GF,V,L2,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
L1 is Element of the carrier of GF
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)
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,L1,(GF,V,L2,l)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L1,l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,(GF,V,L1,L2),(GF,V,L1,l)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L1,L2) + (GF,V,L1,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),(GF,V,L1,l)) . F is Element of the carrier of GF
(GF,V,L2,l) . F is Element of the carrier of GF
L1 * ((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 * ((L2 . F) + (l . F)) is Element of the carrier of GF
L1 * (L2 . F) is Element of the carrier of GF
L1 * (l . F) is Element of the carrier of GF
(L1 * (L2 . F)) + (L1 * (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) + (L1 * (l . F)) is Element of the carrier of GF
(GF,V,L1,l) . F is Element of the carrier of GF
((GF,V,L1,L2) . F) + ((GF,V,L1,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
L1 is Element of the carrier of GF
L2 is Element of the carrier of GF
L1 * L2 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)
(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)
(GF,V,(L1 * L2),l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
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,(L1 * L2),l) . F is Element of the carrier of GF
(GF,V,L2,l) . F is Element of the carrier of GF
L1 * ((GF,V,L2,l) . F) is Element of the carrier of GF
l . F is Element of the carrier of GF
L2 * (l . F) is Element of the carrier of GF
L1 * (L2 * (l . F)) is Element of the carrier of GF
(L1 * L2) * (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
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
L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,(1. GF),L1) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
L2 is Element of the carrier of V
(GF,V,(1. GF),L1) . L2 is Element of the carrier of GF
L1 . L2 is Element of the carrier of GF
(1. GF) * (L1 . L2) 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
1. GF is Element of the carrier of GF
- (1. GF) 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,(- (1. GF)),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 Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,(- (1. GF)),l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,(- (1. GF)),L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
F is Element of the carrier of V
l . F is Element of the carrier of GF
(GF,V,(- (1. GF)),L2) . F is Element of the carrier of GF
(1. GF) * (l . F) is Element of the carrier of GF
(1. GF) * (1. GF) is Element of the carrier of GF
((1. GF) * (1. GF)) * (l . F) is Element of the carrier of GF
(- (1. GF)) * (- (1. GF)) is Element of the carrier of GF
((- (1. GF)) * (- (1. GF))) * (l . F) is Element of the carrier of GF
(GF,V,((- (1. GF)) * (- (1. GF))),l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,((- (1. GF)) * (- (1. GF))),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
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
V is Element of the carrier of GF
(- (1. GF)) * V is Element of the carrier of GF
- V is Element of the carrier of GF
0. GF is V62(GF) Element of the carrier of GF
(0. GF) - (1. GF) is Element of the carrier of GF
((0. GF) - (1. GF)) * V is Element of the carrier of GF
(0. GF) * V is Element of the carrier of GF
(1. GF) * V is Element of the carrier of GF
((0. GF) * V) - ((1. GF) * V) is Element of the carrier of GF
(0. GF) - ((1. GF) * V) is Element of the carrier of GF
- ((1. GF) * V) 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)
(GF,V,L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L2) . L1 is Element of the carrier of GF
L2 . L1 is Element of the carrier of GF
- (L2 . L1) is Element of the carrier of GF
(- (1. GF)) * (L2 . 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
(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) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),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 Element of the carrier of V
L2 . l is Element of the carrier of GF
(GF,V,L1) . l is Element of the carrier of GF
L1 . l is Element of the carrier of GF
(L1 . l) + (L2 . l) is Element of the carrier of GF
(GF,V) . l is Element of the carrier of GF
0. GF is V62(GF) Element of the carrier of GF
- (L1 . l) is Element of the carrier of GF
GF is non empty non degenerated V60() right_complementable almost_left_invertible V105() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
1. GF is V62(GF) Element of the carrier of GF
the carrier of GF is non empty V12() set
- (1. GF) is Element of the carrier of GF
0. GF is V62(GF) Element of the carrier of 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 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 quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),L1) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(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
{ b1 where b1 is Element of the carrier of V : not (GF,V,L1) . b1 = 0. GF } is set
(GF,V,L1) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is 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,(- (1. GF)),(GF,V,L1)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,(GF,V,(GF,V,L1))) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not (GF,V,(GF,V,L1)) . b1 = 0. GF } 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
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
L2 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,L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),L2) 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
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)
(GF,V,L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L1,(GF,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 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 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)
(GF,V,l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L2,(GF,V,l)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
L2 + (GF,V,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
(GF,V,l) . L1 is Element of the carrier of GF
(L2 . L1) + ((GF,V,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
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
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is set
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)
(GF,V,L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L1,(GF,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 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)
{ b1 where b1 is Element of the carrier of V : not (GF,V,L1,L2) . b1 = 0. GF } is set
(GF,V,L2) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
(GF,V,L1) \/ (GF,V,L2) is finite Element of K19( the carrier of V)
(GF,V,(GF,V,L2)) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not (GF,V,L2) . b1 = 0. GF } is set
(GF,V,L1) \/ (GF,V,(GF,V,L2)) is finite 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
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)
(GF,V,l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),l) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L2,(GF,V,l)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
L2 + (GF,V,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 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,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 quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),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,L1)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
L1 + (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))
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
L2 is Element of the carrier of V
(GF,V,L1,L1) . L2 is Element of the carrier of GF
(GF,V) . L2 is Element of the carrier of GF
L1 . L2 is Element of the carrier of GF
(L1 . L2) - (L1 . L2) is Element of the carrier of GF
0. GF is V62(GF) 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 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)
(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 Element of the carrier of V
(GF,V,L2) is Element of the carrier of V
(GF,V,L1) + (GF,V,L2) is Element of the carrier of V
(GF,V,(GF,V,L1,L2)) 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
{ b1 where b1 is Element of the carrier of V : not (GF,V,L1,L2) . b1 = 0. GF } is set
(GF,V,L1) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is set
(GF,V,(GF,V,L1,L2)) \/ (GF,V,L1) is finite Element of K19( the carrier of V)
(GF,V,L2) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0. GF } is set
((GF,V,(GF,V,L1,L2)) \/ (GF,V,L1)) \/ (GF,V,L2) is finite Element of K19( the carrier of V)
(((GF,V,(GF,V,L1,L2)) \/ (GF,V,L1)) \/ (GF,V,L2)) \ (GF,V,L1) is finite Element of K19( the carrier of V)
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng G is finite set
(GF,V,(GF,V,L1,L2)) \/ (GF,V,L2) is finite Element of K19( the carrier of V)
(GF,V,L1) \/ ((GF,V,(GF,V,L1,L2)) \/ (GF,V,L2)) is finite Element of K19( the carrier of V)
(((GF,V,(GF,V,L1,L2)) \/ (GF,V,L1)) \/ (GF,V,L2)) \ (GF,V,(GF,V,L1,L2)) is finite Element of K19( the carrier of V)
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng P is finite set
(GF,V,L1) \/ (GF,V,L2) is finite Element of K19( the carrier of V)
(GF,V,(GF,V,L1,L2)) \/ ((GF,V,L1) \/ (GF,V,L2)) is finite Element of K19( the carrier of V)
(((GF,V,(GF,V,L1,L2)) \/ (GF,V,L1)) \/ (GF,V,L2)) \ (GF,V,L2) is finite Element of K19( the carrier of V)
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng P is finite set
k is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng k is finite set
(GF,V,k,(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
Sum (GF,V,k,(GF,V,L1,L2)) 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
k ^ P is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
i is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng i is finite set
(GF,V,i,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,i,L1) is Element of the carrier of V
rng (k ^ P) is finite set
rng P is finite set
(rng k) \/ (rng P) is finite set
(GF,V,(GF,V,L1,L2)) \/ (((GF,V,(GF,V,L1,L2)) \/ (GF,V,L1)) \/ (GF,V,L2)) is finite Element of K19( 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
i ^ 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 (i ^ f) is finite set
rng f is finite set
(rng i) \/ (rng f) is finite set
(GF,V,L1) \/ (((GF,V,(GF,V,L1,L2)) \/ (GF,V,L1)) \/ (GF,V,L2)) is finite Element of K19( the carrier of V)
(rng k) /\ (rng P) is finite set
the Element of (rng k) /\ (rng P) is Element of (rng k) /\ (rng P)
(rng i) /\ (rng f) is finite set
the Element of (rng i) /\ (rng f) is Element of (rng i) /\ (rng f)
len (i ^ f) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
len (k ^ P) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom P is finite set
Seg (len (k ^ P)) is V34() V35() V36() V37() V38() V39() finite len (k ^ P) -element Element of K19(NAT)
g is set
dom (i ^ f) is finite set
f is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
(i ^ f) . f is set
P . f is set
(k ^ P) . (P . f) is set
(k ^ P) <- ((i ^ f) . f) is set
(k ^ P) . ((k ^ P) <- ((i ^ f) . f)) is set
(i ^ f) . g is set
P . g is set
(k ^ P) . (P . g) is set
rng P is finite set
dom (k ^ P) is finite set
g is set
f is set
P . f is set
H is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
(i ^ f) . H is set
P . H is set
(k ^ P) <- ((i ^ f) . H) is set
g is set
P . g is set
Seg (len P) is V34() V35() V36() V37() V38() V39() finite len P -element Element of K19(NAT)
Seg (len P) is V34() V35() V36() V37() V38() V39() finite len P -element Element of K19(NAT)
P (#) (k ^ P) is Relation-like Function-like finite set
(k ^ P) " is Relation-like Function-like set
(i ^ f) (#) ((k ^ P) ") is Relation-like Function-like finite set
f is set
dom ((k ^ P) ") is set
rng ((i ^ f) (#) ((k ^ P) ")) is finite set
rng ((k ^ P) ") is set
(k ^ P) (#) ((k ^ P) ") is Relation-like Function-like finite set
P (#) ((k ^ P) (#) ((k ^ P) ")) is Relation-like Function-like finite set
id (dom (k ^ P)) is Relation-like Function-like one-to-one set
P (#) (id (dom (k ^ P))) is Relation-like Function-like finite set
len P is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
(GF,V,P,(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
len (GF,V,P,(GF,V,L1,L2)) 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() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom P is finite set
P /. g is Element of the carrier of V
P . g is set
dom (GF,V,P,(GF,V,L1,L2)) is finite set
(GF,V,P,(GF,V,L1,L2)) . g is set
(GF,V,L1,L2) . (P /. g) is Element of the carrier of GF
((GF,V,L1,L2) . (P /. g)) * (P /. g) is Element of the carrier of V
(0. GF) * (P /. g) is Element of the carrier of V
Sum (GF,V,P,(GF,V,L1,L2)) is Element of the carrier of V
Sum P is Element of the carrier of V
(0. GF) * (Sum P) is Element of the carrier of V
0. V is V62(V) 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
(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
len (GF,V,f,L1) 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() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom f is finite set
f /. g is Element of the carrier of V
f . g is set
dom (GF,V,f,L1) is finite set
(GF,V,f,L1) . g is set
L1 . (f /. g) is Element of the carrier of GF
(L1 . (f /. g)) * (f /. g) is Element of the carrier of V
(0. GF) * (f /. g) is Element of the carrier of V
Sum (GF,V,f,L1) is Element of the carrier of V
Sum f is Element of the carrier of V
(0. GF) * (Sum f) is Element of the carrier of V
Fp is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len Fp is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
(GF,V,Fp,L2) 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,Fp,L2) 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() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom Fp is finite set
Fp /. g is Element of the carrier of V
Fp . g is set
dom (GF,V,Fp,L2) is finite set
(GF,V,Fp,L2) . g is set
L2 . (Fp /. g) is Element of the carrier of GF
(L2 . (Fp /. g)) * (Fp /. g) is Element of the carrier of V
(0. GF) * (Fp /. g) is Element of the carrier of V
Sum (GF,V,Fp,L2) is Element of the carrier of V
Sum Fp is Element of the carrier of V
(0. GF) * (Sum Fp) is Element of the carrier of V
(GF,V,(i ^ 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
len (GF,V,(i ^ f),L1) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
Seg (len (i ^ f)) is V34() V35() V36() V37() V38() V39() finite len (i ^ f) -element Element of K19(NAT)
dom (GF,V,(i ^ f),L1) is finite set
(GF,V,(k ^ P),(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
H is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng H is finite set
(GF,V,H,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,H,L2) is Element of the carrier of V
H ^ Fp is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng Fp is finite set
(rng H) /\ (rng Fp) is finite set
the Element of (rng H) /\ (rng Fp) is Element of (rng H) /\ (rng Fp)
rng (H ^ Fp) is finite set
(rng H) \/ (rng Fp) is finite set
(GF,V,L2) \/ (((GF,V,(GF,V,L1,L2)) \/ (GF,V,L1)) \/ (GF,V,L2)) is finite Element of K19( the carrier of V)
len (H ^ Fp) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
R is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len R is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom R is finite set
Seg (len (H ^ Fp)) is V34() V35() V36() V37() V38() V39() finite len (H ^ Fp) -element Element of K19(NAT)
h is set
R is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
(i ^ f) . R is set
R . R is set
(H ^ Fp) . (R . R) is set
(H ^ Fp) <- ((i ^ f) . R) is set
(H ^ Fp) . ((H ^ Fp) <- ((i ^ f) . R)) is set
(i ^ f) . h is set
R . h is set
(H ^ Fp) . (R . h) is set
rng R is finite set
dom (H ^ Fp) is finite set
h is set
R is set
R . R is set
R is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
(i ^ f) . R is set
R . R is set
(H ^ Fp) <- ((i ^ f) . R) is set
h is set
R . h is set
Seg (len R) is V34() V35() V36() V37() V38() V39() finite len R -element Element of K19(NAT)
Seg (len R) is V34() V35() V36() V37() V38() V39() finite len R -element Element of K19(NAT)
R (#) (H ^ Fp) is Relation-like Function-like finite set
(H ^ Fp) " is Relation-like Function-like set
(i ^ f) (#) ((H ^ Fp) ") is Relation-like Function-like finite set
R is set
dom ((H ^ Fp) ") is set
rng ((i ^ f) (#) ((H ^ Fp) ")) is finite set
rng ((H ^ Fp) ") is set
(H ^ Fp) (#) ((H ^ Fp) ") is Relation-like Function-like finite set
R (#) ((H ^ Fp) (#) ((H ^ Fp) ")) is Relation-like Function-like finite set
id (dom (H ^ Fp)) is Relation-like Function-like one-to-one set
R (#) (id (dom (H ^ Fp))) is Relation-like Function-like finite set
(GF,V,(H ^ Fp),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,(H ^ Fp),L2) is Element of the carrier of V
(GF,V,H,L2) ^ (GF,V,Fp,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,H,L2) ^ (GF,V,Fp,L2)) is Element of the carrier of V
(Sum (GF,V,H,L2)) + (0. V) is Element of the carrier of V
Sum (GF,V,(i ^ f),L1) is Element of the carrier of V
(GF,V,i,L1) ^ (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,i,L1) ^ (GF,V,f,L1)) is Element of the carrier of V
(Sum (GF,V,i,L1)) + (0. V) is Element of the carrier of V
K20((dom (H ^ Fp)),(dom (H ^ Fp))) is finite set
K19(K20((dom (H ^ Fp)),(dom (H ^ Fp)))) is non empty finite V45() set
R is Relation-like dom (H ^ Fp) -defined dom (H ^ Fp) -valued Function-like quasi_total finite Element of K19(K20((dom (H ^ Fp)),(dom (H ^ Fp))))
len (GF,V,(H ^ Fp),L2) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom (GF,V,(H ^ Fp),L2) is finite set
K20((dom (GF,V,(H ^ Fp),L2)),(dom (GF,V,(H ^ Fp),L2))) is finite set
K19(K20((dom (GF,V,(H ^ Fp),L2)),(dom (GF,V,(H ^ Fp),L2)))) is non empty finite V45() set
R is Relation-like dom (H ^ Fp) -defined dom (H ^ Fp) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (H ^ Fp)),(dom (H ^ Fp))))
R is Relation-like dom (GF,V,(H ^ Fp),L2) -defined dom (GF,V,(H ^ Fp),L2) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (GF,V,(H ^ Fp),L2)),(dom (GF,V,(H ^ Fp),L2))))
R (#) (GF,V,(H ^ Fp),L2) is Relation-like Function-like finite set
Hp is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len Hp is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
K20((dom (k ^ P)),(dom (k ^ P))) is finite set
K19(K20((dom (k ^ P)),(dom (k ^ P)))) is non empty finite V45() set
P is Relation-like dom (k ^ P) -defined dom (k ^ P) -valued Function-like quasi_total finite Element of K19(K20((dom (k ^ P)),(dom (k ^ P))))
len (GF,V,(k ^ P),(GF,V,L1,L2)) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom (GF,V,(k ^ P),(GF,V,L1,L2)) is finite set
K20((dom (GF,V,(k ^ P),(GF,V,L1,L2))),(dom (GF,V,(k ^ P),(GF,V,L1,L2)))) is finite set
K19(K20((dom (GF,V,(k ^ P),(GF,V,L1,L2))),(dom (GF,V,(k ^ P),(GF,V,L1,L2))))) is non empty finite V45() set
P is Relation-like dom (k ^ P) -defined dom (k ^ P) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (k ^ P)),(dom (k ^ P))))
P is Relation-like dom (GF,V,(k ^ P),(GF,V,L1,L2)) -defined dom (GF,V,(k ^ P),(GF,V,L1,L2)) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (GF,V,(k ^ P),(GF,V,L1,L2))),(dom (GF,V,(k ^ P),(GF,V,L1,L2)))))
P (#) (GF,V,(k ^ P),(GF,V,L1,L2)) is Relation-like Function-like finite set
Sum (GF,V,(k ^ P),(GF,V,L1,L2)) is Element of the carrier of V
(GF,V,k,(GF,V,L1,L2)) ^ (GF,V,P,(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
Sum ((GF,V,k,(GF,V,L1,L2)) ^ (GF,V,P,(GF,V,L1,L2))) is Element of the carrier of V
(Sum (GF,V,k,(GF,V,L1,L2))) + (0. V) is Element of the carrier of V
I is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len I is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom I is finite set
I is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
I . I is set
(GF,V,(i ^ f),L1) /. I is Element of the carrier of V
Hp /. I is Element of the carrier of V
((GF,V,(i ^ f),L1) /. I) + (Hp /. I) is Element of the carrier of V
rng I is finite set
I is set
x is set
I . x is set
k is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
I . k is set
(GF,V,(i ^ f),L1) /. k is Element of the carrier of V
Hp /. k is Element of the carrier of V
((GF,V,(i ^ f),L1) /. k) + (Hp /. k) is Element of the carrier of V
Fp is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len Fp is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
I is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len I is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
x is set
Seg (len I) is V34() V35() V36() V37() V38() V39() finite len I -element Element of K19(NAT)
dom Hp is finite set
k is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
Hp /. k is Element of the carrier of V
(R (#) (GF,V,(H ^ Fp),L2)) . k is set
R . k is set
(GF,V,(H ^ Fp),L2) . (R . k) is set
(i ^ f) /. k is Element of the carrier of V
dom Fp is finite set
Fp . k is set
P . k is set
(GF,V,(k ^ P),(GF,V,L1,L2)) . (P . k) is set
dom R is finite set
j is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
(H ^ Fp) . j is set
(i ^ f) . k is set
dom P is finite set
l is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
(k ^ P) . l is set
(GF,V,(H ^ Fp),L2) . j is set
L2 . ((i ^ f) /. k) is Element of the carrier of GF
(L2 . ((i ^ f) /. k)) * ((i ^ f) /. k) is Element of the carrier of V
(GF,V,(k ^ P),(GF,V,L1,L2)) . l is set
(GF,V,L1,L2) . ((i ^ f) /. k) is Element of the carrier of GF
((GF,V,L1,L2) . ((i ^ f) /. k)) * ((i ^ f) /. k) is Element of the carrier of V
L1 . ((i ^ f) /. k) is Element of the carrier of GF
(L1 . ((i ^ f) /. k)) + (L2 . ((i ^ f) /. k)) is Element of the carrier of GF
((L1 . ((i ^ f) /. k)) + (L2 . ((i ^ f) /. k))) * ((i ^ f) /. k) is Element of the carrier of V
(L1 . ((i ^ f) /. k)) * ((i ^ f) /. k) is Element of the carrier of V
((L1 . ((i ^ f) /. k)) * ((i ^ f) /. k)) + ((L2 . ((i ^ f) /. k)) * ((i ^ f) /. k)) is Element of the carrier of V
(GF,V,(i ^ f),L1) /. k is Element of the carrier of V
(GF,V,(i ^ f),L1) . k is set
I . x is set
Fp . x is set
dom I is finite set
Sum Fp is Element of the carrier of V
Sum Hp is Element of the carrier of V
GF is non empty non degenerated V60() right_complementable almost_left_invertible V105() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of GF is non empty V12() 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 Element of the carrier of V
L2 is Element of the carrier of GF
(GF,V,L2,L1) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,(GF,V,L2,L1)) is Element of the carrier of V
L2 * (GF,V,L1) is Element of the carrier of V
0. GF is V62(GF) Element of the carrier of GF
(GF,V,(GF,V,L2,L1)) is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
{ b1 where b1 is Element of the carrier of V : not (GF,V,L2,L1) . b1 = 0. GF } is 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
rng F is finite set
(GF,V,F,(GF,V,L2,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,(GF,V,L2,L1)) is Element of the carrier of V
(GF,V,L1) is finite Element of K19( the carrier of V)
{ b1 where b1 is Element of the carrier of V : not L1 . b1 = 0. GF } is set
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 G is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
len F is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
P is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len P is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom P is finite set
rng P is finite set
Seg (len F) is V34() V35() V36() V37() V38() V39() finite len F -element Element of K19(NAT)
P is set
P is set
P . P is set
P is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom G is finite set
G . P is set
P . P is set
F <- (G . P) is set
dom F is finite set
P is set
dom G is finite set
P . P is set
dom F is finite set
Seg (len P) is V34() V35() V36() V37() V38() V39() finite len P -element Element of K19(NAT)
Seg (len P) is V34() V35() V36() V37() V38() V39() finite len P -element Element of K19(NAT)
P is set
P is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
G . P is set
P . P is set
F . (P . P) is set
F <- (G . P) is set
F . (F <- (G . P)) is set
G . P is set
P . P is set
F . (P . P) is set
P (#) F is Relation-like Function-like finite set
F " is Relation-like Function-like set
G (#) (F ") is Relation-like Function-like finite set
P is set
dom (F ") is set
rng (G (#) (F ")) is finite set
rng (F ") is set
F (#) (F ") is Relation-like Function-like finite set
P (#) (F (#) (F ")) is Relation-like Function-like finite set
id (dom F) is Relation-like Function-like one-to-one set
P (#) (id (dom F)) is Relation-like Function-like finite set
K20((Seg (len F)),(Seg (len F))) is finite set
K19(K20((Seg (len F)),(Seg (len F)))) is non empty finite V45() set
P is Relation-like Seg (len F) -defined Seg (len F) -valued Function-like quasi_total finite Element of K19(K20((Seg (len F)),(Seg (len F))))
len (GF,V,F,(GF,V,L2,L1)) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom (GF,V,F,(GF,V,L2,L1)) is finite set
K20((dom (GF,V,F,(GF,V,L2,L1))),(dom (GF,V,F,(GF,V,L2,L1)))) is finite set
K19(K20((dom (GF,V,F,(GF,V,L2,L1))),(dom (GF,V,F,(GF,V,L2,L1))))) is non empty finite V45() set
P is Relation-like Seg (len F) -defined Seg (len F) -valued Function-like quasi_total bijective finite Element of K19(K20((Seg (len F)),(Seg (len F))))
P is Relation-like dom (GF,V,F,(GF,V,L2,L1)) -defined dom (GF,V,F,(GF,V,L2,L1)) -valued Function-like quasi_total bijective finite Element of K19(K20((dom (GF,V,F,(GF,V,L2,L1))),(dom (GF,V,F,(GF,V,L2,L1)))))
P (#) (GF,V,F,(GF,V,L2,L1)) is Relation-like Function-like finite set
Fp is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
len Fp is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
len (GF,V,G,L1) is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
k is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
dom (GF,V,G,L1) is finite set
v is Element of the carrier of V
(GF,V,G,L1) . k is set
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 P is finite set
G . k is set
F <- (G . k) is set
G /. k is Element of the carrier of V
P . k is set
F . (P . k) is set
i is ext-real V28() V32() V33() V34() V35() V36() V37() V38() V39() finite cardinal V52() V53() Element of NAT
F . i is set
F /. i is Element of the carrier of V
Seg (len (GF,V,F,(GF,V,L2,L1))) is V34() V35() V36() V37() V38() V39() finite len (GF,V,F,(GF,V,L2,L1)) -element Element of K19(NAT)
Fp . k is set
(GF,V,F,(GF,V,L2,L1)) . (P . k) is set
(GF,V,F,(GF,V,L2,L1)) . (F <- (G . k)) is set
(GF,V,L2,L1) . (F /. i) is Element of the carrier of GF
((GF,V,L2,L1) . (F /. i)) * (F /. i) is Element of the carrier of V
L1 . (F /. i) is Element of the carrier of GF
L2 * (L1 . (F /. i)) is Element of the carrier of GF
(L2 * (L1 . (F /. i))) * (F /. i) is Element of the carrier of V
(L1 . (F /. i)) * (F /. i) is Element of the carrier of V
L2 * ((L1 . (F /. i)) * (F /. i)) is Element of the carrier of V
L2 * v is Element of the carrier of V
Sum Fp is Element of the carrier of V
dom Fp is finite set
0. GF is V62(GF) Element of the carrier of GF
(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
0. GF is V62(GF) 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 Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),L1) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,(GF,V,L1)) is Element of the carrier of V
(GF,V,L1) is Element of the carrier of V
- (GF,V,L1) is Element of the carrier of V
(GF,V,L1) + (GF,V,(GF,V,L1)) is Element of the carrier of V
(GF,V,L1,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,L1)) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
L1 + (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))
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,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,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
L1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,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)
(GF,V,L1,L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(GF,V,(- (1. GF)),L2) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total (GF,V)
(GF,V,L1,(GF,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 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 Element of the carrier of V
(GF,V,L2) is Element of the carrier of V
(GF,V,L1) - (GF,V,L2) is Element of the carrier of V
(GF,V,(GF,V,L2)) is Element of the carrier of V
(GF,V,L1) + (GF,V,(GF,V,L2)) is Element of the carrier of V
- (GF,V,L2) is Element of the carrier of V
(GF,V,L1) + (- (GF,V,L2)) 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
1. GF is Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
V is Element of the carrier of GF
(- (1. GF)) * V is Element of the carrier of GF
- V is Element of the carrier of GF
GF is non empty non degenerated V60() right_complementable almost_left_invertible V105() associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
1. GF is V62(GF) Element of the carrier of GF
the carrier of GF is non empty V12() set
- (1. GF) is Element of the carrier of GF
0. GF is V62(GF) Element of the carrier of GF