:: AFVECT0 semantic presentation

K122() is Element of bool K118()

K118() is set

bool K118() is V11() set

K117() is set

bool K117() is V11() set

bool K122() is V11() set

K14() is Relation-like non-empty empty-yielding V11() set

1 is V11() set

G_Real is non empty strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

the carrier of G_Real is V11() set

the non empty non trivial strict AffVect-like AffinStruct is non empty non trivial strict AffVect-like AffinStruct

o9 is non empty AffinStruct

the carrier of o9 is V11() set

o is Element of the carrier of o9

AS is Element of the carrier of o9

X is Element of the carrier of o9

Z is Element of the carrier of o9

T is Element of the carrier of o9

f is Element of the carrier of o9

a is Element of the carrier of o9

g is Element of the carrier of o9

b is Element of the carrier of o9

o is Element of the carrier of o9

AS is Element of the carrier of o9

X is Element of the carrier of o9

Z is Element of the carrier of o9

T is Element of the carrier of o9

g is Element of the carrier of o9

o is Element of the carrier of o9

AS is Element of the carrier of o9

X is Element of the carrier of o9

Z is Element of the carrier of o9

T is Element of the carrier of o9

a is Element of the carrier of o9

b is Element of the carrier of o9

g is Element of the carrier of o9

f is Element of the carrier of o9

ADG is non empty AffinStruct

the carrier of ADG is V11() set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

g is Element of the carrier of ADG

f is Element of the carrier of ADG

T is Element of the carrier of ADG

a is Element of the carrier of ADG

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

T is Element of the carrier of ADG

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

f is Element of the carrier of ADG

a is Element of the carrier of ADG

T is Element of the carrier of ADG

g is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

T is Element of the carrier of ADG

g is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

T is Element of the carrier of ADG

g is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

T is Element of the carrier of ADG

g is Element of the carrier of ADG

f is Element of the carrier of ADG

a is Element of the carrier of ADG

b is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

T is Element of the carrier of ADG

g is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

AS is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

T is Element of the carrier of ADG

g is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

T is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

T is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o is Element of the carrier of ADG

o9 is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

(ADG,o9,o) is Element of the carrier of ADG

AS is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

(ADG,o9,o) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

(ADG,o9,o) is Element of the carrier of ADG

(ADG,o9,(ADG,o9,o)) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

(ADG,o9,o) is Element of the carrier of ADG

AS is Element of the carrier of ADG

(ADG,o9,AS) is Element of the carrier of ADG

(ADG,o9,(ADG,o9,o)) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

(ADG,o9,o) is Element of the carrier of ADG

(ADG,o9,(ADG,o9,o)) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

(ADG,AS,o) is Element of the carrier of ADG

(ADG,AS,o9) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

(ADG,Z,o9) is Element of the carrier of ADG

(ADG,Z,o) is Element of the carrier of ADG

(ADG,Z,AS) is Element of the carrier of ADG

(ADG,Z,X) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

(ADG,AS,o9) is Element of the carrier of ADG

(ADG,AS,o) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

(ADG,X,o9) is Element of the carrier of ADG

(ADG,X,o) is Element of the carrier of ADG

(ADG,X,AS) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

(ADG,o9,o) is Element of the carrier of ADG

AS is Element of the carrier of ADG

(ADG,AS,o) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

(ADG,o9,o) is Element of the carrier of ADG

AS is Element of the carrier of ADG

(ADG,o9,AS) is Element of the carrier of ADG

(ADG,o,(ADG,o9,AS)) is Element of the carrier of ADG

(ADG,o9,(ADG,o,(ADG,o9,AS))) is Element of the carrier of ADG

(ADG,(ADG,o9,o),AS) is Element of the carrier of ADG

(ADG,o9,(ADG,o9,AS)) is Element of the carrier of ADG

(ADG,(ADG,o9,o),(ADG,o9,(ADG,o9,AS))) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

(ADG,o9,o) is Element of the carrier of ADG

AS is Element of the carrier of ADG

(ADG,o,AS) is Element of the carrier of ADG

(ADG,o9,(ADG,o,AS)) is Element of the carrier of ADG

(ADG,o9,AS) is Element of the carrier of ADG

(ADG,o,(ADG,o9,AS)) is Element of the carrier of ADG

(ADG,o9,(ADG,o,(ADG,o9,AS))) is Element of the carrier of ADG

(ADG,(ADG,o9,o),AS) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

(ADG,AS,X) is Element of the carrier of ADG

(ADG,o,(ADG,AS,X)) is Element of the carrier of ADG

(ADG,o9,(ADG,o,(ADG,AS,X))) is Element of the carrier of ADG

(ADG,o9,X) is Element of the carrier of ADG

(ADG,o,(ADG,o9,X)) is Element of the carrier of ADG

(ADG,AS,(ADG,o,(ADG,o9,X))) is Element of the carrier of ADG

(ADG,AS,o9) is Element of the carrier of ADG

(ADG,o,(ADG,AS,o9)) is Element of the carrier of ADG

(ADG,o9,o9) is Element of the carrier of ADG

(ADG,o,(ADG,o9,o9)) is Element of the carrier of ADG

(ADG,o,o9) is Element of the carrier of ADG

(ADG,AS,(ADG,AS,o9)) is Element of the carrier of ADG

(ADG,AS,(ADG,o,o9)) is Element of the carrier of ADG

(ADG,o,(ADG,o,(ADG,AS,o9))) is Element of the carrier of ADG

(ADG,o9,(ADG,o,(ADG,AS,o9))) is Element of the carrier of ADG

(ADG,AS,(ADG,o,(ADG,o9,o9))) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

(ADG,AS,X) is Element of the carrier of ADG

(ADG,o,(ADG,AS,X)) is Element of the carrier of ADG

(ADG,o9,(ADG,o,(ADG,AS,X))) is Element of the carrier of ADG

Z is Element of the carrier of ADG

T is Element of the carrier of ADG

(ADG,Z,o9) is Element of the carrier of ADG

(ADG,T,X) is Element of the carrier of ADG

(ADG,AS,(ADG,T,X)) is Element of the carrier of ADG

(ADG,Z,o) is Element of the carrier of ADG

(ADG,(ADG,Z,o),X) is Element of the carrier of ADG

(ADG,(ADG,Z,o9),(ADG,(ADG,Z,o),X)) is Element of the carrier of ADG

(ADG,Z,X) is Element of the carrier of ADG

(ADG,o,(ADG,Z,X)) is Element of the carrier of ADG

(ADG,Z,(ADG,o,(ADG,Z,X))) is Element of the carrier of ADG

(ADG,(ADG,Z,o9),(ADG,Z,(ADG,o,(ADG,Z,X)))) is Element of the carrier of ADG

(ADG,Z,(ADG,Z,(ADG,o,(ADG,Z,X)))) is Element of the carrier of ADG

(ADG,o9,(ADG,Z,(ADG,Z,(ADG,o,(ADG,Z,X))))) is Element of the carrier of ADG

(ADG,Z,(ADG,o9,(ADG,Z,(ADG,Z,(ADG,o,(ADG,Z,X)))))) is Element of the carrier of ADG

(ADG,o9,(ADG,o,(ADG,Z,X))) is Element of the carrier of ADG

(ADG,Z,(ADG,o9,(ADG,o,(ADG,Z,X)))) is Element of the carrier of ADG

(ADG,o9,X) is Element of the carrier of ADG

(ADG,o,(ADG,o9,X)) is Element of the carrier of ADG

(ADG,Z,(ADG,o,(ADG,o9,X))) is Element of the carrier of ADG

(ADG,Z,(ADG,Z,(ADG,o,(ADG,o9,X)))) is Element of the carrier of ADG

(ADG,AS,(ADG,o,(ADG,o9,X))) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

(ADG,AS,o) is Element of the carrier of ADG

X is Element of the carrier of ADG

(ADG,X,o9) is Element of the carrier of ADG

(ADG,(ADG,X,o9),o) is Element of the carrier of ADG

(ADG,X,o) is Element of the carrier of ADG

(ADG,o9,(ADG,X,o)) is Element of the carrier of ADG

(ADG,X,(ADG,o9,(ADG,X,o))) is Element of the carrier of ADG

(ADG,X,(ADG,AS,o)) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

(ADG,o9,o) is Element of the carrier of ADG

AS is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

o9 is Element of the carrier of ADG

o is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

o . (AS,X) is Element of the carrier of ADG

[AS,X] is V15() set

o . [AS,X] is set

(ADG,o9,AS,X) is Element of the carrier of ADG

AS is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

X is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

Z is Element of [: the carrier of ADG, the carrier of ADG:]

AS . Z is Element of the carrier of ADG

X . Z is Element of the carrier of ADG

T is Element of the carrier of ADG

g is Element of the carrier of ADG

[T,g] is V15() set

AS . (T,g) is Element of the carrier of ADG

AS . [T,g] is set

(ADG,o9,T,g) is Element of the carrier of ADG

X . (T,g) is Element of the carrier of ADG

X . [T,g] is set

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

bool [: the carrier of ADG, the carrier of ADG:] is V11() set

o9 is Element of the carrier of ADG

o is Relation-like the carrier of ADG -defined the carrier of ADG -valued Function-like V18( the carrier of ADG, the carrier of ADG) Element of bool [: the carrier of ADG, the carrier of ADG:]

AS is Element of the carrier of ADG

o . AS is Element of the carrier of ADG

(ADG,o9,AS) is Element of the carrier of ADG

AS is Relation-like the carrier of ADG -defined the carrier of ADG -valued Function-like V18( the carrier of ADG, the carrier of ADG) Element of bool [: the carrier of ADG, the carrier of ADG:]

X is Relation-like the carrier of ADG -defined the carrier of ADG -valued Function-like V18( the carrier of ADG, the carrier of ADG) Element of bool [: the carrier of ADG, the carrier of ADG:]

Z is Element of the carrier of ADG

AS . Z is Element of the carrier of ADG

X . Z is Element of the carrier of ADG

(ADG,o9,Z) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is strict addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o is non empty non trivial () AffinStruct

the carrier of o is V11() non trivial set

X is non empty non trivial () AffinStruct

the carrier of X is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

AS is Element of the carrier of o

(o,AS) is non empty strict addLoopStr

(o,AS) is Relation-like [: the carrier of o, the carrier of o:] -defined the carrier of o -valued Function-like V18([: the carrier of o, the carrier of o:], the carrier of o) Element of bool [:[: the carrier of o, the carrier of o:], the carrier of o:]

[: the carrier of o, the carrier of o:] is Relation-like V11() set

[:[: the carrier of o, the carrier of o:], the carrier of o:] is Relation-like V11() set

bool [:[: the carrier of o, the carrier of o:], the carrier of o:] is V11() set

addLoopStr(# the carrier of o,(o,AS),AS #) is strict addLoopStr

the addF of (o,AS) is Relation-like [: the carrier of (o,AS), the carrier of (o,AS):] -defined the carrier of (o,AS) -valued Function-like V18([: the carrier of (o,AS), the carrier of (o,AS):], the carrier of (o,AS)) Element of bool [:[: the carrier of (o,AS), the carrier of (o,AS):], the carrier of (o,AS):]

the carrier of (o,AS) is V11() set

[: the carrier of (o,AS), the carrier of (o,AS):] is Relation-like V11() set

[:[: the carrier of (o,AS), the carrier of (o,AS):], the carrier of (o,AS):] is Relation-like V11() set

bool [:[: the carrier of (o,AS), the carrier of (o,AS):], the carrier of (o,AS):] is V11() set

Z is Element of the carrier of X

(X,Z) is non empty strict addLoopStr

(X,Z) is Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like V18([: the carrier of X, the carrier of X:], the carrier of X) Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[: the carrier of X, the carrier of X:] is Relation-like V11() set

[:[: the carrier of X, the carrier of X:], the carrier of X:] is Relation-like V11() set

bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is V11() set

addLoopStr(# the carrier of X,(X,Z),Z #) is strict addLoopStr

0. (X,Z) is V52((X,Z)) Element of the carrier of (X,Z)

the carrier of (X,Z) is V11() set

the ZeroF of (X,Z) is Element of the carrier of (X,Z)

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

o is Element of the carrier of (ADG,o9)

X is Element of the carrier of ADG

AS is Element of the carrier of (ADG,o9)

Z is Element of the carrier of ADG

o + AS is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,AS) is Element of the carrier of (ADG,o9)

[o,AS] is V15() set

the addF of (ADG,o9) . [o,AS] is set

(ADG,o9) . (X,Z) is Element of the carrier of ADG

[X,Z] is V15() set

(ADG,o9) . [X,Z] is set

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

o is Element of the carrier of (ADG,o9)

AS is Element of the carrier of (ADG,o9)

o + AS is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,AS) is Element of the carrier of (ADG,o9)

[o,AS] is V15() set

the addF of (ADG,o9) . [o,AS] is set

AS + o is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . (AS,o) is Element of the carrier of (ADG,o9)

[AS,o] is V15() set

the addF of (ADG,o9) . [AS,o] is set

T is Element of the carrier of ADG

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

(ADG,o9,X,Z) is Element of the carrier of ADG

(ADG,o9,Z,X) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

o is Element of the carrier of (ADG,o9)

AS is Element of the carrier of (ADG,o9)

o + AS is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,AS) is Element of the carrier of (ADG,o9)

[o,AS] is V15() set

the addF of (ADG,o9) . [o,AS] is set

X is Element of the carrier of (ADG,o9)

(o + AS) + X is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . ((o + AS),X) is Element of the carrier of (ADG,o9)

[(o + AS),X] is V15() set

the addF of (ADG,o9) . [(o + AS),X] is set

AS + X is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . (AS,X) is Element of the carrier of (ADG,o9)

[AS,X] is V15() set

the addF of (ADG,o9) . [AS,X] is set

o + (AS + X) is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . (o,(AS + X)) is Element of the carrier of (ADG,o9)

[o,(AS + X)] is V15() set

the addF of (ADG,o9) . [o,(AS + X)] is set

z19 is Element of the carrier of ADG

b is Element of the carrier of ADG

g is Element of the carrier of ADG

x1 is Element of the carrier of ADG

Z is Element of the carrier of ADG

(ADG,o9,Z,b) is Element of the carrier of ADG

fa is Element of the carrier of ADG

T is Element of the carrier of ADG

(ADG,o9,Z,T) is Element of the carrier of ADG

(ADG,o9,T,g) is Element of the carrier of ADG

z29 is Element of the carrier of ADG

(ADG,o9,fa,g) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

0. (ADG,o9) is V52((ADG,o9)) Element of the carrier of (ADG,o9)

the ZeroF of (ADG,o9) is Element of the carrier of (ADG,o9)

o is Element of the carrier of (ADG,o9)

o + (0. (ADG,o9)) is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,(0. (ADG,o9))) is Element of the carrier of (ADG,o9)

[o,(0. (ADG,o9))] is V15() set

the addF of (ADG,o9) . [o,(0. (ADG,o9))] is set

X is Element of the carrier of ADG

AS is Element of the carrier of ADG

(ADG,o9,AS,o9) is Element of the carrier of ADG

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

o is Element of the carrier of (ADG,o9)

AS is Element of the carrier of (ADG,o9)

o + AS is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,AS) is Element of the carrier of (ADG,o9)

[o,AS] is V15() set

the addF of (ADG,o9) . [o,AS] is set

AS + o is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . (AS,o) is Element of the carrier of (ADG,o9)

[AS,o] is V15() set

the addF of (ADG,o9) . [AS,o] is set

o is Element of the carrier of (ADG,o9)

AS is Element of the carrier of (ADG,o9)

o + AS is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,AS) is Element of the carrier of (ADG,o9)

[o,AS] is V15() set

the addF of (ADG,o9) . [o,AS] is set

X is Element of the carrier of (ADG,o9)

(o + AS) + X is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . ((o + AS),X) is Element of the carrier of (ADG,o9)

[(o + AS),X] is V15() set

the addF of (ADG,o9) . [(o + AS),X] is set

AS + X is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . (AS,X) is Element of the carrier of (ADG,o9)

[AS,X] is V15() set

the addF of (ADG,o9) . [AS,X] is set

o + (AS + X) is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . (o,(AS + X)) is Element of the carrier of (ADG,o9)

[o,(AS + X)] is V15() set

the addF of (ADG,o9) . [o,(AS + X)] is set

0. (ADG,o9) is V52((ADG,o9)) Element of the carrier of (ADG,o9)

the ZeroF of (ADG,o9) is Element of the carrier of (ADG,o9)

o is Element of the carrier of (ADG,o9)

o + (0. (ADG,o9)) is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,(0. (ADG,o9))) is Element of the carrier of (ADG,o9)

[o,(0. (ADG,o9))] is V15() set

the addF of (ADG,o9) . [o,(0. (ADG,o9))] is set

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

o is Element of the carrier of (ADG,o9)

(ADG,o9) is Relation-like the carrier of ADG -defined the carrier of ADG -valued Function-like V18( the carrier of ADG, the carrier of ADG) Element of bool [: the carrier of ADG, the carrier of ADG:]

bool [: the carrier of ADG, the carrier of ADG:] is V11() set

AS is Element of the carrier of ADG

(ADG,o9) . AS is Element of the carrier of ADG

X is Element of the carrier of (ADG,o9)

o + X is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,X) is Element of the carrier of (ADG,o9)

[o,X] is V15() set

the addF of (ADG,o9) . [o,X] is set

0. (ADG,o9) is V52((ADG,o9)) Element of the carrier of (ADG,o9)

the ZeroF of (ADG,o9) is Element of the carrier of (ADG,o9)

(ADG,o9,o9) is Element of the carrier of ADG

(ADG,o9,AS) is Element of the carrier of ADG

(ADG,o9,AS,(ADG,o9,AS)) is Element of the carrier of ADG

(ADG,o9) . (AS,(ADG,o9,AS)) is Element of the carrier of ADG

[AS,(ADG,o9,AS)] is V15() set

(ADG,o9) . [AS,(ADG,o9,AS)] is set

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

(ADG,o9) is Relation-like the carrier of ADG -defined the carrier of ADG -valued Function-like V18( the carrier of ADG, the carrier of ADG) Element of bool [: the carrier of ADG, the carrier of ADG:]

bool [: the carrier of ADG, the carrier of ADG:] is V11() set

o is Element of the carrier of (ADG,o9)

- o is Element of the carrier of (ADG,o9)

AS is Element of the carrier of ADG

(ADG,o9) . AS is Element of the carrier of ADG

(ADG,o9,o9) is Element of the carrier of ADG

(ADG,o9,AS) is Element of the carrier of ADG

(ADG,o9,AS,(ADG,o9,AS)) is Element of the carrier of ADG

X is Element of the carrier of (ADG,o9)

o + X is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,X) is Element of the carrier of (ADG,o9)

[o,X] is V15() set

the addF of (ADG,o9) . [o,X] is set

(ADG,o9) . (o,(ADG,o9,AS)) is set

[o,(ADG,o9,AS)] is V15() set

(ADG,o9) . [o,(ADG,o9,AS)] is set

0. (ADG,o9) is V52((ADG,o9)) Element of the carrier of (ADG,o9)

the ZeroF of (ADG,o9) is Element of the carrier of (ADG,o9)

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

0. (ADG,o9) is V52((ADG,o9)) Element of the carrier of (ADG,o9)

the carrier of (ADG,o9) is V11() set

the ZeroF of (ADG,o9) is Element of the carrier of (ADG,o9)

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

o is Element of the carrier of (ADG,o9)

AS is Element of the carrier of ADG

X is Element of the carrier of ADG

(ADG,o9,X,X) is Element of the carrier of ADG

Z is Element of the carrier of (ADG,o9)

Z + Z is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (Z,Z) is Element of the carrier of (ADG,o9)

[Z,Z] is V15() set

the addF of (ADG,o9) . [Z,Z] is set

ADG is non empty non trivial () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

o is Element of the carrier of (ADG,o9)

ADG is non empty non trivial AffVect-like () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict right_complementable Abelian add-associative right_zeroed Two_Divisible addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

0. (ADG,o9) is V52((ADG,o9)) Element of the carrier of (ADG,o9)

the ZeroF of (ADG,o9) is Element of the carrier of (ADG,o9)

o is Element of the carrier of (ADG,o9)

o + o is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,o) is Element of the carrier of (ADG,o9)

[o,o] is V15() set

the addF of (ADG,o9) . [o,o] is set

AS is Element of the carrier of ADG

(ADG,o9,AS,AS) is Element of the carrier of ADG

ADG is non empty non trivial AffVect-like () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict right_complementable Abelian add-associative right_zeroed Two_Divisible addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

the carrier of (ADG,o9) is V11() set

0. (ADG,o9) is V52((ADG,o9)) Element of the carrier of (ADG,o9)

the ZeroF of (ADG,o9) is Element of the carrier of (ADG,o9)

o is Element of the carrier of (ADG,o9)

o + o is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (o,o) is Element of the carrier of (ADG,o9)

[o,o] is V15() set

the addF of (ADG,o9) . [o,o] is set

o9 is Element of the carrier of G_Real

o is Element of the carrier of G_Real

ADG is non empty non trivial AffVect-like () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

ADG is non empty non trivial AffVect-like () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

ADG is non empty non trivial right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

AV ADG is non empty strict AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of ADG

ADG is non empty non trivial right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

AV ADG is non empty strict AffinStruct

ADG is non empty non trivial strict AffVect-like () AffinStruct

the carrier of ADG is V11() non trivial set

o9 is Element of the carrier of ADG

(ADG,o9) is non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

(ADG,o9) is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

addLoopStr(# the carrier of ADG,(ADG,o9),o9 #) is strict addLoopStr

AV (ADG,o9) is non empty non trivial strict AffVect-like () AffinStruct

AS is set

X is set

[AS,X] is V15() set

the CONGR of ADG is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined [: the carrier of ADG, the carrier of ADG:] -valued Element of bool [:[: the carrier of ADG, the carrier of ADG:],[: the carrier of ADG, the carrier of ADG:]:]

[:[: the carrier of ADG, the carrier of ADG:],[: the carrier of ADG, the carrier of ADG:]:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:],[: the carrier of ADG, the carrier of ADG:]:] is V11() set

[AS,X] `2 is set

X `1 is set

X `2 is set

[(X `1),(X `2)] is V15() set

[AS,X] `1 is set

AS `1 is set

AS `2 is set

the carrier of (ADG,o9) is V11() non trivial set

f is Element of the carrier of ADG

a is Element of the carrier of ADG

b is Element of the carrier of ADG

fa is Element of the carrier of ADG

[(AS `1),(AS `2)] is V15() set

z19 is Element of the carrier of (ADG,o9)

x2 is Element of the carrier of (ADG,o9)

z19 + x2 is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined the carrier of (ADG,o9) -valued Function-like V18([: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9)) Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):]

[: the carrier of (ADG,o9), the carrier of (ADG,o9):] is Relation-like V11() set

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):], the carrier of (ADG,o9):] is V11() set

the addF of (ADG,o9) . (z19,x2) is Element of the carrier of (ADG,o9)

[z19,x2] is V15() set

the addF of (ADG,o9) . [z19,x2] is set

z29 is Element of the carrier of (ADG,o9)

x1 is Element of the carrier of (ADG,o9)

z29 + x1 is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . (z29,x1) is Element of the carrier of (ADG,o9)

[z29,x1] is V15() set

the addF of (ADG,o9) . [z29,x1] is set

y1 is Element of the carrier of ADG

(ADG,o9,f,fa) is Element of the carrier of ADG

y2 is Element of the carrier of ADG

(ADG,o9,a,b) is Element of the carrier of ADG

CONGRD (ADG,o9) is Relation-like [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -defined [: the carrier of (ADG,o9), the carrier of (ADG,o9):] -valued Element of bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):],[: the carrier of (ADG,o9), the carrier of (ADG,o9):]:]

[:[: the carrier of (ADG,o9), the carrier of (ADG,o9):],[: the carrier of (ADG,o9), the carrier of (ADG,o9):]:] is Relation-like V11() set

bool [:[: the carrier of (ADG,o9), the carrier of (ADG,o9):],[: the carrier of (ADG,o9), the carrier of (ADG,o9):]:] is V11() set

f is Element of the carrier of (ADG,o9)

fa is Element of the carrier of (ADG,o9)

f + fa is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . (f,fa) is Element of the carrier of (ADG,o9)

[f,fa] is V15() set

the addF of (ADG,o9) . [f,fa] is set

a is Element of the carrier of (ADG,o9)

b is Element of the carrier of (ADG,o9)

a + b is Element of the carrier of (ADG,o9)

the addF of (ADG,o9) . (a,b) is Element of the carrier of (ADG,o9)

[a,b] is V15() set

the addF of (ADG,o9) . [a,b] is set

z2 is Element of the carrier of ADG

x2 is Element of the carrier of ADG

y1 is Element of the carrier of ADG

(ADG,o9,x2,y1) is Element of the carrier of ADG

z1 is Element of the carrier of ADG

x1 is Element of the carrier of ADG

y2 is Element of the carrier of ADG

(ADG,o9,x1,y2) is Element of the carrier of ADG

the carrier of (AV (ADG,o9)) is V11() non trivial set

ADG is strict AffinStruct

o9 is non empty non trivial AffVect-like () AffinStruct

the carrier of o9 is V11() non trivial set

the Element of the carrier of o9 is Element of the carrier of o9

(o9, the Element of the carrier of o9) is non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

(o9, the Element of the carrier of o9) is Relation-like [: the carrier of o9, the carrier of o9:] -defined the carrier of o9 -valued Function-like V18([: the carrier of o9, the carrier of o9:], the carrier of o9) Element of bool [:[: the carrier of o9, the carrier of o9:], the carrier of o9:]

[: the carrier of o9, the carrier of o9:] is Relation-like V11() set

[:[: the carrier of o9, the carrier of o9:], the carrier of o9:] is Relation-like V11() set

bool [:[: the carrier of o9, the carrier of o9:], the carrier of o9:] is V11() set

addLoopStr(# the carrier of o9,(o9, the Element of the carrier of o9), the Element of the carrier of o9 #) is strict addLoopStr

AS is non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

AV AS is non empty non trivial strict AffVect-like () AffinStruct

o9 is non empty non trivial right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

AV o9 is non empty non trivial strict AffVect-like () AffinStruct

AS is non empty non trivial right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

AV AS is non empty non trivial strict AffVect-like () AffinStruct

ADG is non empty addLoopStr

the carrier of ADG is V11() set

o9 is non empty addLoopStr

the carrier of o9 is V11() set

[: the carrier of ADG, the carrier of o9:] is Relation-like V11() set

bool [: the carrier of ADG, the carrier of o9:] is V11() set

ADG is non empty non trivial right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

the carrier of ADG is V11() non trivial set

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

bool [: the carrier of ADG, the carrier of ADG:] is V11() set

AV ADG is non empty non trivial strict AffVect-like () AffinStruct

the carrier of (AV ADG) is V11() non trivial set

0. ADG is V52(ADG) Element of the carrier of ADG

the ZeroF of ADG is Element of the carrier of ADG

o9 is Relation-like the carrier of ADG -defined the carrier of ADG -valued Function-like V18( the carrier of ADG, the carrier of ADG) Element of bool [: the carrier of ADG, the carrier of ADG:]

o9 . (0. ADG) is Element of the carrier of ADG

o is Element of the carrier of ADG

AS is Element of the carrier of (AV ADG)

((AV ADG),AS) is Relation-like [: the carrier of (AV ADG), the carrier of (AV ADG):] -defined the carrier of (AV ADG) -valued Function-like V18([: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG)) Element of bool [:[: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG):]

[: the carrier of (AV ADG), the carrier of (AV ADG):] is Relation-like V11() set

[:[: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG):] is Relation-like V11() set

bool [:[: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG):] is V11() set

((AV ADG),AS) is non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

addLoopStr(# the carrier of (AV ADG),((AV ADG),AS),AS #) is strict addLoopStr

0. ((AV ADG),AS) is V52(((AV ADG),AS)) Element of the carrier of ((AV ADG),AS)

the carrier of ((AV ADG),AS) is V11() non trivial set

the ZeroF of ((AV ADG),AS) is Element of the carrier of ((AV ADG),AS)

((AV ADG),AS) is Relation-like the carrier of (AV ADG) -defined the carrier of (AV ADG) -valued Function-like V18( the carrier of (AV ADG), the carrier of (AV ADG)) Element of bool [: the carrier of (AV ADG), the carrier of (AV ADG):]

bool [: the carrier of (AV ADG), the carrier of (AV ADG):] is V11() set

X is Element of the carrier of ADG

Z is Element of the carrier of ADG

X + Z is Element of the carrier of ADG

the addF of ADG is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

the addF of ADG . (X,Z) is Element of the carrier of ADG

[X,Z] is V15() set

the addF of ADG . [X,Z] is set

o9 . (X + Z) is Element of the carrier of ADG

o9 . X is Element of the carrier of ADG

o9 . Z is Element of the carrier of ADG

((AV ADG),AS) . ((o9 . X),(o9 . Z)) is set

[(o9 . X),(o9 . Z)] is V15() set

((AV ADG),AS) . [(o9 . X),(o9 . Z)] is set

- X is Element of the carrier of ADG

o9 . (- X) is Element of the carrier of ADG

((AV ADG),AS) . (o9 . X) is set

CONGRD ADG is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined [: the carrier of ADG, the carrier of ADG:] -valued Element of bool [:[: the carrier of ADG, the carrier of ADG:],[: the carrier of ADG, the carrier of ADG:]:]

[:[: the carrier of ADG, the carrier of ADG:],[: the carrier of ADG, the carrier of ADG:]:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:],[: the carrier of ADG, the carrier of ADG:]:] is V11() set

AffinStruct(# the carrier of ADG,(CONGRD ADG) #) is strict AffinStruct

f is Element of the carrier of (AV ADG)

a is Element of the carrier of (AV ADG)

((AV ADG),AS,f,a) is Element of the carrier of (AV ADG)

b is Element of the carrier of (AV ADG)

[o,(o9 . X)] is V15() set

fa is Element of the carrier of ADG

[(o9 . Z),fa] is V15() set

[[o,(o9 . X)],[(o9 . Z),fa]] is V15() set

o + fa is Element of the carrier of ADG

the addF of ADG . (o,fa) is Element of the carrier of ADG

[o,fa] is V15() set

the addF of ADG . [o,fa] is set

(o9 . X) + (o9 . Z) is Element of the carrier of ADG

the addF of ADG . ((o9 . X),(o9 . Z)) is Element of the carrier of ADG

the addF of ADG . [(o9 . X),(o9 . Z)] is set

o + X is Element of the carrier of ADG

the addF of ADG . (o,X) is Element of the carrier of ADG

[o,X] is V15() set

the addF of ADG . [o,X] is set

o + Z is Element of the carrier of ADG

the addF of ADG . (o,Z) is Element of the carrier of ADG

[o,Z] is V15() set

the addF of ADG . [o,Z] is set

X + o is Element of the carrier of ADG

the addF of ADG . (X,o) is Element of the carrier of ADG

[X,o] is V15() set

the addF of ADG . [X,o] is set

(X + o) + Z is Element of the carrier of ADG

the addF of ADG . ((X + o),Z) is Element of the carrier of ADG

[(X + o),Z] is V15() set

the addF of ADG . [(X + o),Z] is set

o + ((X + o) + Z) is Element of the carrier of ADG

the addF of ADG . (o,((X + o) + Z)) is Element of the carrier of ADG

[o,((X + o) + Z)] is V15() set

the addF of ADG . [o,((X + o) + Z)] is set

o + (X + Z) is Element of the carrier of ADG

the addF of ADG . (o,(X + Z)) is Element of the carrier of ADG

[o,(X + Z)] is V15() set

the addF of ADG . [o,(X + Z)] is set

o + (o + (X + Z)) is Element of the carrier of ADG

the addF of ADG . (o,(o + (X + Z))) is Element of the carrier of ADG

[o,(o + (X + Z))] is V15() set

the addF of ADG . [o,(o + (X + Z))] is set

o + (0. ADG) is Element of the carrier of ADG

the addF of ADG . (o,(0. ADG)) is Element of the carrier of ADG

[o,(0. ADG)] is V15() set

the addF of ADG . [o,(0. ADG)] is set

f is Element of the carrier of (AV ADG)

((AV ADG),AS,f) is Element of the carrier of (AV ADG)

b is Element of the carrier of (AV ADG)

[(o9 . X),o] is V15() set

fa is Element of the carrier of ADG

[o,fa] is V15() set

[[(o9 . X),o],[o,fa]] is V15() set

(o9 . X) + fa is Element of the carrier of ADG

the addF of ADG . ((o9 . X),fa) is Element of the carrier of ADG

[(o9 . X),fa] is V15() set

the addF of ADG . [(o9 . X),fa] is set

o + o is Element of the carrier of ADG

the addF of ADG . (o,o) is Element of the carrier of ADG

[o,o] is V15() set

the addF of ADG . [o,o] is set

o + X is Element of the carrier of ADG

the addF of ADG . (o,X) is Element of the carrier of ADG

[o,X] is V15() set

the addF of ADG . [o,X] is set

(o + X) + fa is Element of the carrier of ADG

the addF of ADG . ((o + X),fa) is Element of the carrier of ADG

[(o + X),fa] is V15() set

the addF of ADG . [(o + X),fa] is set

X + fa is Element of the carrier of ADG

the addF of ADG . (X,fa) is Element of the carrier of ADG

[X,fa] is V15() set

the addF of ADG . [X,fa] is set

o + (X + fa) is Element of the carrier of ADG

the addF of ADG . (o,(X + fa)) is Element of the carrier of ADG

[o,(X + fa)] is V15() set

the addF of ADG . [o,(X + fa)] is set

o + (- X) is Element of the carrier of ADG

the addF of ADG . (o,(- X)) is Element of the carrier of ADG

[o,(- X)] is V15() set

the addF of ADG . [o,(- X)] is set

fa + X is Element of the carrier of ADG

the addF of ADG . (fa,X) is Element of the carrier of ADG

[fa,X] is V15() set

the addF of ADG . [fa,X] is set

(fa + X) + (- X) is Element of the carrier of ADG

the addF of ADG . ((fa + X),(- X)) is Element of the carrier of ADG

[(fa + X),(- X)] is V15() set

the addF of ADG . [(fa + X),(- X)] is set

X + (- X) is Element of the carrier of ADG

the addF of ADG . (X,(- X)) is Element of the carrier of ADG

[X,(- X)] is V15() set

the addF of ADG . [X,(- X)] is set

fa + (X + (- X)) is Element of the carrier of ADG

the addF of ADG . (fa,(X + (- X))) is Element of the carrier of ADG

[fa,(X + (- X))] is V15() set

the addF of ADG . [fa,(X + (- X))] is set

fa + (0. ADG) is Element of the carrier of ADG

the addF of ADG . (fa,(0. ADG)) is Element of the carrier of ADG

[fa,(0. ADG)] is V15() set

the addF of ADG . [fa,(0. ADG)] is set

ADG is non empty non trivial right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

the carrier of ADG is V11() non trivial set

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

bool [: the carrier of ADG, the carrier of ADG:] is V11() set

o9 is Relation-like the carrier of ADG -defined the carrier of ADG -valued Function-like V18( the carrier of ADG, the carrier of ADG) Element of bool [: the carrier of ADG, the carrier of ADG:]

o is Element of the carrier of ADG

AS is set

proj1 o9 is set

X is set

o9 . AS is set

o9 . X is set

T is Element of the carrier of ADG

o + T is Element of the carrier of ADG

the addF of ADG is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

the addF of ADG . (o,T) is Element of the carrier of ADG

[o,T] is V15() set

the addF of ADG . [o,T] is set

Z is Element of the carrier of ADG

o9 . Z is Element of the carrier of ADG

o + Z is Element of the carrier of ADG

the addF of ADG . (o,Z) is Element of the carrier of ADG

[o,Z] is V15() set

the addF of ADG . [o,Z] is set

ADG is non empty non trivial right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

the carrier of ADG is V11() non trivial set

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

bool [: the carrier of ADG, the carrier of ADG:] is V11() set

AV ADG is non empty non trivial strict AffVect-like () AffinStruct

the carrier of (AV ADG) is V11() non trivial set

o9 is Relation-like the carrier of ADG -defined the carrier of ADG -valued Function-like V18( the carrier of ADG, the carrier of ADG) Element of bool [: the carrier of ADG, the carrier of ADG:]

rng o9 is set

proj1 o9 is set

AS is Element of the carrier of ADG

X is Element of the carrier of (AV ADG)

((AV ADG),X) is non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

((AV ADG),X) is Relation-like [: the carrier of (AV ADG), the carrier of (AV ADG):] -defined the carrier of (AV ADG) -valued Function-like V18([: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG)) Element of bool [:[: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG):]

[: the carrier of (AV ADG), the carrier of (AV ADG):] is Relation-like V11() set

[:[: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG):] is Relation-like V11() set

bool [:[: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG):] is V11() set

addLoopStr(# the carrier of (AV ADG),((AV ADG),X),X #) is strict addLoopStr

the carrier of ((AV ADG),X) is V11() non trivial set

Z is set

T is Element of the carrier of ADG

T - AS is Element of the carrier of ADG

- AS is Element of the carrier of ADG

T + (- AS) is Element of the carrier of ADG

the addF of ADG is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

the addF of ADG . (T,(- AS)) is Element of the carrier of ADG

[T,(- AS)] is V15() set

the addF of ADG . [T,(- AS)] is set

o9 . (T - AS) is Element of the carrier of ADG

(- AS) + T is Element of the carrier of ADG

the addF of ADG . ((- AS),T) is Element of the carrier of ADG

[(- AS),T] is V15() set

the addF of ADG . [(- AS),T] is set

AS + ((- AS) + T) is Element of the carrier of ADG

the addF of ADG . (AS,((- AS) + T)) is Element of the carrier of ADG

[AS,((- AS) + T)] is V15() set

the addF of ADG . [AS,((- AS) + T)] is set

AS + (- AS) is Element of the carrier of ADG

the addF of ADG . (AS,(- AS)) is Element of the carrier of ADG

[AS,(- AS)] is V15() set

the addF of ADG . [AS,(- AS)] is set

(AS + (- AS)) + T is Element of the carrier of ADG

the addF of ADG . ((AS + (- AS)),T) is Element of the carrier of ADG

[(AS + (- AS)),T] is V15() set

the addF of ADG . [(AS + (- AS)),T] is set

0. ADG is V52(ADG) Element of the carrier of ADG

the ZeroF of ADG is Element of the carrier of ADG

T + (0. ADG) is Element of the carrier of ADG

the addF of ADG . (T,(0. ADG)) is Element of the carrier of ADG

[T,(0. ADG)] is V15() set

the addF of ADG . [T,(0. ADG)] is set

ADG is non empty non trivial right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

the carrier of ADG is V11() non trivial set

AV ADG is non empty non trivial strict AffVect-like () AffinStruct

the carrier of (AV ADG) is V11() non trivial set

o9 is Element of the carrier of ADG

o is Element of the carrier of (AV ADG)

((AV ADG),o) is non empty non trivial strict right_complementable Abelian add-associative right_zeroed Fanoian Two_Divisible addLoopStr

((AV ADG),o) is Relation-like [: the carrier of (AV ADG), the carrier of (AV ADG):] -defined the carrier of (AV ADG) -valued Function-like V18([: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG)) Element of bool [:[: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG):]

[: the carrier of (AV ADG), the carrier of (AV ADG):] is Relation-like V11() set

[:[: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG):] is Relation-like V11() set

bool [:[: the carrier of (AV ADG), the carrier of (AV ADG):], the carrier of (AV ADG):] is V11() set

addLoopStr(# the carrier of (AV ADG),((AV ADG),o),o #) is strict addLoopStr

the carrier of ((AV ADG),o) is V11() non trivial set

[: the carrier of ADG, the carrier of ADG:] is Relation-like V11() set

bool [: the carrier of ADG, the carrier of ADG:] is V11() set

g is Relation-like the carrier of ADG -defined the carrier of ADG -valued Function-like V18( the carrier of ADG, the carrier of ADG) Element of bool [: the carrier of ADG, the carrier of ADG:]

[: the carrier of ADG, the carrier of ((AV ADG),o):] is Relation-like V11() set

bool [: the carrier of ADG, the carrier of ((AV ADG),o):] is V11() set

f is Relation-like the carrier of ADG -defined the carrier of ((AV ADG),o) -valued Function-like V18( the carrier of ADG, the carrier of ((AV ADG),o)) Element of bool [: the carrier of ADG, the carrier of ((AV ADG),o):]

a is Element of the carrier of ADG

f . a is Element of the carrier of ((AV ADG),o)

b is Element of the carrier of ADG

a + b is Element of the carrier of ADG

the addF of ADG is Relation-like [: the carrier of ADG, the carrier of ADG:] -defined the carrier of ADG -valued Function-like V18([: the carrier of ADG, the carrier of ADG:], the carrier of ADG) Element of bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:]

[:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is Relation-like V11() set

bool [:[: the carrier of ADG, the carrier of ADG:], the carrier of ADG:] is V11() set

the addF of ADG . (a,b) is Element of the carrier of ADG

[a,b] is V15() set

the addF of ADG . [a,b] is set

f . (a + b) is Element of the carrier of ((AV ADG),o)

f . b is Element of the carrier of ((AV ADG),o)

(f . a) +