:: PRVECT_1 semantic presentation

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

c

(G,i,GS,i,c

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(# H

the carrier of VectSpStr(# H

the addF of VectSpStr(# H

[: the carrier of VectSpStr(# H

[:[: the carrier of VectSpStr(# H

bool [:[: the carrier of VectSpStr(# H

the ZeroF of VectSpStr(# H

addLoopStr(# the carrier of VectSpStr(# H

the lmult of VectSpStr(# H

[: the carrier of G, the carrier of VectSpStr(# H

[:[: the carrier of G, the carrier of VectSpStr(# H

bool [:[: the carrier of G, the