NAT is non empty V29() V30() V31() V36() V41() V42() countable denumerable Element of bool REAL
REAL is set
bool REAL is set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty set
{{},1} is non empty set
[:1,1:] is Relation-like set
bool [:1,1:] is set
[:[:1,1:],1:] is Relation-like set
bool [:[:1,1:],1:] is set
NAT is non empty V29() V30() V31() V36() V41() V42() countable denumerable set
bool NAT is V36() set
bool NAT is V36() set
2 is non empty set
3 is non empty set
K189() is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V29() V30() V31() V33() V34() V35() V36() V41() V43( {} ) Cardinal-yielding countable FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
Seg 1 is countable Element of bool NAT
G is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of G is non empty set
0. G is V65(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
GS is Element of the carrier of G
the addF of G . ((0. G),GS) is Element of the carrier of G
[(0. G),GS] is set
{(0. G),GS} is non empty set
{(0. G)} is non empty trivial V43(1) set
{{(0. G),GS},{(0. G)}} is non empty set
the addF of G . [(0. G),GS] is set
(0. G) + GS is Element of the carrier of G
the addF of G . (GS,(0. G)) is Element of the carrier of G
[GS,(0. G)] is set
{GS,(0. G)} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,(0. G)},{GS}} is non empty set
the addF of G . [GS,(0. G)] is set
GS + (0. G) is Element of the carrier of G
G is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of G is non empty set
comp G is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
bool [: the carrier of G, the carrier of G:] is set
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
0. G is V65(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
GS is Element of the carrier of G
(comp G) . GS is Element of the carrier of G
the addF of G . (GS,((comp G) . GS)) is Element of the carrier of G
[GS,((comp G) . GS)] is set
{GS,((comp G) . GS)} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,((comp G) . GS)},{GS}} is non empty set
the addF of G . [GS,((comp G) . GS)] is set
- GS is Element of the carrier of G
GS + (- GS) is Element of the carrier of G
the addF of G . (GS,(- GS)) is Element of the carrier of G
[GS,(- GS)] is set
{GS,(- GS)} is non empty set
{{GS,(- GS)},{GS}} is non empty set
the addF of G . [GS,(- GS)] is set
the_unity_wrt the addF of G is Element of the carrier of G
the addF of G . (((comp G) . GS),GS) is Element of the carrier of G
[((comp G) . GS),GS] is set
{((comp G) . GS),GS} is non empty set
{((comp G) . GS)} is non empty trivial V43(1) set
{{((comp G) . GS),GS},{((comp G) . GS)}} is non empty set
the addF of G . [((comp G) . GS),GS] is set
((comp G) . GS) + GS is Element of the carrier of G
G is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of G is non empty set
comp G is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
bool [: the carrier of G, the carrier of G:] is set
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
0. G is V65(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
GS is Element of the carrier of G
(comp G) . GS is Element of the carrier of G
the addF of G . (GS,((comp G) . GS)) is Element of the carrier of G
[GS,((comp G) . GS)] is set
{GS,((comp G) . GS)} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,((comp G) . GS)},{GS}} is non empty set
the addF of G . [GS,((comp G) . GS)] is set
- GS is Element of the carrier of G
GS + (- GS) is Element of the carrier of G
the addF of G . (GS,(- GS)) is Element of the carrier of G
[GS,(- GS)] is set
{GS,(- GS)} is non empty set
{{GS,(- GS)},{GS}} is non empty set
the addF of G . [GS,(- GS)] is set
the_unity_wrt the addF of G is Element of the carrier of G
the addF of G . (((comp G) . GS),GS) is Element of the carrier of G
[((comp G) . GS),GS] is set
{((comp G) . GS),GS} is non empty set
{((comp G) . GS)} is non empty trivial V43(1) set
{{((comp G) . GS),GS},{((comp G) . GS)}} is non empty set
the addF of G . [((comp G) . GS),GS] is set
((comp G) . GS) + GS is Element of the carrier of G
G is non empty addLoopStr
the carrier of G is non empty set
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
0. G is V65(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
comp G is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is set
GS is Element of the carrier of G
(comp G) . GS is Element of the carrier of G
i is Element of the carrier of G
GS + i is Element of the carrier of G
the addF of G . (GS,i) is Element of the carrier of G
[GS,i] is set
{GS,i} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,i},{GS}} is non empty set
the addF of G . [GS,i] is set
the_unity_wrt the addF of G is Element of the carrier of G
GS is Element of the carrier of G
i is Element of the carrier of G
GS + i is Element of the carrier of G
the addF of G . (GS,i) is Element of the carrier of G
[GS,i] is set
{GS,i} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,i},{GS}} is non empty set
the addF of G . [GS,i] is set
i + GS is Element of the carrier of G
the addF of G . (i,GS) is Element of the carrier of G
[i,GS] is set
{i,GS} is non empty set
{i} is non empty trivial V43(1) set
{{i,GS},{i}} is non empty set
the addF of G . [i,GS] is set
y is Element of the carrier of G
i is Element of the carrier of G
y + i is Element of the carrier of G
the addF of G . (y,i) is Element of the carrier of G
[y,i] is set
{y,i} is non empty set
{y} is non empty trivial V43(1) set
{{y,i},{y}} is non empty set
the addF of G . [y,i] is set
x is Element of the carrier of G
(y + i) + x is Element of the carrier of G
the addF of G . ((y + i),x) is Element of the carrier of G
[(y + i),x] is set
{(y + i),x} is non empty set
{(y + i)} is non empty trivial V43(1) set
{{(y + i),x},{(y + i)}} is non empty set
the addF of G . [(y + i),x] is set
i + x is Element of the carrier of G
the addF of G . (i,x) is Element of the carrier of G
[i,x] is set
{i,x} is non empty set
{i} is non empty trivial V43(1) set
{{i,x},{i}} is non empty set
the addF of G . [i,x] is set
y + (i + x) is Element of the carrier of G
the addF of G . (y,(i + x)) is Element of the carrier of G
[y,(i + x)] is set
{y,(i + x)} is non empty set
{{y,(i + x)},{y}} is non empty set
the addF of G . [y,(i + x)] is set
i is Element of the carrier of G
i + (0. G) is Element of the carrier of G
the addF of G . (i,(0. G)) is Element of the carrier of G
[i,(0. G)] is set
{i,(0. G)} is non empty set
{i} is non empty trivial V43(1) set
{{i,(0. G)},{i}} is non empty set
the addF of G . [i,(0. G)] is set
G is non empty addLoopStr
the carrier of G is non empty set
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
GS is Element of the carrier of G
i is Element of the carrier of G
GS + i is Element of the carrier of G
the addF of G . (GS,i) is Element of the carrier of G
[GS,i] is set
{GS,i} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,i},{GS}} is non empty set
the addF of G . [GS,i] is set
i + GS is Element of the carrier of G
the addF of G . (i,GS) is Element of the carrier of G
[i,GS] is set
{i,GS} is non empty set
{i} is non empty trivial V43(1) set
{{i,GS},{i}} is non empty set
the addF of G . [i,GS] is set
GS is Element of the carrier of G
i is Element of the carrier of G
GS + i is Element of the carrier of G
the addF of G . (GS,i) is Element of the carrier of G
[GS,i] is set
{GS,i} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,i},{GS}} is non empty set
the addF of G . [GS,i] is set
y is Element of the carrier of G
(GS + i) + y is Element of the carrier of G
the addF of G . ((GS + i),y) is Element of the carrier of G
[(GS + i),y] is set
{(GS + i),y} is non empty set
{(GS + i)} is non empty trivial V43(1) set
{{(GS + i),y},{(GS + i)}} is non empty set
the addF of G . [(GS + i),y] is set
i + y is Element of the carrier of G
the addF of G . (i,y) is Element of the carrier of G
[i,y] is set
{i,y} is non empty set
{i} is non empty trivial V43(1) set
{{i,y},{i}} is non empty set
the addF of G . [i,y] is set
GS + (i + y) is Element of the carrier of G
the addF of G . (GS,(i + y)) is Element of the carrier of G
[GS,(i + y)] is set
{GS,(i + y)} is non empty set
{{GS,(i + y)},{GS}} is non empty set
the addF of G . [GS,(i + y)] is set
G is non empty addLoopStr
the carrier of G is non empty set
0. G is V65(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
GS is Element of the carrier of G
GS + (0. G) is Element of the carrier of G
the addF of G . (GS,(0. G)) is Element of the carrier of G
[GS,(0. G)] is set
{GS,(0. G)} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,(0. G)},{GS}} is non empty set
the addF of G . [GS,(0. G)] is set
G is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V118() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of G is non empty non trivial set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
GS is Element of the carrier of G
i is Element of the carrier of G
y is Element of the carrier of G
the multF of G . (i,y) is Element of the carrier of G
[i,y] is set
{i,y} is non empty set
{i} is non empty trivial V43(1) set
{{i,y},{i}} is non empty set
the multF of G . [i,y] is set
the multF of G . (GS,( the multF of G . (i,y))) is Element of the carrier of G
[GS,( the multF of G . (i,y))] is set
{GS,( the multF of G . (i,y))} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,( the multF of G . (i,y))},{GS}} is non empty set
the multF of G . [GS,( the multF of G . (i,y))] is set
the multF of G . (GS,i) is Element of the carrier of G
[GS,i] is set
{GS,i} is non empty set
{{GS,i},{GS}} is non empty set
the multF of G . [GS,i] is set
the multF of G . (( the multF of G . (GS,i)),y) is Element of the carrier of G
[( the multF of G . (GS,i)),y] is set
{( the multF of G . (GS,i)),y} is non empty set
{( the multF of G . (GS,i))} is non empty trivial V43(1) set
{{( the multF of G . (GS,i)),y},{( the multF of G . (GS,i))}} is non empty set
the multF of G . [( the multF of G . (GS,i)),y] is set
the multF of G . (i,y) is Element of the carrier of G
the multF of G . (GS,( the multF of G . (i,y))) is Element of the carrier of G
[GS,( the multF of G . (i,y))] is set
{GS,( the multF of G . (i,y))} is non empty set
{{GS,( the multF of G . (i,y))},{GS}} is non empty set
the multF of G . [GS,( the multF of G . (i,y))] is set
i * y is Element of the carrier of G
GS * (i * y) is Element of the carrier of G
the multF of G . (GS,(i * y)) is Element of the carrier of G
[GS,(i * y)] is set
{GS,(i * y)} is non empty set
{{GS,(i * y)},{GS}} is non empty set
the multF of G . [GS,(i * y)] is set
GS * i is Element of the carrier of G
the multF of G . (GS,i) is Element of the carrier of G
(GS * i) * y is Element of the carrier of G
the multF of G . ((GS * i),y) is Element of the carrier of G
[(GS * i),y] is set
{(GS * i),y} is non empty set
{(GS * i)} is non empty trivial V43(1) set
{{(GS * i),y},{(GS * i)}} is non empty set
the multF of G . [(GS * i),y] is set
the multF of G . (( the multF of G . (GS,i)),y) is Element of the carrier of G
[( the multF of G . (GS,i)),y] is set
{( the multF of G . (GS,i)),y} is non empty set
{( the multF of G . (GS,i))} is non empty trivial V43(1) set
{{( the multF of G . (GS,i)),y},{( the multF of G . (GS,i))}} is non empty set
the multF of G . [( the multF of G . (GS,i)),y] is set
G is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V118() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of G is non empty non trivial set
0. G is V65(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
GS is Element of the carrier of G
the addF of G . ((0. G),GS) is Element of the carrier of G
[(0. G),GS] is set
{(0. G),GS} is non empty set
{(0. G)} is non empty trivial V43(1) set
{{(0. G),GS},{(0. G)}} is non empty set
the addF of G . [(0. G),GS] is set
GS + (0. G) is Element of the carrier of G
the addF of G . (GS,(0. G)) is Element of the carrier of G
[GS,(0. G)] is set
{GS,(0. G)} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,(0. G)},{GS}} is non empty set
the addF of G . [GS,(0. G)] is set
G is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V118() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of G is non empty non trivial set
1_ G is Element of the carrier of G
1. G is V65(G) Element of the carrier of G
the OneF of G is Element of the carrier of G
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
GS is Element of the carrier of G
the multF of G . ((1_ G),GS) is Element of the carrier of G
[(1_ G),GS] is set
{(1_ G),GS} is non empty set
{(1_ G)} is non empty trivial V43(1) set
{{(1_ G),GS},{(1_ G)}} is non empty set
the multF of G . [(1_ G),GS] is set
(1_ G) * GS is Element of the carrier of G
the multF of G . (GS,(1_ G)) is Element of the carrier of G
[GS,(1_ G)] is set
{GS,(1_ G)} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,(1_ G)},{GS}} is non empty set
the multF of G . [GS,(1_ G)] is set
GS * (1_ G) is Element of the carrier of G
G is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V118() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of G is non empty non trivial set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
GS is Element of the carrier of G
i is Element of the carrier of G
y is Element of the carrier of G
the addF of G . (i,y) is Element of the carrier of G
[i,y] is set
{i,y} is non empty set
{i} is non empty trivial V43(1) set
{{i,y},{i}} is non empty set
the addF of G . [i,y] is set
the multF of G . (GS,( the addF of G . (i,y))) is Element of the carrier of G
[GS,( the addF of G . (i,y))] is set
{GS,( the addF of G . (i,y))} is non empty set
{GS} is non empty trivial V43(1) set
{{GS,( the addF of G . (i,y))},{GS}} is non empty set
the multF of G . [GS,( the addF of G . (i,y))] is set
i + y is Element of the carrier of G
GS * (i + y) is Element of the carrier of G
the multF of G . (GS,(i + y)) is Element of the carrier of G
[GS,(i + y)] is set
{GS,(i + y)} is non empty set
{{GS,(i + y)},{GS}} is non empty set
the multF of G . [GS,(i + y)] is set
GS * i is Element of the carrier of G
the multF of G . (GS,i) is Element of the carrier of G
[GS,i] is set
{GS,i} is non empty set
{{GS,i},{GS}} is non empty set
the multF of G . [GS,i] is set
GS * y is Element of the carrier of G
the multF of G . (GS,y) is Element of the carrier of G
[GS,y] is set
{GS,y} is non empty set
{{GS,y},{GS}} is non empty set
the multF of G . [GS,y] is set
(GS * i) + (GS * y) is Element of the carrier of G
the addF of G . ((GS * i),(GS * y)) is Element of the carrier of G
[(GS * i),(GS * y)] is set
{(GS * i),(GS * y)} is non empty set
{(GS * i)} is non empty trivial V43(1) set
{{(GS * i),(GS * y)},{(GS * i)}} is non empty set
the addF of G . [(GS * i),(GS * y)] is set
the addF of G . (( the multF of G . (GS,i)),( the multF of G . (GS,y))) is Element of the carrier of G
[( the multF of G . (GS,i)),( the multF of G . (GS,y))] is set
{( the multF of G . (GS,i)),( the multF of G . (GS,y))} is non empty set
{( the multF of G . (GS,i))} is non empty trivial V43(1) set
{{( the multF of G . (GS,i)),( the multF of G . (GS,y))},{( the multF of G . (GS,i))}} is non empty set
the addF of G . [( the multF of G . (GS,i)),( the multF of G . (GS,y))] is set
the addF of G . (GS,i) is Element of the carrier of G
the addF of G . [GS,i] is set
the multF of G . (( the addF of G . (GS,i)),y) is Element of the carrier of G
[( the addF of G . (GS,i)),y] is set
{( the addF of G . (GS,i)),y} is non empty set
{( the addF of G . (GS,i))} is non empty trivial V43(1) set
{{( the addF of G . (GS,i)),y},{( the addF of G . (GS,i))}} is non empty set
the multF of G . [( the addF of G . (GS,i)),y] is set
GS + i is Element of the carrier of G
(GS + i) * y is Element of the carrier of G
the multF of G . ((GS + i),y) is Element of the carrier of G
[(GS + i),y] is set
{(GS + i),y} is non empty set
{(GS + i)} is non empty trivial V43(1) set
{{(GS + i),y},{(GS + i)}} is non empty set
the multF of G . [(GS + i),y] is set
i * y is Element of the carrier of G
the multF of G . (i,y) is Element of the carrier of G
the multF of G . [i,y] is set
(GS * y) + (i * y) is Element of the carrier of G
the addF of G . ((GS * y),(i * y)) is Element of the carrier of G
[(GS * y),(i * y)] is set
{(GS * y),(i * y)} is non empty set
{(GS * y)} is non empty trivial V43(1) set
{{(GS * y),(i * y)},{(GS * y)}} is non empty set
the addF of G . [(GS * y),(i * y)] is set
the addF of G . (( the multF of G . (GS,y)),( the multF of G . (i,y))) is Element of the carrier of G
[( the multF of G . (GS,y)),( the multF of G . (i,y))] is set
{( the multF of G . (GS,y)),( the multF of G . (i,y))} is non empty set
{( the multF of G . (GS,y))} is non empty trivial V43(1) set
{{( the multF of G . (GS,y)),( the multF of G . (i,y))},{( the multF of G . (GS,y))}} is non empty set
the addF of G . [( the multF of G . (GS,y)),( the multF of G . (i,y))] is set
G is non empty set
[:G,G:] is Relation-like set
[:[:G,G:],G:] is Relation-like set
bool [:[:G,G:],G:] is set
GS is V29() V30() V31() V35() V36() V41() countable set
GS -tuples_on G is functional non empty FinSequence-membered FinSequenceSet of G
i is Relation-like [:G,G:] -defined G -valued Function-like total V18([:G,G:],G) Element of bool [:[:G,G:],G:]
y is Relation-like NAT -defined G -valued Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on G
i is Relation-like NAT -defined G -valued Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on G
i .: (y,i) is set
G is non empty set
[:G,G:] is Relation-like set
[:[:G,G:],G:] is Relation-like set
bool [:[:G,G:],G:] is set
i is V29() V30() V31() V35() V36() V41() countable set
i -tuples_on G is functional non empty FinSequence-membered FinSequenceSet of G
[:(i -tuples_on G),(i -tuples_on G):] is Relation-like set
[:[:(i -tuples_on G),(i -tuples_on G):],(i -tuples_on G):] is Relation-like set
bool [:[:(i -tuples_on G),(i -tuples_on G):],(i -tuples_on G):] is set
GS is Relation-like [:G,G:] -defined G -valued Function-like total V18([:G,G:],G) Element of bool [:[:G,G:],G:]
y is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
x is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
(G,i,GS,x,i) is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
y is Relation-like [:(i -tuples_on G),(i -tuples_on G):] -defined i -tuples_on G -valued Function-like total V18([:(i -tuples_on G),(i -tuples_on G):],i -tuples_on G) Element of bool [:[:(i -tuples_on G),(i -tuples_on G):],(i -tuples_on G):]
i is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
x is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
y . (i,x) is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
[i,x] is set
{i,x} is functional non empty set
{i} is functional non empty trivial V43(1) with_common_domain set
{{i,x},{i}} is non empty set
y . [i,x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,i,GS,i,x) is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
y . (i,i) is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
[i,i] is set
{i,i} is functional non empty set
{i} is functional non empty trivial V43(1) with_common_domain set
{{i,i},{i}} is non empty set
y . [i,i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
i is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
c10 is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
(G,i,GS,i,c10) is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
y is Relation-like [:(i -tuples_on G),(i -tuples_on G):] -defined i -tuples_on G -valued Function-like total V18([:(i -tuples_on G),(i -tuples_on G):],i -tuples_on G) Element of bool [:[:(i -tuples_on G),(i -tuples_on G):],(i -tuples_on G):]
i is Relation-like [:(i -tuples_on G),(i -tuples_on G):] -defined i -tuples_on G -valued Function-like total V18([:(i -tuples_on G),(i -tuples_on G):],i -tuples_on G) Element of bool [:[:(i -tuples_on G),(i -tuples_on G):],(i -tuples_on G):]
x is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
y . (x,i) is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
[x,i] is set
{x,i} is functional non empty set
{x} is functional non empty trivial V43(1) with_common_domain set
{{x,i},{x}} is non empty set
y . [x,i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,i,GS,x,i) is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i . (x,i) is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i . [x,i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
G is non empty set
[:G,G:] is Relation-like set
bool [:G,G:] is set
i is V29() V30() V31() V35() V36() V41() countable set
i -tuples_on G is functional non empty FinSequence-membered FinSequenceSet of G
[:(i -tuples_on G),(i -tuples_on G):] is Relation-like set
bool [:(i -tuples_on G),(i -tuples_on G):] is set
GS is Relation-like G -defined G -valued Function-like non empty total V18(G,G) Element of bool [:G,G:]
y is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
GS * i is Relation-like NAT -defined G -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of G
x is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
y is Relation-like i -tuples_on G -defined i -tuples_on G -valued Function-like non empty total V18(i -tuples_on G,i -tuples_on G) Element of bool [:(i -tuples_on G),(i -tuples_on G):]
i is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
y . i is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
GS * i is Relation-like NAT -defined G -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of G
x is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
y . x is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
i is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
GS * i is Relation-like NAT -defined G -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of G
y is Relation-like i -tuples_on G -defined i -tuples_on G -valued Function-like non empty total V18(i -tuples_on G,i -tuples_on G) Element of bool [:(i -tuples_on G),(i -tuples_on G):]
i is Relation-like i -tuples_on G -defined i -tuples_on G -valued Function-like non empty total V18(i -tuples_on G,i -tuples_on G) Element of bool [:(i -tuples_on G),(i -tuples_on G):]
x is Relation-like NAT -defined G -valued Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
y . x is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
GS * x is Relation-like NAT -defined G -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of G
i . x is Relation-like NAT -defined Function-like V36() V43(i) countable FinSequence-like FinSubsequence-like Element of i -tuples_on G
G is V29() V30() V31() V35() V36() V41() countable set
GS is non empty set
[:GS,GS:] is Relation-like set
[:[:GS,GS:],GS:] is Relation-like set
bool [:[:GS,GS:],GS:] is set
G -tuples_on GS is functional non empty FinSequence-membered FinSequenceSet of GS
i is Relation-like [:GS,GS:] -defined GS -valued Function-like total V18([:GS,GS:],GS) Element of bool [:[:GS,GS:],GS:]
(GS,i,G) is Relation-like [:(G -tuples_on GS),(G -tuples_on GS):] -defined G -tuples_on GS -valued Function-like total V18([:(G -tuples_on GS),(G -tuples_on GS):],G -tuples_on GS) Element of bool [:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):]
[:(G -tuples_on GS),(G -tuples_on GS):] is Relation-like set
[:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):] is Relation-like set
bool [:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):] is set
y is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
i is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,i,G) . (y,i) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[y,i] is set
{y,i} is functional non empty set
{y} is functional non empty trivial V43(1) with_common_domain set
{{y,i},{y}} is non empty set
(GS,i,G) . [y,i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(GS,G,i,y,i) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,G,i,i,y) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,i,G) . (i,y) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[i,y] is set
{i,y} is functional non empty set
{i} is functional non empty trivial V43(1) with_common_domain set
{{i,y},{i}} is non empty set
(GS,i,G) . [i,y] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
G is V29() V30() V31() V35() V36() V41() countable set
GS is non empty set
[:GS,GS:] is Relation-like set
[:[:GS,GS:],GS:] is Relation-like set
bool [:[:GS,GS:],GS:] is set
G -tuples_on GS is functional non empty FinSequence-membered FinSequenceSet of GS
i is Relation-like [:GS,GS:] -defined GS -valued Function-like total V18([:GS,GS:],GS) Element of bool [:[:GS,GS:],GS:]
(GS,i,G) is Relation-like [:(G -tuples_on GS),(G -tuples_on GS):] -defined G -tuples_on GS -valued Function-like total V18([:(G -tuples_on GS),(G -tuples_on GS):],G -tuples_on GS) Element of bool [:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):]
[:(G -tuples_on GS),(G -tuples_on GS):] is Relation-like set
[:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):] is Relation-like set
bool [:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):] is set
y is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
i is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,i,G) . (y,i) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[y,i] is set
{y,i} is functional non empty set
{y} is functional non empty trivial V43(1) with_common_domain set
{{y,i},{y}} is non empty set
(GS,i,G) . [y,i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,i,G) . (((GS,i,G) . (y,i)),x) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[((GS,i,G) . (y,i)),x] is set
{((GS,i,G) . (y,i)),x} is functional non empty set
{((GS,i,G) . (y,i))} is functional non empty trivial V43(1) with_common_domain set
{{((GS,i,G) . (y,i)),x},{((GS,i,G) . (y,i))}} is non empty set
(GS,i,G) . [((GS,i,G) . (y,i)),x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(GS,G,i,y,i) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,i,G) . ((GS,G,i,y,i),x) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[(GS,G,i,y,i),x] is set
{(GS,G,i,y,i),x} is functional non empty set
{(GS,G,i,y,i)} is functional non empty trivial V43(1) with_common_domain set
{{(GS,G,i,y,i),x},{(GS,G,i,y,i)}} is non empty set
(GS,i,G) . [(GS,G,i,y,i),x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(GS,G,i,(GS,G,i,y,i),x) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,G,i,i,x) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,G,i,y,(GS,G,i,i,x)) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,i,G) . (y,(GS,G,i,i,x)) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[y,(GS,G,i,i,x)] is set
{y,(GS,G,i,i,x)} is functional non empty set
{{y,(GS,G,i,i,x)},{y}} is non empty set
(GS,i,G) . [y,(GS,G,i,i,x)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(GS,i,G) . (i,x) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[i,x] is set
{i,x} is functional non empty set
{i} is functional non empty trivial V43(1) with_common_domain set
{{i,x},{i}} is non empty set
(GS,i,G) . [i,x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(GS,i,G) . (y,((GS,i,G) . (i,x))) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[y,((GS,i,G) . (i,x))] is set
{y,((GS,i,G) . (i,x))} is functional non empty set
{{y,((GS,i,G) . (i,x))},{y}} is non empty set
(GS,i,G) . [y,((GS,i,G) . (i,x))] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
G is V29() V30() V31() V35() V36() V41() countable set
GS is non empty set
[:GS,GS:] is Relation-like set
[:[:GS,GS:],GS:] is Relation-like set
bool [:[:GS,GS:],GS:] is set
G -tuples_on GS is functional non empty FinSequence-membered FinSequenceSet of GS
i is Element of GS
G |-> i is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
y is Relation-like [:GS,GS:] -defined GS -valued Function-like total V18([:GS,GS:],GS) Element of bool [:[:GS,GS:],GS:]
(GS,y,G) is Relation-like [:(G -tuples_on GS),(G -tuples_on GS):] -defined G -tuples_on GS -valued Function-like total V18([:(G -tuples_on GS),(G -tuples_on GS):],G -tuples_on GS) Element of bool [:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):]
[:(G -tuples_on GS),(G -tuples_on GS):] is Relation-like set
[:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):] is Relation-like set
bool [:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):] is set
the_unity_wrt y is Element of GS
i is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,y,G) . ((G |-> i),i) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[(G |-> i),i] is set
{(G |-> i),i} is functional non empty set
{(G |-> i)} is functional non empty trivial V43(1) with_common_domain set
{{(G |-> i),i},{(G |-> i)}} is non empty set
(GS,y,G) . [(G |-> i),i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,G,y,(G |-> i),x) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,y,G) . (i,(G |-> i)) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[i,(G |-> i)] is set
{i,(G |-> i)} is functional non empty set
{i} is functional non empty trivial V43(1) with_common_domain set
{{i,(G |-> i)},{i}} is non empty set
(GS,y,G) . [i,(G |-> i)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(GS,G,y,x,(G |-> i)) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
G is V29() V30() V31() V35() V36() V41() countable set
GS is non empty set
[:GS,GS:] is Relation-like set
[:[:GS,GS:],GS:] is Relation-like set
bool [:[:GS,GS:],GS:] is set
bool [:GS,GS:] is set
G -tuples_on GS is functional non empty FinSequence-membered FinSequenceSet of GS
i is Relation-like [:GS,GS:] -defined GS -valued Function-like total V18([:GS,GS:],GS) Element of bool [:[:GS,GS:],GS:]
(GS,i,G) is Relation-like [:(G -tuples_on GS),(G -tuples_on GS):] -defined G -tuples_on GS -valued Function-like total V18([:(G -tuples_on GS),(G -tuples_on GS):],G -tuples_on GS) Element of bool [:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):]
[:(G -tuples_on GS),(G -tuples_on GS):] is Relation-like set
[:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):] is Relation-like set
bool [:[:(G -tuples_on GS),(G -tuples_on GS):],(G -tuples_on GS):] is set
y is Relation-like GS -defined GS -valued Function-like non empty total V18(GS,GS) Element of bool [:GS,GS:]
(GS,y,G) is Relation-like G -tuples_on GS -defined G -tuples_on GS -valued Function-like non empty total V18(G -tuples_on GS,G -tuples_on GS) Element of bool [:(G -tuples_on GS),(G -tuples_on GS):]
bool [:(G -tuples_on GS),(G -tuples_on GS):] is set
the_inverseOp_wrt i is Relation-like GS -defined GS -valued Function-like non empty total V18(GS,GS) Element of bool [:GS,GS:]
i is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
x is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
y * x is Relation-like NAT -defined GS -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of GS
(GS,y,G) . i is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,i,G) . (i,((GS,y,G) . i)) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[i,((GS,y,G) . i)] is set
{i,((GS,y,G) . i)} is functional non empty set
{i} is functional non empty trivial V43(1) with_common_domain set
{{i,((GS,y,G) . i)},{i}} is non empty set
(GS,i,G) . [i,((GS,y,G) . i)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(GS,i,G) . (x,(y * x)) is set
[x,(y * x)] is set
{x,(y * x)} is functional non empty set
{x} is functional non empty trivial V43(1) with_common_domain set
{{x,(y * x)},{x}} is non empty set
(GS,i,G) . [x,(y * x)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
i is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,G,i,x,i) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
the_unity_wrt i is Element of GS
G |-> (the_unity_wrt i) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
(GS,i,G) . (((GS,y,G) . i),i) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
[((GS,y,G) . i),i] is set
{((GS,y,G) . i),i} is functional non empty set
{((GS,y,G) . i)} is functional non empty trivial V43(1) with_common_domain set
{{((GS,y,G) . i),i},{((GS,y,G) . i)}} is non empty set
(GS,i,G) . [((GS,y,G) . i),i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(GS,i,G) . ((y * x),x) is set
[(y * x),x] is set
{(y * x),x} is functional non empty set
{(y * x)} is functional non empty trivial V43(1) with_common_domain set
{{(y * x),x},{(y * x)}} is non empty set
(GS,i,G) . [(y * x),x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(GS,G,i,i,x) is Relation-like NAT -defined GS -valued Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
i is Element of GS
the_unity_wrt (GS,i,G) is Relation-like NAT -defined Function-like V36() V43(G) countable FinSequence-like FinSubsequence-like Element of G -tuples_on GS
G is non empty addLoopStr
GS is V29() V30() V31() V35() V36() V41() countable set
the carrier of G is non empty set
GS -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet of the carrier of G
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
( the carrier of G, the addF of G,GS) is Relation-like [:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):] -defined GS -tuples_on the carrier of G -valued Function-like total V18([:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):],GS -tuples_on the carrier of G) Element of bool [:[:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):]
[:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):] is Relation-like set
[:[:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):] is Relation-like set
bool [:[:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):] is set
0. G is V65(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
GS |-> (0. G) is Relation-like NAT -defined the carrier of G -valued Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
addLoopStr(# (GS -tuples_on the carrier of G),( the carrier of G, the addF of G,GS),(GS |-> (0. G)) #) is strict addLoopStr
y is non empty addLoopStr
comp G is Relation-like the carrier of G -defined the carrier of G -valued Function-like non empty total V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
bool [: the carrier of G, the carrier of G:] is set
the carrier of y is non empty set
i is Element of the carrier of y
( the carrier of G,(comp G),GS) is Relation-like GS -tuples_on the carrier of G -defined GS -tuples_on the carrier of G -valued Function-like non empty total V18(GS -tuples_on the carrier of G,GS -tuples_on the carrier of G) Element of bool [:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):]
bool [:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):] is set
( the carrier of G,(comp G),GS) . i is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
i is Element of the carrier of y
i + i is Element of the carrier of y
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like total V18([: the carrier of y, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is Relation-like set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is Relation-like set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is set
the addF of y . (i,i) is Element of the carrier of y
[i,i] is set
{i,i} is non empty set
{i} is non empty trivial V43(1) set
{{i,i},{i}} is non empty set
the addF of y . [i,i] is set
0. y is V65(y) Element of the carrier of y
the ZeroF of y is Element of the carrier of y
the_unity_wrt ( the carrier of G, the addF of G,GS) is Relation-like NAT -defined Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
0. y is V65(y) Element of the carrier of y
the carrier of y is non empty set
the ZeroF of y is Element of the carrier of y
G is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
GS is V29() V30() V31() V35() V36() V41() countable set
(G,GS) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr
G is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V118() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of G is non empty non trivial set
GS is V29() V30() V31() V35() V36() V41() countable set
GS -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet of the carrier of G
[: the carrier of G,(GS -tuples_on the carrier of G):] is Relation-like set
[:[: the carrier of G,(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):] is Relation-like set
bool [:[: the carrier of G,(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):] is set
the multF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
i is set
y is set
i is set
[y,i] is set
{y,i} is non empty set
{y} is non empty trivial V43(1) set
{{y,i},{y}} is non empty set
i is Element of the carrier of G
x is Relation-like NAT -defined the carrier of G -valued Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
the multF of G [;] (i,x) is Relation-like NAT -defined the carrier of G -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of the carrier of G
i is Relation-like NAT -defined the carrier of G -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of the carrier of G
[i,x] is set
{i,x} is non empty set
{i} is non empty trivial V43(1) set
{{i,x},{i}} is non empty set
i is Relation-like [: the carrier of G,(GS -tuples_on the carrier of G):] -defined GS -tuples_on the carrier of G -valued Function-like total V18([: the carrier of G,(GS -tuples_on the carrier of G):],GS -tuples_on the carrier of G) Element of bool [:[: the carrier of G,(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):]
y is Element of the carrier of G
i is Relation-like NAT -defined the carrier of G -valued Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
i . (y,i) is Relation-like NAT -defined Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
[y,i] is set
{y,i} is non empty set
{y} is non empty trivial V43(1) set
{{y,i},{y}} is non empty set
i . [y,i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
the multF of G [;] (y,i) is Relation-like NAT -defined the carrier of G -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of the carrier of G
x is Element of the carrier of G
i is Relation-like NAT -defined the carrier of G -valued Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
[x,i] is set
{x,i} is non empty set
{x} is non empty trivial V43(1) set
{{x,i},{x}} is non empty set
the multF of G [;] (x,i) is Relation-like NAT -defined the carrier of G -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of the carrier of G
i is Relation-like [: the carrier of G,(GS -tuples_on the carrier of G):] -defined GS -tuples_on the carrier of G -valued Function-like total V18([: the carrier of G,(GS -tuples_on the carrier of G):],GS -tuples_on the carrier of G) Element of bool [:[: the carrier of G,(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):]
y is Relation-like [: the carrier of G,(GS -tuples_on the carrier of G):] -defined GS -tuples_on the carrier of G -valued Function-like total V18([: the carrier of G,(GS -tuples_on the carrier of G):],GS -tuples_on the carrier of G) Element of bool [:[: the carrier of G,(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):]
i is Element of the carrier of G
x is Relation-like NAT -defined the carrier of G -valued Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
i . (i,x) is Relation-like NAT -defined Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
[i,x] is set
{i,x} is non empty set
{i} is non empty trivial V43(1) set
{{i,x},{i}} is non empty set
i . [i,x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
the multF of G [;] (i,x) is Relation-like NAT -defined the carrier of G -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of the carrier of G
y . (i,x) is Relation-like NAT -defined Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
y . [i,x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
G is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital V118() left_unital Abelian add-associative right_zeroed doubleLoopStr
GS is V29() V30() V31() V35() V36() V41() countable set
(G,GS) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr
(G,GS) is Relation-like [: the carrier of G,(GS -tuples_on the carrier of G):] -defined GS -tuples_on the carrier of G -valued Function-like total V18([: the carrier of G,(GS -tuples_on the carrier of G):],GS -tuples_on the carrier of G) Element of bool [:[: the carrier of G,(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):]
the carrier of G is non empty non trivial set
GS -tuples_on the carrier of G is functional non empty FinSequence-membered FinSequenceSet of the carrier of G
[: the carrier of G,(GS -tuples_on the carrier of G):] is Relation-like set
[:[: the carrier of G,(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):] is Relation-like set
bool [:[: the carrier of G,(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):] is set
the addF of G is Relation-like [: the carrier of G, the carrier of G:] -defined the carrier of G -valued Function-like total V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is Relation-like set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is Relation-like set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
( the carrier of G, the addF of G,GS) is Relation-like [:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):] -defined GS -tuples_on the carrier of G -valued Function-like total V18([:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):],GS -tuples_on the carrier of G) Element of bool [:[:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):]
[:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):] is Relation-like set
[:[:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):] is Relation-like set
bool [:[:(GS -tuples_on the carrier of G),(GS -tuples_on the carrier of G):],(GS -tuples_on the carrier of G):] is set
0. G is V65(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
GS |-> (0. G) is Relation-like NAT -defined the carrier of G -valued Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
addLoopStr(# (GS -tuples_on the carrier of G),( the carrier of G, the addF of G,GS),(GS |-> (0. G)) #) is strict addLoopStr
the carrier of (G,GS) is non empty set
[: the carrier of G, the carrier of (G,GS):] is Relation-like set
[:[: the carrier of G, the carrier of (G,GS):], the carrier of (G,GS):] is Relation-like set
bool [:[: the carrier of G, the carrier of (G,GS):], the carrier of (G,GS):] is set
the addF of (G,GS) is Relation-like [: the carrier of (G,GS), the carrier of (G,GS):] -defined the carrier of (G,GS) -valued Function-like total V18([: the carrier of (G,GS), the carrier of (G,GS):], the carrier of (G,GS)) Element of bool [:[: the carrier of (G,GS), the carrier of (G,GS):], the carrier of (G,GS):]
[: the carrier of (G,GS), the carrier of (G,GS):] is Relation-like set
[:[: the carrier of (G,GS), the carrier of (G,GS):], the carrier of (G,GS):] is Relation-like set
bool [:[: the carrier of (G,GS), the carrier of (G,GS):], the carrier of (G,GS):] is set
0. (G,GS) is V65((G,GS)) Element of the carrier of (G,GS)
the ZeroF of (G,GS) is Element of the carrier of (G,GS)
i is Relation-like [: the carrier of G, the carrier of (G,GS):] -defined the carrier of (G,GS) -valued Function-like total V18([: the carrier of G, the carrier of (G,GS):], the carrier of (G,GS)) Element of bool [:[: the carrier of G, the carrier of (G,GS):], the carrier of (G,GS):]
VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #) is strict VectSpStr over G
the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #) is set
the addF of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #) is Relation-like [: the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #), the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):] -defined the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #) -valued Function-like V18([: the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #), the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):], the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #)) Element of bool [:[: the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #), the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):], the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):]
[: the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #), the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):] is Relation-like set
[:[: the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #), the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):], the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):] is Relation-like set
bool [:[: the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #), the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):], the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):] is set
the ZeroF of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #) is Element of the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #)
addLoopStr(# the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #), the addF of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #), the ZeroF of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #) #) is strict addLoopStr
the lmult of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #) is Relation-like [: the carrier of G, the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):] -defined the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #) -valued Function-like V18([: the carrier of G, the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):], the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #)) Element of bool [:[: the carrier of G, the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):], the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):]
[: the carrier of G, the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):] is Relation-like set
[:[: the carrier of G, the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):], the carrier of VectSpStr(# H1((G,GS)),H2((G,GS)),H4((G,GS)),i #):] is Relation-like set
bool [:[: the carrier of G, the