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 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
i is strict VectSpStr over G
the carrier of i is set
the addF of i is Relation-like [: the carrier of i, the carrier of i:] -defined the carrier of i -valued Function-like V18([: the carrier of i, the carrier of i:], the carrier of i) Element of bool [:[: the carrier of i, the carrier of i:], the carrier of i:]
[: the carrier of i, the carrier of i:] is Relation-like set
[:[: the carrier of i, the carrier of i:], the carrier of i:] is Relation-like set
bool [:[: the carrier of i, the carrier of i:], the carrier of i:] is set
the ZeroF of i is Element of the carrier of i
addLoopStr(# the carrier of i, the addF of i, the ZeroF of i #) is strict addLoopStr
the lmult of i is Relation-like [: the carrier of G, the carrier of i:] -defined the carrier of i -valued Function-like V18([: the carrier of G, the carrier of i:], the carrier of i) Element of bool [:[: the carrier of G, the carrier of i:], the carrier of i:]
[: the carrier of G, the carrier of i:] is Relation-like set
[:[: the carrier of G, the carrier of i:], the carrier of i:] is Relation-like set
bool [:[: the carrier of G, the carrier of i:], the carrier of i:] is set
y is strict VectSpStr over G
the carrier of y is set
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like 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 ZeroF of y is Element of the carrier of y
addLoopStr(# the carrier of y, the addF of y, the ZeroF of y #) is strict addLoopStr
the lmult of y is Relation-like [: the carrier of G, the carrier of y:] -defined the carrier of y -valued Function-like V18([: the carrier of G, the carrier of y:], the carrier of y) Element of bool [:[: the carrier of G, the carrier of y:], the carrier of y:]
[: the carrier of G, the carrier of y:] is Relation-like set
[:[: the carrier of G, the carrier of y:], the carrier of y:] is Relation-like set
bool [:[: the carrier of G, the carrier of y:], the carrier of 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
GS is V29() V30() V31() V35() V36() V41() countable set
(G,GS) is strict VectSpStr over G
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 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
the ZeroF of (G,GS) is Element of the carrier of (G,GS)
addLoopStr(# the carrier of (G,GS), the addF of (G,GS), the ZeroF of (G,GS) #) is strict addLoopStr
(G,GS) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr
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:]
y is Relation-like [:GS,GS:] -defined GS -valued Function-like total V18([:GS,GS:],GS) Element of bool [:[:GS,GS:],GS:]
i is Element of 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
i [;] (i,x) is Relation-like NAT -defined GS -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of 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,G,y,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
i [;] (i,(GS,G,y,x,i)) is Relation-like NAT -defined GS -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of GS
i [;] (i,i) is Relation-like NAT -defined GS -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of GS
y .: ((i [;] (i,x)),(i [;] (i,i))) is Relation-like NAT -defined GS -valued Function-like V36() countable FinSequence-like FinSubsequence-like FinSequence of GS
<:x,i:> is Relation-like Function-like set
<:x,i:> * y is Relation-like GS -valued Function-like set
i [;] (i,(<:x,i:> * y)) is set
dom (<:x,i:> * y) is set
(dom (<:x,i:> * y)) --> i is Relation-like dom (<:x,i:> * y) -defined GS -valued Function-like total V18( dom (<:x,i:> * y),GS) Element of bool [:(dom (<:x,i:> * y)),GS:]
[:(dom (<:x,i:> * y)),GS:] is Relation-like set
bool [:(dom (<:x,i:> * y)),GS:] is set
<:((dom (<:x,i:> * y)) --> i),(<:x,i:> * y):> is Relation-like Function-like set
<:((dom (<:x,i:> * y)) --> i),(<:x,i:> * y):> * i is Relation-like GS -valued Function-like set
dom x is V43(G) countable Element of bool NAT
(dom x) --> i is Relation-like dom x -defined GS -valued Function-like total V18( dom x,GS) Element of bool [:(dom x),GS:]
[:(dom x),GS:] is Relation-like set
bool [:(dom x),GS:] is set
<:((dom x) --> i),x:> is Relation-like Function-like set
<:((dom x) --> i),x:> * i is Relation-like GS -valued Function-like set
rng (<:((dom x) --> i),x:> * i) is set
rng i is set
dom i is V43(G) countable Element of bool NAT
(dom i) --> i is Relation-like dom i -defined GS -valued Function-like total V18( dom i,GS) Element of bool [:(dom i),GS:]
[:(dom i),GS:] is Relation-like set
bool [:(dom i),GS:] is set
<:((dom i) --> i),i:> is Relation-like Function-like set
<:((dom i) --> i),i:> * i is Relation-like GS -valued Function-like set
rng (<:((dom i) --> i),i:> * i) is set
<:(<:((dom x) --> i),x:> * i),(<:((dom i) --> i),i:> * i):> is Relation-like Function-like set
rng <:(<:((dom x) --> i),x:> * i),(<:((dom i) --> i),i:> * i):> is set
[:(rng (<:((dom x) --> i),x:> * i)),(rng (<:((dom i) --> i),i:> * i)):] is Relation-like set
[:(rng i),(rng i):] is Relation-like set
dom y is Relation-like set
len i is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len i) is V36() V43( len i) countable Element of bool NAT
Seg G is V36() V43(G) countable Element of bool NAT
rng x is set
rng i is set
[:(rng x),(rng i):] is Relation-like set
rng <:x,i:> is set
dom ((dom i) --> i) is set
len x is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len x) is V36() V43( len x) countable Element of bool NAT
dom <:x,i:> is set
dom ((dom (<:x,i:> * y)) --> i) is set
dom <:((dom (<:x,i:> * y)) --> i),(<:x,i:> * y):> is set
rng <:((dom i) --> i),i:> is set
rng ((dom i) --> i) is set
[:(rng ((dom i) --> i)),(rng i):] is Relation-like set
[:(rng ((dom i) --> i)),GS:] is Relation-like set
{i} is non empty trivial V43(1) set
[:{i},GS:] is Relation-like set
rng <:((dom x) --> i),x:> is set
rng ((dom x) --> i) is set
[:(rng ((dom x) --> i)),(rng x):] is Relation-like set
[:(rng ((dom x) --> i)),GS:] is Relation-like set
dom ((dom x) --> i) is set
rng ((dom (<:x,i:> * y)) --> i) is set
dom i is Relation-like set
dom (<:((dom i) --> i),i:> * i) is set
dom <:((dom i) --> i),i:> is set
y .: ((<:((dom x) --> i),x:> * i),(i [;] (i,i))) is set
y .: ((<:((dom x) --> i),x:> * i),(<:((dom i) --> i),i:> * i)) is set
<:(<:((dom x) --> i),x:> * i),(<:((dom i) --> i),i:> * i):> * y is Relation-like GS -valued Function-like set
dom (<:((dom x) --> i),x:> * i) is set
dom <:((dom x) --> i),x:> is set
dom <:(<:((dom x) --> i),x:> * i),(<:((dom i) --> i),i:> * i):> is set
dom (<:(<:((dom x) --> i),x:> * i),(<:((dom i) --> i),i:> * i):> * y) is set
rng (<:x,i:> * y) is set
rng <:((dom (<:x,i:> * y)) --> i),(<:x,i:> * y):> is set
[:(rng ((dom (<:x,i:> * y)) --> i)),(rng (<:x,i:> * y)):] is Relation-like set
dom (<:((dom (<:x,i:> * y)) --> i),(<:x,i:> * y):> * i) is set
i is set
(i [;] (i,(GS,G,y,x,i))) . i is set
(y .: ((i [;] (i,x)),(i [;] (i,i)))) . i is set
dom (GS,G,y,x,i) is V43(G) countable Element of bool NAT
(dom (GS,G,y,x,i)) --> i is Relation-like dom (GS,G,y,x,i) -defined GS -valued Function-like total V18( dom (GS,G,y,x,i),GS) Element of bool [:(dom (GS,G,y,x,i)),GS:]
[:(dom (GS,G,y,x,i)),GS:] is Relation-like set
bool [:(dom (GS,G,y,x,i)),GS:] is set
<:((dom (GS,G,y,x,i)) --> i),(GS,G,y,x,i):> is Relation-like Function-like set
dom <:((dom (GS,G,y,x,i)) --> i),(GS,G,y,x,i):> is set
dom ((dom (GS,G,y,x,i)) --> i) is set
(dom ((dom (GS,G,y,x,i)) --> i)) /\ (dom (GS,G,y,x,i)) is countable Element of bool NAT
<:((dom (GS,G,y,x,i)) --> i),(GS,G,y,x,i):> * i is Relation-like GS -valued Function-like set
dom (<:((dom (GS,G,y,x,i)) --> i),(GS,G,y,x,i):> * i) is set
x . i is set
dom (i [;] (i,x)) is countable Element of bool NAT
i . i is set
dom (i [;] (i,i)) is countable Element of bool NAT
(GS,G,y,x,i) . i is set
i . (i,((GS,G,y,x,i) . i)) is set
[i,((GS,G,y,x,i) . i)] is set
{i,((GS,G,y,x,i) . i)} is non empty set
{{i,((GS,G,y,x,i) . i)},{i}} is non empty set
i . [i,((GS,G,y,x,i) . i)] is set
y . ((x . i),(i . i)) is set
[(x . i),(i . i)] is set
{(x . i),(i . i)} is non empty set
{(x . i)} is non empty trivial V43(1) set
{{(x . i),(i . i)},{(x . i)}} is non empty set
y . [(x . i),(i . i)] is set
i . (i,(y . ((x . i),(i . i)))) is set
[i,(y . ((x . i),(i . i)))] is set
{i,(y . ((x . i),(i . i)))} is non empty set
{{i,(y . ((x . i),(i . i)))},{i}} is non empty set
i . [i,(y . ((x . i),(i . i)))] is set
i . (i,(x . i)) is set
[i,(x . i)] is set
{i,(x . i)} is non empty set
{{i,(x . i)},{i}} is non empty set
i . [i,(x . i)] is set
i . (i,(i . i)) is set
[i,(i . i)] is set
{i,(i . i)} is non empty set
{{i,(i . i)},{i}} is non empty set
i . [i,(i . i)] is set
y . ((i . (i,(x . i))),(i . (i,(i . i)))) is set
[(i . (i,(x . i))),(i . (i,(i . i)))] is set
{(i . (i,(x . i))),(i . (i,(i . i)))} is non empty set
{(i . (i,(x . i)))} is non empty trivial V43(1) set
{{(i . (i,(x . i))),(i . (i,(i . i)))},{(i . (i,(x . i)))}} is non empty set
y . [(i . (i,(x . i))),(i . (i,(i . i)))] is set
(i [;] (i,x)) . i is set
y . (((i [;] (i,x)) . i),(i . (i,(i . i)))) is set
[((i [;] (i,x)) . i),(i . (i,(i . i)))] is set
{((i [;] (i,x)) . i),(i . (i,(i . i)))} is non empty set
{((i [;] (i,x)) . i)} is non empty trivial V43(1) set
{{((i [;] (i,x)) . i),(i . (i,(i . i)))},{((i [;] (i,x)) . i)}} is non empty set
y . [((i [;] (i,x)) . i),(i . (i,(i . i)))] is set
(i [;] (i,i)) . i is set
y . (((i [;] (i,x)) . i),((i [;] (i,i)) . i)) is set
[((i [;] (i,x)) . i),((i [;] (i,i)) . i)] is set
{((i [;] (i,x)) . i),((i [;] (i,i)) . i)} is non empty set
{{((i [;] (i,x)) . i),((i [;] (i,i)) . i)},{((i [;] (i,x)) . i)}} is non empty set
y . [((i [;] (i,x)) . i),((i [;] (i,i)) . 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
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 Element of 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 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 VectSpStr over G
the carrier of (G,GS) is non empty 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
the ZeroF of (G,GS) is Element of the carrier of (G,GS)
addLoopStr(# the carrier of (G,GS), the addF of (G,GS), the ZeroF of (G,GS) #) is strict addLoopStr
(G,GS) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr
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 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
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_unity_wrt the multF of G is Element of the carrier of G
i is Element of the carrier of G
y is Element of the carrier of (G,GS)
i is Element of the carrier of (G,GS)
y + i is Element of the carrier of (G,GS)
the addF of (G,GS) . (y,i) is Element of the carrier of (G,GS)
[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,GS) . [y,i] is set
i * (y + i) is Element of the carrier of (G,GS)
the lmult of (G,GS) 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):]
[: 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 lmult of (G,GS) . (i,(y + i)) is Element of the carrier of (G,GS)
[i,(y + i)] is set
{i,(y + i)} is non empty set
{i} is non empty trivial V43(1) set
{{i,(y + i)},{i}} is non empty set
the lmult of (G,GS) . [i,(y + i)] is set
i * y is Element of the carrier of (G,GS)
the lmult of (G,GS) . (i,y) is Element of the carrier of (G,GS)
[i,y] is set
{i,y} is non empty set
{{i,y},{i}} is non empty set
the lmult of (G,GS) . [i,y] is set
i * i is Element of the carrier of (G,GS)
the lmult of (G,GS) . (i,i) is Element of the carrier of (G,GS)
[i,i] is set
{i,i} is non empty set
{{i,i},{i}} is non empty set
the lmult of (G,GS) . [i,i] is set
(i * y) + (i * i) is Element of the carrier of (G,GS)
the addF of (G,GS) . ((i * y),(i * i)) is Element of the carrier of (G,GS)
[(i * y),(i * i)] is set
{(i * y),(i * i)} is non empty set
{(i * y)} is non empty trivial V43(1) set
{{(i * y),(i * i)},{(i * y)}} is non empty set
the addF of (G,GS) . [(i * y),(i * i)] is set
(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,(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 carrier of G, the addF of G,GS) . (y,i) is set
( the carrier of G, the addF of G,GS) . [y,i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,GS) . (i,(( the carrier of G, the addF of G,GS) . (y,i))) is set
[i,(( the carrier of G, the addF of G,GS) . (y,i))] is set
{i,(( the carrier of G, the addF of G,GS) . (y,i))} is non empty set
{{i,(( the carrier of G, the addF of G,GS) . (y,i))},{i}} is non empty set
(G,GS) . [i,(( the carrier of G, the addF of G,GS) . (y,i))] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
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 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 carrier of G,GS, the addF of G,x,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
(G,GS) . (i,( the carrier of G,GS, the addF of G,x,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
[i,( the carrier of G,GS, the addF of G,x,i)] is set
{i,( the carrier of G,GS, the addF of G,x,i)} is non empty set
{{i,( the carrier of G,GS, the addF of G,x,i)},{i}} is non empty set
(G,GS) . [i,( the carrier of G,GS, the addF of G,x,i)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G,GS, the multF of G,i,( the carrier of G,GS, the addF of G,x,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
( the carrier of G,GS, the multF of G,i,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 carrier of G,GS, the multF of G,i,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
( the carrier of G,GS, the addF of G,( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,i,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
( the carrier of G, the addF of G,GS) . (( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,i,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
[( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,i,i)] is set
{( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,i,i)} is functional non empty set
{( the carrier of G,GS, the multF of G,i,x)} is functional non empty trivial V43(1) with_common_domain set
{{( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,i,i)},{( the carrier of G,GS, the multF of G,i,x)}} is non empty set
( the carrier of G, the addF of G,GS) . [( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,i,i)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,GS) . (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,x},{i}} is non empty set
(G,GS) . [i,x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G, the addF of G,GS) . (((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,i,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
[((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,i,i)] is set
{((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,i,i)} is functional non empty set
{((G,GS) . (i,x))} is functional non empty trivial V43(1) with_common_domain set
{{((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,i,i)},{((G,GS) . (i,x))}} is non empty set
( the carrier of G, the addF of G,GS) . [((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,i,i)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,GS) . (i,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
[i,i] is set
{i,i} is non empty set
{{i,i},{i}} is non empty set
(G,GS) . [i,i] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G, the addF of G,GS) . (((G,GS) . (i,x)),((G,GS) . (i,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
[((G,GS) . (i,x)),((G,GS) . (i,i))] is set
{((G,GS) . (i,x)),((G,GS) . (i,i))} is functional non empty set
{{((G,GS) . (i,x)),((G,GS) . (i,i))},{((G,GS) . (i,x))}} is non empty set
( the carrier of G, the addF of G,GS) . [((G,GS) . (i,x)),((G,GS) . (i,i))] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G, the addF of G,GS) . (( the lmult of (G,GS) . (i,y)),((G,GS) . (i,i))) is set
[( the lmult of (G,GS) . (i,y)),((G,GS) . (i,i))] is set
{( the lmult of (G,GS) . (i,y)),((G,GS) . (i,i))} is non empty set
{( the lmult of (G,GS) . (i,y))} is non empty trivial V43(1) set
{{( the lmult of (G,GS) . (i,y)),((G,GS) . (i,i))},{( the lmult of (G,GS) . (i,y))}} is non empty set
( the carrier of G, the addF of G,GS) . [( the lmult of (G,GS) . (i,y)),((G,GS) . (i,i))] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
i is Element of the carrier of G
y is Element of the carrier of G
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
i is Element of the carrier of (G,GS)
(i + y) * i is Element of the carrier of (G,GS)
the lmult of (G,GS) 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):]
[: 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 lmult of (G,GS) . ((i + y),i) is Element of the carrier of (G,GS)
[(i + y),i] is set
{(i + y),i} is non empty set
{(i + y)} is non empty trivial V43(1) set
{{(i + y),i},{(i + y)}} is non empty set
the lmult of (G,GS) . [(i + y),i] is set
i * i is Element of the carrier of (G,GS)
the lmult of (G,GS) . (i,i) is Element of the carrier of (G,GS)
[i,i] is set
{i,i} is non empty set
{{i,i},{i}} is non empty set
the lmult of (G,GS) . [i,i] is set
y * i is Element of the carrier of (G,GS)
the lmult of (G,GS) . (y,i) is Element of the carrier of (G,GS)
[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 lmult of (G,GS) . [y,i] is set
(i * i) + (y * i) is Element of the carrier of (G,GS)
the addF of (G,GS) . ((i * i),(y * i)) is Element of the carrier of (G,GS)
[(i * i),(y * i)] is set
{(i * i),(y * i)} is non empty set
{(i * i)} is non empty trivial V43(1) set
{{(i * i),(y * i)},{(i * i)}} is non empty set
the addF of (G,GS) . [(i * i),(y * i)] is set
i + y is Element of the carrier of G
(i + y) * i is Element of the carrier of (G,GS)
the lmult of (G,GS) . ((i + y),i) is Element of the carrier of (G,GS)
[(i + y),i] is set
{(i + y),i} is non empty set
{(i + y)} is non empty trivial V43(1) set
{{(i + y),i},{(i + y)}} is non empty set
the lmult of (G,GS) . [(i + y),i] is set
(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,(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
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
(G,GS) . ((i + y),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 + y),x] is set
{(i + y),x} is non empty set
{{(i + y),x},{(i + y)}} is non empty set
(G,GS) . [(i + y),x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G,GS, the multF of G,( the addF of G . (i,y)),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 carrier of G,GS, the multF of G,i,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 carrier of G,GS, the multF of G,y,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 carrier of G,GS, the addF of G,( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,y,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 carrier of G, the addF of G,GS) . (( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,y,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
[( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,y,x)] is set
{( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,y,x)} is functional non empty set
{( the carrier of G,GS, the multF of G,i,x)} is functional non empty trivial V43(1) with_common_domain set
{{( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,y,x)},{( the carrier of G,GS, the multF of G,i,x)}} is non empty set
( the carrier of G, the addF of G,GS) . [( the carrier of G,GS, the multF of G,i,x),( the carrier of G,GS, the multF of G,y,x)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,GS) . (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,x},{i}} is non empty set
(G,GS) . [i,x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G, the addF of G,GS) . (((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,y,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
[((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,y,x)] is set
{((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,y,x)} is functional non empty set
{((G,GS) . (i,x))} is functional non empty trivial V43(1) with_common_domain set
{{((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,y,x)},{((G,GS) . (i,x))}} is non empty set
( the carrier of G, the addF of G,GS) . [((G,GS) . (i,x)),( the carrier of G,GS, the multF of G,y,x)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,GS) . (y,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,x] is set
{y,x} is non empty set
{{y,x},{y}} is non empty set
(G,GS) . [y,x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G, the addF of G,GS) . (((G,GS) . (i,x)),((G,GS) . (y,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
[((G,GS) . (i,x)),((G,GS) . (y,x))] is set
{((G,GS) . (i,x)),((G,GS) . (y,x))} is functional non empty set
{{((G,GS) . (i,x)),((G,GS) . (y,x))},{((G,GS) . (i,x))}} is non empty set
( the carrier of G, the addF of G,GS) . [((G,GS) . (i,x)),((G,GS) . (y,x))] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G, the addF of G,GS) . (( the lmult of (G,GS) . (i,i)),((G,GS) . (y,x))) is set
[( the lmult of (G,GS) . (i,i)),((G,GS) . (y,x))] is set
{( the lmult of (G,GS) . (i,i)),((G,GS) . (y,x))} is non empty set
{( the lmult of (G,GS) . (i,i))} is non empty trivial V43(1) set
{{( the lmult of (G,GS) . (i,i)),((G,GS) . (y,x))},{( the lmult of (G,GS) . (i,i))}} is non empty set
( the carrier of G, the addF of G,GS) . [( the lmult of (G,GS) . (i,i)),((G,GS) . (y,x))] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
i is Element of the carrier of G
y is Element of the carrier of G
i * 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
i is Element of the carrier of (G,GS)
(i * y) * i is Element of the carrier of (G,GS)
the lmult of (G,GS) 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):]
[: 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 lmult of (G,GS) . ((i * y),i) is Element of the carrier of (G,GS)
[(i * y),i] is set
{(i * y),i} is non empty set
{(i * y)} is non empty trivial V43(1) set
{{(i * y),i},{(i * y)}} is non empty set
the lmult of (G,GS) . [(i * y),i] is set
y * i is Element of the carrier of (G,GS)
the lmult of (G,GS) . (y,i) is Element of the carrier of (G,GS)
[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 lmult of (G,GS) . [y,i] is set
i * (y * i) is Element of the carrier of (G,GS)
the lmult of (G,GS) . (i,(y * i)) is Element of the carrier of (G,GS)
[i,(y * i)] is set
{i,(y * i)} is non empty set
{{i,(y * i)},{i}} is non empty set
the lmult of (G,GS) . [i,(y * i)] is set
i * y is Element of the carrier of G
(i * y) * i is Element of the carrier of (G,GS)
the lmult of (G,GS) . ((i * y),i) is Element of the carrier of (G,GS)
[(i * y),i] is set
{(i * y),i} is non empty set
{(i * y)} is non empty trivial V43(1) set
{{(i * y),i},{(i * y)}} is non empty set
the lmult of (G,GS) . [(i * y),i] is set
(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,(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
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
(G,GS) . ((i * y),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 * y),x] is set
{(i * y),x} is non empty set
{{(i * y),x},{(i * y)}} is non empty set
(G,GS) . [(i * y),x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G,GS, the multF of G,(i * y),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 carrier of G,GS, the multF of G,y,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 carrier of G,GS, the multF of G,i,( the carrier of G,GS, the multF of G,y,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
(G,GS) . (i,( the carrier of G,GS, the multF of G,y,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,( the carrier of G,GS, the multF of G,y,x)] is set
{i,( the carrier of G,GS, the multF of G,y,x)} is non empty set
{{i,( the carrier of G,GS, the multF of G,y,x)},{i}} is non empty set
(G,GS) . [i,( the carrier of G,GS, the multF of G,y,x)] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,GS) . (y,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,x] is set
{y,x} is non empty set
{{y,x},{y}} is non empty set
(G,GS) . [y,x] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,GS) . (i,((G,GS) . (y,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,((G,GS) . (y,x))] is set
{i,((G,GS) . (y,x))} is non empty set
{{i,((G,GS) . (y,x))},{i}} is non empty set
(G,GS) . [i,((G,GS) . (y,x))] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
(G,GS) . (i,( the lmult of (G,GS) . (y,i))) is set
[i,( the lmult of (G,GS) . (y,i))] is set
{i,( the lmult of (G,GS) . (y,i))} is non empty set
{{i,( the lmult of (G,GS) . (y,i))},{i}} is non empty set
(G,GS) . [i,( the lmult of (G,GS) . (y,i))] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
i is Element of the carrier of (G,GS)
(1. G) * i is Element of the carrier of (G,GS)
the lmult of (G,GS) 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):]
[: 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 lmult of (G,GS) . ((1. G),i) is Element of the carrier of (G,GS)
[(1. G),i] is set
{(1. G),i} is non empty set
{(1. G)} is non empty trivial V43(1) set
{{(1. G),i},{(1. G)}} is non empty set
the lmult of (G,GS) . [(1. G),i] is set
(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,(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
y 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
(G,GS) . ((1. G),y) is Relation-like NAT -defined Function-like V36() V43(GS) countable FinSequence-like FinSubsequence-like Element of GS -tuples_on the carrier of G
[(1. G),y] is set
{(1. G),y} is non empty set
{{(1. G),y},{(1. G)}} is non empty set
(G,GS) . [(1. G),y] is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
( the carrier of G,GS, the multF of G,(1. G),y) 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
F1() is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len F1() is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
dom F1() is non empty countable Element of bool NAT
G is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
len G is V29() V30() V31() V35() V36() V41() countable Element of NAT
dom G is countable Element of bool NAT
GS is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len GS is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
i is Element of dom F1()
GS . i is set
F2(i) is set
Seg (len F1()) is non empty V36() V43( len F1()) countable Element of bool NAT
G is Relation-like non-empty Function-like non empty set
product G is functional non empty with_common_domain product-like set
dom G is non empty set
GS is Relation-like Function-like G -compatible Element of product G
i is Element of dom G
GS . i is set
G . i is non empty set
G is Relation-like non-empty Function-like non empty set
dom G is non empty set
GS is Relation-like Function-like set
dom GS is set
i is Element of dom G
GS . i is set
G . i is non empty set
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
pr1 ((G . i),(G . i)) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
GS is Relation-like Function-like set
dom GS is set
i is Element of dom G
GS . i is set
G . i is non empty set
[:(G . i),(G . i):] is Relation-like set
bool [:(G . i),(G . i):] is set
id (G . i) is Relation-like G . i -defined G . i -valued Function-like one-to-one non empty total V18(G . i,G . i) Element of bool [:(G . i),(G . i):]
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
GS is Relation-like Function-like (G)
dom G is non empty countable Element of bool NAT
dom GS is set
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len G) is non empty V36() V43( len G) countable Element of bool NAT
GS is Relation-like Function-like (G)
dom G is non empty countable Element of bool NAT
dom GS is set
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len G) is non empty V36() V43( len G) countable Element of bool NAT
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
dom G is non empty countable Element of bool NAT
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
len GS is V29() V30() V31() V35() V36() V41() countable Element of NAT
dom GS is countable Element of bool NAT
i is Element of dom G
GS . i is set
G . i is non empty set
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
dom G is non empty countable Element of bool NAT
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
len GS is V29() V30() V31() V35() V36() V41() countable Element of NAT
dom GS is countable Element of bool NAT
i is Element of dom G
GS . i is set
G . i is non empty set
[:(G . i),(G . i):] is Relation-like set
bool [:(G . i),(G . i):] is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
dom G is non empty countable Element of bool NAT
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
i is Element of dom G
GS . i is set
G . i is non empty set
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
dom G is non empty countable Element of bool NAT
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
i is Element of dom G
GS . i is set
G . i is non empty set
[:(G . i),(G . i):] is Relation-like set
bool [:(G . i),(G . i):] is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
product G is functional non empty with_common_domain product-like set
[:(product G),(product G):] is Relation-like set
bool [:(product G),(product G):] is set
dom G is non empty countable Element of bool NAT
GS is Relation-like product G -defined product G -valued Function-like non empty total V18( product G, product G) Element of bool [:(product G),(product G):]
i is Relation-like product G -defined product G -valued Function-like non empty total V18( product G, product G) Element of bool [:(product G),(product G):]
y is Relation-like NAT -defined Function-like G -compatible Element of product G
GS . y is Relation-like NAT -defined Function-like G -compatible Element of product G
dom (GS . y) is set
i . y is Relation-like NAT -defined Function-like G -compatible Element of product G
dom (i . y) is set
i is set
(GS . y) . i is set
(i . y) . i is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
product G is functional non empty with_common_domain product-like set
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
doms GS is Relation-like Function-like set
rngs GS is Relation-like Function-like set
product (rngs GS) is functional with_common_domain product-like set
dom (doms GS) is set
rng GS is set
SubFuncs (rng GS) is set
GS " (SubFuncs (rng GS)) is set
dom G is non empty countable Element of bool NAT
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len G) is non empty V36() V43( len G) countable Element of bool NAT
dom GS is countable Element of bool NAT
len GS is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len GS) is V36() V43( len GS) countable Element of bool NAT
i is set
y is Element of dom G
(G,GS,y) is Relation-like G . y -defined G . y -valued Function-like non empty total V18(G . y,G . y) Element of bool [:(G . y),(G . y):]
G . y is non empty set
[:(G . y),(G . y):] is Relation-like set
bool [:(G . y),(G . y):] is set
i is set
y is Element of dom G
(rngs GS) . y is set
(G,GS,y) is Relation-like G . y -defined G . y -valued Function-like non empty total V18(G . y,G . y) Element of bool [:(G . y),(G . y):]
G . y is non empty set
[:(G . y),(G . y):] is Relation-like set
bool [:(G . y),(G . y):] is set
rng (G,GS,y) is non empty set
(rngs GS) . i is set
G . i is set
i is set
y is Element of dom G
(doms GS) . y is set
(G,GS,y) is Relation-like G . y -defined G . y -valued Function-like non empty total V18(G . y,G . y) Element of bool [:(G . y),(G . y):]
G . y is non empty set
[:(G . y),(G . y):] is Relation-like set
bool [:(G . y),(G . y):] is set
dom (G,GS,y) is non empty set
(doms GS) . i is set
G . i is set
dom (rngs GS) is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
Frege GS is Relation-like Function-like set
product G is functional non empty with_common_domain product-like set
[:(product G),(product G):] is Relation-like set
bool [:(product G),(product G):] is set
rngs GS is Relation-like Function-like set
product (rngs GS) is functional with_common_domain product-like set
rng (Frege GS) is set
dom (Frege GS) is set
doms GS is Relation-like Function-like set
product (doms GS) is functional with_common_domain product-like set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
product G is functional non empty with_common_domain product-like set
dom G is non empty countable Element of bool NAT
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
(G,GS) is Relation-like product G -defined product G -valued Function-like non empty total V18( product G, product G) Element of bool [:(product G),(product G):]
[:(product G),(product G):] is Relation-like set
bool [:(product G),(product G):] is set
i is Relation-like NAT -defined Function-like G -compatible Element of product G
(G,GS) . i is Relation-like NAT -defined Function-like G -compatible Element of product G
y is Element of dom G
(G,((G,GS) . i),y) is Element of G . y
G . y is non empty set
(G,GS,y) is Relation-like G . y -defined G . y -valued Function-like non empty total V18(G . y,G . y) Element of bool [:(G . y),(G . y):]
[:(G . y),(G . y):] is Relation-like set
bool [:(G . y),(G . y):] is set
(G,i,y) is Element of G . y
(G,GS,y) . (G,i,y) is Element of G . y
dom GS is countable Element of bool NAT
len GS is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len GS) is V36() V43( len GS) countable Element of bool NAT
doms GS is Relation-like Function-like set
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len G) is non empty V36() V43( len G) countable Element of bool NAT
G is functional non empty set
[:G,G:] is Relation-like set
[:[:G,G:],G:] is Relation-like set
bool [:[:G,G:],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:]
i is Relation-like Function-like Element of G
y is Relation-like Function-like Element of G
GS . (i,y) is set
[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,y] is Relation-like Function-like set
GS . (i,y) is Relation-like Function-like Element of G
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
product G is functional non empty with_common_domain product-like set
[:(product G),(product G):] is Relation-like set
[:[:(product G),(product G):],(product G):] is Relation-like set
bool [:[:(product G),(product G):],(product G):] is set
dom G is non empty countable Element of bool NAT
GS is Relation-like [:(product G),(product G):] -defined product G -valued Function-like total V18([:(product G),(product G):], product G) Element of bool [:[:(product G),(product G):],(product G):]
i is Relation-like [:(product G),(product G):] -defined product G -valued Function-like total V18([:(product G),(product G):], product G) Element of bool [:[:(product G),(product G):],(product G):]
y is Relation-like NAT -defined Function-like G -compatible Element of product G
i is Relation-like NAT -defined Function-like G -compatible Element of product G
((product G),GS,y,i) is Relation-like NAT -defined Function-like G -compatible Element of product G
[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 . [y,i] is Relation-like Function-like set
dom ((product G),GS,y,i) is set
((product G),i,y,i) is Relation-like NAT -defined Function-like G -compatible Element of product G
i . [y,i] is Relation-like Function-like set
dom ((product G),i,y,i) is set
x is set
((product G),GS,y,i) . x is set
((product G),i,y,i) . x is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
product G is functional non empty with_common_domain product-like set
[:(product G),(product G):] is Relation-like set
[:[:(product G),(product G):],(product G):] is Relation-like set
bool [:[:(product G),(product G):],(product G):] is set
dom G is non empty countable Element of bool NAT
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
i is Relation-like NAT -defined Function-like G -compatible Element of product G
y is Relation-like NAT -defined Function-like G -compatible Element of product G
i is set
x is Element of dom G
G . x is non empty set
(G,GS,x) is Relation-like [:(G . x),(G . x):] -defined G . x -valued Function-like total V18([:(G . x),(G . x):],G . x) Element of bool [:[:(G . x),(G . x):],(G . x):]
[:(G . x),(G . x):] is Relation-like set
[:[:(G . x),(G . x):],(G . x):] is Relation-like set
bool [:[:(G . x),(G . x):],(G . x):] is set
(G,i,x) is Element of G . x
(G,y,x) is Element of G . x
(G,GS,x) . ((G,i,x),(G,y,x)) is Element of G . x
[(G,i,x),(G,y,x)] is set
{(G,i,x),(G,y,x)} is non empty set
{(G,i,x)} is non empty trivial V43(1) set
{{(G,i,x),(G,y,x)},{(G,i,x)}} is non empty set
(G,GS,x) . [(G,i,x),(G,y,x)] is set
i is Relation-like Function-like set
dom i is set
x is set
i . x is set
G . x is set
i is Element of dom G
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
(G,i,i) is Element of G . i
(G,y,i) is Element of G . i
(G,GS,i) . ((G,i,i),(G,y,i)) is Element of G . i
[(G,i,i),(G,y,i)] is set
{(G,i,i),(G,y,i)} is non empty set
{(G,i,i)} is non empty trivial V43(1) set
{{(G,i,i),(G,y,i)},{(G,i,i)}} is non empty set
(G,GS,i) . [(G,i,i),(G,y,i)] is set
x is Relation-like NAT -defined Function-like G -compatible Element of product G
i is Element of dom G
(G,x,i) is Element of G . i
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
(G,i,i) is Element of G . i
(G,y,i) is Element of G . i
(G,GS,i) . ((G,i,i),(G,y,i)) is Element of G . i
[(G,i,i),(G,y,i)] is set
{(G,i,i),(G,y,i)} is non empty set
{(G,i,i)} is non empty trivial V43(1) set
{{(G,i,i),(G,y,i)},{(G,i,i)}} is non empty set
(G,GS,i) . [(G,i,i),(G,y,i)] is set
i . i is set
i is Element of dom G
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
(G,i,i) is Element of G . i
(G,y,i) is Element of G . i
(G,GS,i) . ((G,i,i),(G,y,i)) is Element of G . i
[(G,i,i),(G,y,i)] is set
{(G,i,i),(G,y,i)} is non empty set
{(G,i,i)} is non empty trivial V43(1) set
{{(G,i,i),(G,y,i)},{(G,i,i)}} is non empty set
(G,GS,i) . [(G,i,i),(G,y,i)] is set
i is Relation-like [:(product G),(product G):] -defined product G -valued Function-like total V18([:(product G),(product G):], product G) Element of bool [:[:(product G),(product G):],(product G):]
y is Relation-like NAT -defined Function-like G -compatible Element of product G
i is Relation-like NAT -defined Function-like G -compatible Element of product G
((product G),i,y,i) is Relation-like NAT -defined Function-like G -compatible Element of product G
[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
i . [y,i] is Relation-like Function-like set
x is Element of dom G
(G,((product G),i,y,i),x) is Element of G . x
G . x is non empty set
(G,GS,x) is Relation-like [:(G . x),(G . x):] -defined G . x -valued Function-like total V18([:(G . x),(G . x):],G . x) Element of bool [:[:(G . x),(G . x):],(G . x):]
[:(G . x),(G . x):] is Relation-like set
[:[:(G . x),(G . x):],(G . x):] is Relation-like set
bool [:[:(G . x),(G . x):],(G . x):] is set
(G,y,x) is Element of G . x
(G,i,x) is Element of G . x
(G,GS,x) . ((G,y,x),(G,i,x)) is Element of G . x
[(G,y,x),(G,i,x)] is set
{(G,y,x),(G,i,x)} is non empty set
{(G,y,x)} is non empty trivial V43(1) set
{{(G,y,x),(G,i,x)},{(G,y,x)}} is non empty set
(G,GS,x) . [(G,y,x),(G,i,x)] is set
i is Relation-like [:(product G),(product G):] -defined product G -valued Function-like total V18([:(product G),(product G):], product G) Element of bool [:[:(product G),(product G):],(product G):]
y is Relation-like [:(product G),(product G):] -defined product G -valued Function-like total V18([:(product G),(product G):], product G) Element of bool [:[:(product G),(product G):],(product G):]
i is Relation-like NAT -defined Function-like G -compatible Element of product G
x is Relation-like NAT -defined Function-like G -compatible Element of product G
((product G),i,i,x) is Relation-like NAT -defined Function-like G -compatible Element of product 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
i . [i,x] is Relation-like Function-like set
i is Element of dom G
(G,((product G),i,i,x),i) is Element of G . i
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
(G,i,i) is Element of G . i
(G,x,i) is Element of G . i
(G,GS,i) . ((G,i,i),(G,x,i)) is Element of G . i
[(G,i,i),(G,x,i)] is set
{(G,i,i),(G,x,i)} is non empty set
{(G,i,i)} is non empty trivial V43(1) set
{{(G,i,i),(G,x,i)},{(G,i,i)}} is non empty set
(G,GS,i) . [(G,i,i),(G,x,i)] is set
((product G),y,i,x) is Relation-like NAT -defined Function-like G -compatible Element of product G
y . [i,x] is Relation-like Function-like set
(G,((product G),y,i,x),i) is Element of G . i
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
dom G is non empty countable Element of bool NAT
product G is functional non empty with_common_domain product-like set
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
(G,GS) is Relation-like [:(product G),(product G):] -defined product G -valued Function-like total V18([:(product G),(product G):], product G) Element of bool [:[:(product G),(product G):],(product G):]
[:(product G),(product G):] is Relation-like set
[:[:(product G),(product G):],(product G):] is Relation-like set
bool [:[:(product G),(product G):],(product G):] is set
i is Relation-like NAT -defined Function-like G -compatible Element of product G
y is Relation-like NAT -defined Function-like G -compatible Element of product G
(G,GS) . (i,y) is Relation-like NAT -defined Function-like G -compatible Element of product G
[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
(G,GS) . [i,y] is Relation-like Function-like set
(G,GS) . (y,i) is Relation-like NAT -defined Function-like G -compatible Element of product G
[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
(G,GS) . [y,i] is Relation-like Function-like set
i is set
((product G),(G,GS),y,i) is Relation-like NAT -defined Function-like G -compatible Element of product G
x is Element of dom G
(G,((product G),(G,GS),y,i),x) is Element of G . x
G . x is non empty set
(G,GS,x) is Relation-like [:(G . x),(G . x):] -defined G . x -valued Function-like total V18([:(G . x),(G . x):],G . x) Element of bool [:[:(G . x),(G . x):],(G . x):]
[:(G . x),(G . x):] is Relation-like set
[:[:(G . x),(G . x):],(G . x):] is Relation-like set
bool [:[:(G . x),(G . x):],(G . x):] is set
(G,y,x) is Element of G . x
(G,i,x) is Element of G . x
(G,GS,x) . ((G,y,x),(G,i,x)) is Element of G . x
[(G,y,x),(G,i,x)] is set
{(G,y,x),(G,i,x)} is non empty set
{(G,y,x)} is non empty trivial V43(1) set
{{(G,y,x),(G,i,x)},{(G,y,x)}} is non empty set
(G,GS,x) . [(G,y,x),(G,i,x)] is set
((product G),(G,GS),i,y) is Relation-like NAT -defined Function-like G -compatible Element of product G
(G,((product G),(G,GS),i,y),x) is Element of G . x
(G,GS,x) . ((G,i,x),(G,y,x)) is Element of G . x
[(G,i,x),(G,y,x)] is set
{(G,i,x),(G,y,x)} is non empty set
{(G,i,x)} is non empty trivial V43(1) set
{{(G,i,x),(G,y,x)},{(G,i,x)}} is non empty set
(G,GS,x) . [(G,i,x),(G,y,x)] is set
((product G),(G,GS),i,y) . i is set
((product G),(G,GS),y,i) . i is set
dom ((product G),(G,GS),i,y) is set
dom ((product G),(G,GS),y,i) is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
dom G is non empty countable Element of bool NAT
product G is functional non empty with_common_domain product-like set
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
(G,GS) is Relation-like [:(product G),(product G):] -defined product G -valued Function-like total V18([:(product G),(product G):], product G) Element of bool [:[:(product G),(product G):],(product G):]
[:(product G),(product G):] is Relation-like set
[:[:(product G),(product G):],(product G):] is Relation-like set
bool [:[:(product G),(product G):],(product G):] is set
i is Relation-like NAT -defined Function-like G -compatible Element of product G
y is Relation-like NAT -defined Function-like G -compatible Element of product G
i is Relation-like NAT -defined Function-like G -compatible Element of product G
(G,GS) . (y,i) is Relation-like NAT -defined Function-like G -compatible Element of product G
[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
(G,GS) . [y,i] is Relation-like Function-like set
(G,GS) . (i,((G,GS) . (y,i))) is Relation-like NAT -defined Function-like G -compatible Element of product G
[i,((G,GS) . (y,i))] is set
{i,((G,GS) . (y,i))} is functional non empty set
{i} is functional non empty trivial V43(1) with_common_domain set
{{i,((G,GS) . (y,i))},{i}} is non empty set
(G,GS) . [i,((G,GS) . (y,i))] is Relation-like Function-like set
(G,GS) . (i,y) is Relation-like NAT -defined Function-like G -compatible Element of product G
[i,y] is set
{i,y} is functional non empty set
{{i,y},{i}} is non empty set
(G,GS) . [i,y] is Relation-like Function-like set
(G,GS) . (((G,GS) . (i,y)),i) is Relation-like NAT -defined Function-like G -compatible Element of product G
[((G,GS) . (i,y)),i] is set
{((G,GS) . (i,y)),i} is functional non empty set
{((G,GS) . (i,y))} is functional non empty trivial V43(1) with_common_domain set
{{((G,GS) . (i,y)),i},{((G,GS) . (i,y))}} is non empty set
(G,GS) . [((G,GS) . (i,y)),i] is Relation-like Function-like set
((product G),(G,GS),i,y) is Relation-like NAT -defined Function-like G -compatible Element of product G
((product G),(G,GS),y,i) is Relation-like NAT -defined Function-like G -compatible Element of product G
i is set
i is Element of dom G
(G,((product G),(G,GS),y,i),i) is Element of G . i
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
(G,y,i) is Element of G . i
(G,i,i) is Element of G . i
(G,GS,i) . ((G,y,i),(G,i,i)) is Element of G . i
[(G,y,i),(G,i,i)] is set
{(G,y,i),(G,i,i)} is non empty set
{(G,y,i)} is non empty trivial V43(1) set
{{(G,y,i),(G,i,i)},{(G,y,i)}} is non empty set
(G,GS,i) . [(G,y,i),(G,i,i)] is set
((product G),(G,GS),i,((product G),(G,GS),y,i)) is Relation-like NAT -defined Function-like G -compatible Element of product G
[i,((product G),(G,GS),y,i)] is set
{i,((product G),(G,GS),y,i)} is functional non empty set
{{i,((product G),(G,GS),y,i)},{i}} is non empty set
(G,GS) . [i,((product G),(G,GS),y,i)] is Relation-like Function-like set
(G,((product G),(G,GS),i,((product G),(G,GS),y,i)),i) is Element of G . i
(G,i,i) is Element of G . i
(G,GS,i) . ((G,i,i),(G,((product G),(G,GS),y,i),i)) is Element of G . i
[(G,i,i),(G,((product G),(G,GS),y,i),i)] is set
{(G,i,i),(G,((product G),(G,GS),y,i),i)} is non empty set
{(G,i,i)} is non empty trivial V43(1) set
{{(G,i,i),(G,((product G),(G,GS),y,i),i)},{(G,i,i)}} is non empty set
(G,GS,i) . [(G,i,i),(G,((product G),(G,GS),y,i),i)] is set
((product G),(G,GS),((product G),(G,GS),i,y),i) is Relation-like NAT -defined Function-like G -compatible Element of product G
[((product G),(G,GS),i,y),i] is set
{((product G),(G,GS),i,y),i} is functional non empty set
{((product G),(G,GS),i,y)} is functional non empty trivial V43(1) with_common_domain set
{{((product G),(G,GS),i,y),i},{((product G),(G,GS),i,y)}} is non empty set
(G,GS) . [((product G),(G,GS),i,y),i] is Relation-like Function-like set
(G,((product G),(G,GS),((product G),(G,GS),i,y),i),i) is Element of G . i
(G,((product G),(G,GS),i,y),i) is Element of G . i
(G,GS,i) . ((G,((product G),(G,GS),i,y),i),(G,i,i)) is Element of G . i
[(G,((product G),(G,GS),i,y),i),(G,i,i)] is set
{(G,((product G),(G,GS),i,y),i),(G,i,i)} is non empty set
{(G,((product G),(G,GS),i,y),i)} is non empty trivial V43(1) set
{{(G,((product G),(G,GS),i,y),i),(G,i,i)},{(G,((product G),(G,GS),i,y),i)}} is non empty set
(G,GS,i) . [(G,((product G),(G,GS),i,y),i),(G,i,i)] is set
(G,GS,i) . ((G,i,i),(G,y,i)) is Element of G . i
[(G,i,i),(G,y,i)] is set
{(G,i,i),(G,y,i)} is non empty set
{{(G,i,i),(G,y,i)},{(G,i,i)}} is non empty set
(G,GS,i) . [(G,i,i),(G,y,i)] is set
((product G),(G,GS),i,((product G),(G,GS),y,i)) . i is set
((product G),(G,GS),((product G),(G,GS),i,y),i) . i is set
dom ((product G),(G,GS),i,((product G),(G,GS),y,i)) is set
dom ((product G),(G,GS),((product G),(G,GS),i,y),i) is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
product G is functional non empty with_common_domain product-like set
dom G is non empty countable Element of bool NAT
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
(G,GS) is Relation-like [:(product G),(product G):] -defined product G -valued Function-like total V18([:(product G),(product G):], product G) Element of bool [:[:(product G),(product G):],(product G):]
[:(product G),(product G):] is Relation-like set
[:[:(product G),(product G):],(product G):] is Relation-like set
bool [:[:(product G),(product G):],(product G):] is set
i is Relation-like NAT -defined Function-like G -compatible Element of product G
y is Relation-like NAT -defined Function-like G -compatible Element of product G
dom y is set
i is set
((product G),(G,GS),i,y) is Relation-like NAT -defined Function-like G -compatible Element of product G
[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
(G,GS) . [i,y] is Relation-like Function-like set
x is Element of dom G
(G,((product G),(G,GS),i,y),x) is Element of G . x
G . x is non empty set
(G,GS,x) is Relation-like [:(G . x),(G . x):] -defined G . x -valued Function-like total V18([:(G . x),(G . x):],G . x) Element of bool [:[:(G . x),(G . x):],(G . x):]
[:(G . x),(G . x):] is Relation-like set
[:[:(G . x),(G . x):],(G . x):] is Relation-like set
bool [:[:(G . x),(G . x):],(G . x):] is set
(G,i,x) is Element of G . x
(G,y,x) is Element of G . x
(G,GS,x) . ((G,i,x),(G,y,x)) is Element of G . x
[(G,i,x),(G,y,x)] is set
{(G,i,x),(G,y,x)} is non empty set
{(G,i,x)} is non empty trivial V43(1) set
{{(G,i,x),(G,y,x)},{(G,i,x)}} is non empty set
(G,GS,x) . [(G,i,x),(G,y,x)] is set
((product G),(G,GS),i,y) . i is set
y . i is set
dom ((product G),(G,GS),i,y) is set
i is set
((product G),(G,GS),y,i) is Relation-like NAT -defined Function-like G -compatible Element of product G
[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
(G,GS) . [y,i] is Relation-like Function-like set
x is Element of dom G
(G,((product G),(G,GS),y,i),x) is Element of G . x
G . x is non empty set
(G,GS,x) is Relation-like [:(G . x),(G . x):] -defined G . x -valued Function-like total V18([:(G . x),(G . x):],G . x) Element of bool [:[:(G . x),(G . x):],(G . x):]
[:(G . x),(G . x):] is Relation-like set
[:[:(G . x),(G . x):],(G . x):] is Relation-like set
bool [:[:(G . x),(G . x):],(G . x):] is set
(G,y,x) is Element of G . x
(G,i,x) is Element of G . x
(G,GS,x) . ((G,y,x),(G,i,x)) is Element of G . x
[(G,y,x),(G,i,x)] is set
{(G,y,x),(G,i,x)} is non empty set
{(G,y,x)} is non empty trivial V43(1) set
{{(G,y,x),(G,i,x)},{(G,y,x)}} is non empty set
(G,GS,x) . [(G,y,x),(G,i,x)] is set
((product G),(G,GS),y,i) . i is set
y . i is set
dom ((product G),(G,GS),y,i) is set
G is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
dom G is non empty countable Element of bool NAT
product G is functional non empty with_common_domain product-like set
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
(G,GS) is Relation-like [:(product G),(product G):] -defined product G -valued Function-like total V18([:(product G),(product G):], product G) Element of bool [:[:(product G),(product G):],(product G):]
[:(product G),(product G):] is Relation-like set
[:[:(product G),(product G):],(product G):] is Relation-like set
bool [:[:(product G),(product G):],(product G):] is set
i is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like (G)
(G,i) is Relation-like product G -defined product G -valued Function-like non empty total V18( product G, product G) Element of bool [:(product G),(product G):]
bool [:(product G),(product G):] is set
y is set
i is Element of dom G
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
the_unity_wrt (G,GS,i) is Element of G . i
y is Relation-like Function-like set
dom y is set
i is set
y . i is set
G . i is set
x is Element of dom G
G . x is non empty set
(G,GS,x) is Relation-like [:(G . x),(G . x):] -defined G . x -valued Function-like total V18([:(G . x),(G . x):],G . x) Element of bool [:[:(G . x),(G . x):],(G . x):]
[:(G . x),(G . x):] is Relation-like set
[:[:(G . x),(G . x):],(G . x):] is Relation-like set
bool [:[:(G . x),(G . x):],(G . x):] is set
the_unity_wrt (G,GS,x) is Element of G . x
x is Relation-like NAT -defined Function-like G -compatible Element of product G
(G,i) . x is Relation-like NAT -defined Function-like G -compatible Element of product G
(G,GS) . (x,((G,i) . x)) is Relation-like NAT -defined Function-like G -compatible Element of product G
[x,((G,i) . x)] is set
{x,((G,i) . x)} is functional non empty set
{x} is functional non empty trivial V43(1) with_common_domain set
{{x,((G,i) . x)},{x}} is non empty set
(G,GS) . [x,((G,i) . x)] is Relation-like Function-like set
the_unity_wrt (G,GS) is Relation-like NAT -defined Function-like G -compatible Element of product G
(G,GS) . (((G,i) . x),x) is Relation-like NAT -defined Function-like G -compatible Element of product G
[((G,i) . x),x] is set
{((G,i) . x),x} is functional non empty set
{((G,i) . x)} is functional non empty trivial V43(1) with_common_domain set
{{((G,i) . x),x},{((G,i) . x)}} is non empty set
(G,GS) . [((G,i) . x),x] is Relation-like Function-like set
i is Relation-like NAT -defined Function-like G -compatible Element of product G
dom i is set
i is set
i is Element of dom G
(G,((G,i) . x),i) is Element of G . i
G . i is non empty set
(G,i,i) is Relation-like G . i -defined G . i -valued Function-like non empty total V18(G . i,G . i) Element of bool [:(G . i),(G . i):]
[:(G . i),(G . i):] is Relation-like set
bool [:(G . i),(G . i):] is set
(G,x,i) is Element of G . i
(G,i,i) . (G,x,i) is Element of G . i
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
(G,i,i) is Element of G . i
((product G),(G,GS),x,((G,i) . x)) is Relation-like NAT -defined Function-like G -compatible Element of product G
(G,((product G),(G,GS),x,((G,i) . x)),i) is Element of G . i
(G,GS,i) . ((G,x,i),(G,((G,i) . x),i)) is Element of G . i
[(G,x,i),(G,((G,i) . x),i)] is set
{(G,x,i),(G,((G,i) . x),i)} is non empty set
{(G,x,i)} is non empty trivial V43(1) set
{{(G,x,i),(G,((G,i) . x),i)},{(G,x,i)}} is non empty set
(G,GS,i) . [(G,x,i),(G,((G,i) . x),i)] is set
((product G),(G,GS),x,((G,i) . x)) . i is set
i . i is set
i is Element of dom G
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
the_unity_wrt (G,GS,i) is Element of G . i
i is Element of dom G
(G,i,i) is Element of G . i
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
i is Element of dom G
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
the_unity_wrt (G,GS,i) is Element of G . i
i is set
i is Element of dom G
(G,((G,i) . x),i) is Element of G . i
G . i is non empty set
(G,i,i) is Relation-like G . i -defined G . i -valued Function-like non empty total V18(G . i,G . i) Element of bool [:(G . i),(G . i):]
[:(G . i),(G . i):] is Relation-like set
bool [:(G . i),(G . i):] is set
(G,x,i) is Element of G . i
(G,i,i) . (G,x,i) is Element of G . i
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
(G,i,i) is Element of G . i
((product G),(G,GS),((G,i) . x),x) is Relation-like NAT -defined Function-like G -compatible Element of product G
(G,((product G),(G,GS),((G,i) . x),x),i) is Element of G . i
(G,GS,i) . ((G,((G,i) . x),i),(G,x,i)) is Element of G . i
[(G,((G,i) . x),i),(G,x,i)] is set
{(G,((G,i) . x),i),(G,x,i)} is non empty set
{(G,((G,i) . x),i)} is non empty trivial V43(1) set
{{(G,((G,i) . x),i),(G,x,i)},{(G,((G,i) . x),i)}} is non empty set
(G,GS,i) . [(G,((G,i) . x),i),(G,x,i)] is set
((product G),(G,GS),((G,i) . x),x) . i is set
i . i is set
i is Element of dom G
G . i is non empty set
(G,GS,i) is Relation-like [:(G . i),(G . i):] -defined G . i -valued Function-like total V18([:(G . i),(G . i):],G . i) Element of bool [:[:(G . i),(G . i):],(G . i):]
[:(G . i),(G . i):] is Relation-like set
[:[:(G . i),(G . i):],(G . i):] is Relation-like set
bool [:[:(G . i),(G . i):],(G . i):] is set
the_unity_wrt (G,GS,i) is Element of G . i
dom ((product G),(G,GS),x,((G,i) . x)) is set
dom ((product G),(G,GS),((G,i) . x),x) is set
the non empty right_complementable Abelian add-associative right_zeroed addLoopStr is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
<* the non empty right_complementable Abelian add-associative right_zeroed addLoopStr *> is Relation-like NAT -defined Function-like constant non empty trivial V36() V43(1) countable FinSequence-like FinSubsequence-like set
GS is set
rng <* the non empty right_complementable Abelian add-associative right_zeroed addLoopStr *> is non empty trivial V43(1) set
{ the non empty right_complementable Abelian add-associative right_zeroed addLoopStr } is non empty trivial V43(1) set
G is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like () set
dom G is non empty countable Element of bool NAT
GS is Element of dom G
G . GS is set
rng G is non empty set
G is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like () set
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
dom G is non empty countable Element of bool NAT
Seg (len G) is non empty V36() V43( len G) countable Element of bool NAT
GS is V29() V30() V31() V35() V36() V41() countable set
i is Element of dom G
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,i) is non empty set
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
dom GS is countable Element of bool NAT
rng GS is set
i is set
GS . i is set
y is V29() V30() V31() V35() V36() V41() countable Element of NAT
GS . y is set
i is Element of dom G
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,i) is non empty set
i is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len i is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
y is Element of dom G
i . y is set
(G,y) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,y) is non empty set
i is V29() V30() V31() V35() V36() V41() countable Element of NAT
i . i is set
x is Element of dom G
(G,x) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,x) is non empty set
GS is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len GS is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
i is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len i is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
x is V29() V30() V31() V35() V36() V41() countable set
y is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
dom y is countable Element of bool NAT
y . x is set
i is Element of dom G
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,i) is non empty set
i is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
i . x is set
len y is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len y) is V36() V43( len y) countable Element of bool NAT
dom i is countable Element of bool NAT
len i is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len i) is V36() V43( len i) countable Element of bool NAT
G is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like () set
(G) is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
dom (G) is non empty countable Element of bool NAT
GS is Element of dom (G)
G . GS is set
dom G is non empty countable Element of bool NAT
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len G) is non empty V36() V43( len G) countable Element of bool NAT
len (G) is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len (G)) is non empty V36() V43( len (G)) countable Element of bool NAT
i is Element of dom G
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
G is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like () set
(G) is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len (G) is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
dom (G) is non empty countable Element of bool NAT
GS is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len GS is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
dom G is non empty countable Element of bool NAT
i is Element of dom (G)
GS . i is set
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the addF of (G,i) is Relation-like [: the carrier of (G,i), the carrier of (G,i):] -defined the carrier of (G,i) -valued Function-like total V18([: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i)) Element of bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):]
the carrier of (G,i) is non empty set
[: the carrier of (G,i), the carrier of (G,i):] is Relation-like set
[:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is Relation-like set
bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is set
y is Element of dom G
(G,y) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,y) is non empty set
(G) . y is set
(G) . i is non empty set
[:((G) . i),((G) . i):] is Relation-like set
[:[:((G) . i),((G) . i):],((G) . i):] is Relation-like set
bool [:[:((G) . i),((G) . i):],((G) . i):] is set
i is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like ((G))
len i is V29() V30() V31() V35() V36() V41() countable Element of NAT
y is Element of dom (G)
(G) . y is non empty set
[:((G) . y),((G) . y):] is Relation-like set
(G,y) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,y) is non empty set
[: the carrier of (G,y), the carrier of (G,y):] is Relation-like set
((G),i,y) is Relation-like [:((G) . y),((G) . y):] -defined (G) . y -valued Function-like total V18([:((G) . y),((G) . y):],(G) . y) Element of bool [:[:((G) . y),((G) . y):],((G) . y):]
[:[:((G) . y),((G) . y):],((G) . y):] is Relation-like set
bool [:[:((G) . y),((G) . y):],((G) . y):] is set
the addF of (G,y) is Relation-like [: the carrier of (G,y), the carrier of (G,y):] -defined the carrier of (G,y) -valued Function-like total V18([: the carrier of (G,y), the carrier of (G,y):], the carrier of (G,y)) Element of bool [:[: the carrier of (G,y), the carrier of (G,y):], the carrier of (G,y):]
[:[: the carrier of (G,y), the carrier of (G,y):], the carrier of (G,y):] is Relation-like set
bool [:[: the carrier of (G,y), the carrier of (G,y):], the carrier of (G,y):] is set
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like ((G))
len GS is V29() V30() V31() V35() V36() V41() countable Element of NAT
i is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like ((G))
len i is V29() V30() V31() V35() V36() V41() countable Element of NAT
x is V29() V30() V31() V35() V36() V41() countable set
y is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
dom y is countable Element of bool NAT
y . x is set
i is Element of dom (G)
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the addF of (G,i) is Relation-like [: the carrier of (G,i), the carrier of (G,i):] -defined the carrier of (G,i) -valued Function-like total V18([: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i)) Element of bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):]
the carrier of (G,i) is non empty set
[: the carrier of (G,i), the carrier of (G,i):] is Relation-like set
[:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is Relation-like set
bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is set
i is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
i . x is set
len y is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len y) is V36() V43( len y) countable Element of bool NAT
dom i is countable Element of bool NAT
len i is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len i) is V36() V43( len i) countable Element of bool NAT
GS is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len GS is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
dom G is non empty countable Element of bool NAT
i is Element of dom (G)
GS . i is set
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
comp (G,i) is Relation-like the carrier of (G,i) -defined the carrier of (G,i) -valued Function-like non empty total V18( the carrier of (G,i), the carrier of (G,i)) Element of bool [: the carrier of (G,i), the carrier of (G,i):]
the carrier of (G,i) is non empty set
[: the carrier of (G,i), the carrier of (G,i):] is Relation-like set
bool [: the carrier of (G,i), the carrier of (G,i):] is set
y is Element of dom G
(G,y) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,y) is non empty set
(G) . y is set
(G) . i is non empty set
[:((G) . i),((G) . i):] is Relation-like set
bool [:((G) . i),((G) . i):] is set
i is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like ((G))
len i is V29() V30() V31() V35() V36() V41() countable Element of NAT
y is Element of dom (G)
(G) . y is non empty set
(G,y) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,y) is non empty set
((G),i,y) is Relation-like (G) . y -defined (G) . y -valued Function-like non empty total V18((G) . y,(G) . y) Element of bool [:((G) . y),((G) . y):]
[:((G) . y),((G) . y):] is Relation-like set
bool [:((G) . y),((G) . y):] is set
comp (G,y) is Relation-like the carrier of (G,y) -defined the carrier of (G,y) -valued Function-like non empty total V18( the carrier of (G,y), the carrier of (G,y)) Element of bool [: the carrier of (G,y), the carrier of (G,y):]
[: the carrier of (G,y), the carrier of (G,y):] is Relation-like set
bool [: the carrier of (G,y), the carrier of (G,y):] is set
GS is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like ((G))
len GS is V29() V30() V31() V35() V36() V41() countable Element of NAT
i is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like ((G))
len i is V29() V30() V31() V35() V36() V41() countable Element of NAT
x is V29() V30() V31() V35() V36() V41() countable set
y is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
dom y is countable Element of bool NAT
GS . x is set
i is Element of dom (G)
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
comp (G,i) is Relation-like the carrier of (G,i) -defined the carrier of (G,i) -valued Function-like non empty total V18( the carrier of (G,i), the carrier of (G,i)) Element of bool [: the carrier of (G,i), the carrier of (G,i):]
the carrier of (G,i) is non empty set
[: the carrier of (G,i), the carrier of (G,i):] is Relation-like set
bool [: the carrier of (G,i), the carrier of (G,i):] is set
i . x is set
len y is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len y) is V36() V43( len y) countable Element of bool NAT
i is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like set
dom i is countable Element of bool NAT
len i is V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len i) is V36() V43( len i) countable Element of bool NAT
product (G) is functional non empty with_common_domain product-like set
Seg (len (G)) is non empty V36() V43( len (G)) countable Element of bool NAT
GS is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
len GS is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
dom G is non empty countable Element of bool NAT
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len G) is non empty V36() V43( len G) countable Element of bool NAT
i is set
y is Element of dom (G)
GS . y is set
(G,y) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
0. (G,y) is V65((G,y)) Element of the carrier of (G,y)
the carrier of (G,y) is non empty set
the ZeroF of (G,y) is Element of the carrier of (G,y)
i is Element of dom G
(G) . i is set
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,i) is non empty set
GS . i is set
(G) . i is set
dom GS is non empty countable Element of bool NAT
Seg (len GS) is non empty V36() V43( len GS) countable Element of bool NAT
i is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
y is Element of dom (G)
((G),i,y) is Element of (G) . y
(G) . y is non empty set
(G,y) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
0. (G,y) is V65((G,y)) Element of the carrier of (G,y)
the carrier of (G,y) is non empty set
the ZeroF of (G,y) is Element of the carrier of (G,y)
GS is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
i is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
x is set
y is Relation-like Function-like set
y . x is set
i is Element of dom (G)
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
0. (G,i) is V65((G,i)) Element of the carrier of (G,i)
the carrier of (G,i) is non empty set
the ZeroF of (G,i) is Element of the carrier of (G,i)
i is Relation-like Function-like set
i . x is set
dom y is set
dom i is set
G is Relation-like NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like () set
(G) is Relation-like non-empty NAT -defined Function-like non empty V36() countable FinSequence-like FinSubsequence-like set
product (G) is functional non empty with_common_domain product-like set
(G) is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like ((G))
((G),(G)) is Relation-like [:(product (G)),(product (G)):] -defined product (G) -valued Function-like total V18([:(product (G)),(product (G)):], product (G)) Element of bool [:[:(product (G)),(product (G)):],(product (G)):]
[:(product (G)),(product (G)):] is Relation-like set
[:[:(product (G)),(product (G)):],(product (G)):] is Relation-like set
bool [:[:(product (G)),(product (G)):],(product (G)):] is set
(G) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
addLoopStr(# (product (G)),((G),(G)),(G) #) is strict addLoopStr
dom (G) is non empty countable Element of bool NAT
dom G is non empty countable Element of bool NAT
len G is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len G) is non empty V36() V43( len G) countable Element of bool NAT
len (G) is non empty V29() V30() V31() V35() V36() V41() countable Element of NAT
Seg (len (G)) is non empty V36() V43( len (G)) countable Element of bool NAT
i is Element of dom (G)
(G) . i is non empty set
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,i) is non empty set
i is Element of dom (G)
(G) . i is non empty set
[:((G) . i),((G) . i):] is Relation-like set
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,i) is non empty set
[: the carrier of (G,i), the carrier of (G,i):] is Relation-like set
((G),(G),i) is Relation-like [:((G) . i),((G) . i):] -defined (G) . i -valued Function-like total V18([:((G) . i),((G) . i):],(G) . i) Element of bool [:[:((G) . i),((G) . i):],((G) . i):]
[:[:((G) . i),((G) . i):],((G) . i):] is Relation-like set
bool [:[:((G) . i),((G) . i):],((G) . i):] is set
the addF of (G,i) is Relation-like [: the carrier of (G,i), the carrier of (G,i):] -defined the carrier of (G,i) -valued Function-like total V18([: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i)) Element of bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):]
[:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is Relation-like set
bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is set
i is Element of dom (G)
(G) . i is non empty set
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,i) is non empty set
[:((G) . i),((G) . i):] is Relation-like set
[: the carrier of (G,i), the carrier of (G,i):] is Relation-like set
((G),(G),i) is Relation-like [:((G) . i),((G) . i):] -defined (G) . i -valued Function-like total V18([:((G) . i),((G) . i):],(G) . i) Element of bool [:[:((G) . i),((G) . i):],((G) . i):]
[:[:((G) . i),((G) . i):],((G) . i):] is Relation-like set
bool [:[:((G) . i),((G) . i):],((G) . i):] is set
the addF of (G,i) is Relation-like [: the carrier of (G,i), the carrier of (G,i):] -defined the carrier of (G,i) -valued Function-like total V18([: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i)) Element of bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):]
[:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is Relation-like set
bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is set
((G),(G),i) is Element of (G) . i
0. (G,i) is V65((G,i)) Element of the carrier of (G,i)
the ZeroF of (G,i) is Element of the carrier of (G,i)
GS is non empty addLoopStr
the carrier of GS is non empty set
i is Element of the carrier of GS
(G) is Relation-like NAT -defined Function-like V36() countable FinSequence-like FinSubsequence-like ((G))
((G),(G)) is Relation-like product (G) -defined product (G) -valued Function-like non empty total V18( product (G), product (G)) Element of bool [:(product (G)),(product (G)):]
bool [:(product (G)),(product (G)):] is set
((G),(G)) . i is Relation-like Function-like set
y is Element of the carrier of GS
i + y is Element of the carrier of GS
the addF of GS is Relation-like [: the carrier of GS, the carrier of GS:] -defined the carrier of GS -valued Function-like total V18([: the carrier of GS, the carrier of GS:], the carrier of GS) Element of bool [:[: the carrier of GS, the carrier of GS:], the carrier of GS:]
[: the carrier of GS, the carrier of GS:] is Relation-like set
[:[: the carrier of GS, the carrier of GS:], the carrier of GS:] is Relation-like set
bool [:[: the carrier of GS, the carrier of GS:], the carrier of GS:] is set
the addF of GS . (i,y) is Element of the carrier of GS
[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 GS . [i,y] is set
0. GS is V65(GS) Element of the carrier of GS
the ZeroF of GS is Element of the carrier of GS
i is Element of dom (G)
(G) . i is non empty set
[:((G) . i),((G) . i):] is Relation-like set
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,i) is non empty set
[: the carrier of (G,i), the carrier of (G,i):] is Relation-like set
((G),(G),i) is Relation-like [:((G) . i),((G) . i):] -defined (G) . i -valued Function-like total V18([:((G) . i),((G) . i):],(G) . i) Element of bool [:[:((G) . i),((G) . i):],((G) . i):]
[:[:((G) . i),((G) . i):],((G) . i):] is Relation-like set
bool [:[:((G) . i),((G) . i):],((G) . i):] is set
the addF of (G,i) is Relation-like [: the carrier of (G,i), the carrier of (G,i):] -defined the carrier of (G,i) -valued Function-like total V18([: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i)) Element of bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):]
[:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is Relation-like set
bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is set
((G),(G),i) is Relation-like (G) . i -defined (G) . i -valued Function-like non empty total V18((G) . i,(G) . i) Element of bool [:((G) . i),((G) . i):]
bool [:((G) . i),((G) . i):] is set
comp (G,i) is Relation-like the carrier of (G,i) -defined the carrier of (G,i) -valued Function-like non empty total V18( the carrier of (G,i), the carrier of (G,i)) Element of bool [: the carrier of (G,i), the carrier of (G,i):]
bool [: the carrier of (G,i), the carrier of (G,i):] is set
0. (G,i) is V65((G,i)) Element of the carrier of (G,i)
the ZeroF of (G,i) is Element of the carrier of (G,i)
the_unity_wrt ((G),(G)) is Relation-like NAT -defined Function-like (G) -compatible Element of product (G)
i is Element of dom (G)
(G) . i is non empty set
[:((G) . i),((G) . i):] is Relation-like set
(G,i) is non empty right_complementable Abelian add-associative right_zeroed addLoopStr
the carrier of (G,i) is non empty set
[: the carrier of (G,i), the carrier of (G,i):] is Relation-like set
((G),(G),i) is Relation-like [:((G) . i),((G) . i):] -defined (G) . i -valued Function-like total V18([:((G) . i),((G) . i):],(G) . i) Element of bool [:[:((G) . i),((G) . i):],((G) . i):]
[:[:((G) . i),((G) . i):],((G) . i):] is Relation-like set
bool [:[:((G) . i),((G) . i):],((G) . i):] is set
the addF of (G,i) is Relation-like [: the carrier of (G,i), the carrier of (G,i):] -defined the carrier of (G,i) -valued Function-like total V18([: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i)) Element of bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):]
[:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is Relation-like set
bool [:[: the carrier of (G,i), the carrier of (G,i):], the carrier of (G,i):] is set
0. GS is V65(GS) Element of the carrier of GS
the carrier of GS is non empty set
the ZeroF of GS is Element of the carrier of GS