:: 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) + (f . b) is Element of the carrier of ((AV ADG),o)
the addF of ((AV ADG),o) is Relation-like [: the carrier of ((AV ADG),o), the carrier of ((AV ADG),o):] -defined the carrier of ((AV ADG),o) -valued Function-like V18([: the carrier of ((AV ADG),o), the carrier of ((AV ADG),o):], the carrier of ((AV ADG),o)) Element of bool [:[: the carrier of ((AV ADG),o), the carrier of ((AV ADG),o):], the carrier of ((AV ADG),o):]
[: the carrier of ((AV ADG),o), the carrier of ((AV ADG),o):] is Relation-like V11() set
[:[: the carrier of ((AV ADG),o), the carrier of ((AV ADG),o):], the carrier of ((AV ADG),o):] is Relation-like V11() set
bool [:[: the carrier of ((AV ADG),o), the carrier of ((AV ADG),o):], the carrier of ((AV ADG),o):] is V11() set
the addF of ((AV ADG),o) . ((f . a),(f . b)) is Element of the carrier of ((AV ADG),o)
[(f . a),(f . b)] is V15() set
the addF of ((AV ADG),o) . [(f . a),(f . b)] is set
0. ADG is V52(ADG) Element of the carrier of ADG
the ZeroF of ADG is Element of the carrier of ADG
f . (0. ADG) is Element of the carrier of ((AV ADG),o)
0. ((AV ADG),o) is V52(((AV ADG),o)) Element of the carrier of ((AV ADG),o)
the ZeroF of ((AV ADG),o) is Element of 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)
((AV ADG),o) 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
fa is Element of the carrier of (AV ADG)
((AV ADG),o) . fa is Element of the carrier of (AV ADG)
- (f . a) is Element of the carrier of ((AV ADG),o)
rng f is set