REAL is non empty V35() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V35() V40() V41() Element of bool REAL
bool REAL is non empty V35() set
{} is set
the Relation-like non-empty empty-yielding functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() ext-real non positive non negative V35() V40() V42( {} ) V79() FinSequence-like FinSequence-membered integer set is Relation-like non-empty empty-yielding functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() ext-real non positive non negative V35() V40() V42( {} ) V79() FinSequence-like FinSequence-membered integer set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() ext-real positive non negative V35() V40() V79() integer Element of NAT
{{},1} is set
[:1,1:] is Relation-like non empty set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is Relation-like non empty set
bool [:[:1,1:],1:] is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V35() V40() V41() set
bool omega is non empty V35() set
bool NAT is non empty V35() set
COMPLEX is non empty V35() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V31() ext-real positive non negative V35() V40() V79() integer Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V31() ext-real positive non negative V35() V40() V79() integer Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
{{}} is non empty trivial V42(1) set
INT is non empty V35() set
the non empty set is non empty set
the Element of the non empty set is Element of the non empty set
[: the non empty set , the non empty set :] is Relation-like non empty set
[:[: the non empty set , the non empty set :], the non empty set :] is Relation-like non empty set
bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set
the Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
[:INT, the non empty set :] is Relation-like non empty V35() set
[:[:INT, the non empty set :], the non empty set :] is Relation-like non empty V35() set
bool [:[:INT, the non empty set :], the non empty set :] is non empty V35() set
the Relation-like Function-like V18([:INT, the non empty set :], the non empty set ) Element of bool [:[:INT, the non empty set :], the non empty set :] is Relation-like Function-like V18([:INT, the non empty set :], the non empty set ) Element of bool [:[:INT, the non empty set :], the non empty set :]
( the non empty set , the Element of the non empty set , the Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like Function-like V18([:INT, the non empty set :], the non empty set ) Element of bool [:[:INT, the non empty set :], the non empty set :]) is () ()
the carrier of ( the non empty set , the Element of the non empty set , the Relation-like Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like Function-like V18([:INT, the non empty set :], the non empty set ) Element of bool [:[:INT, the non empty set :], the non empty set :]) is set
AG is non empty ()
the carrier of AG is non empty set
the of AG is Relation-like Function-like V18([:INT, the carrier of AG:], the carrier of AG) Element of bool [:[:INT, the carrier of AG:], the carrier of AG:]
[:INT, the carrier of AG:] is Relation-like non empty V35() set
[:[:INT, the carrier of AG:], the carrier of AG:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of AG:], the carrier of AG:] is non empty V35() set
ML is V31() ext-real V79() integer set
ZS is Element of the carrier of AG
the of AG . (ML,ZS) is set
[ML,ZS] is set
{ML,ZS} is set
{ML} is non empty trivial V42(1) set
{{ML,ZS},{ML}} is set
the of AG . [ML,ZS] is set
AD is V31() ext-real V79() integer Element of INT
the of AG . (AD,ZS) is Element of the carrier of AG
[AD,ZS] is set
{AD,ZS} is set
{AD} is non empty trivial V42(1) set
{{AD,ZS},{AD}} is set
the of AG . [AD,ZS] is set
AG is non empty set
[:AG,AG:] is Relation-like non empty set
[:[:AG,AG:],AG:] is Relation-like non empty set
bool [:[:AG,AG:],AG:] is non empty set
[:INT,AG:] is Relation-like non empty V35() set
[:[:INT,AG:],AG:] is Relation-like non empty V35() set
bool [:[:INT,AG:],AG:] is non empty V35() set
ZS is Element of AG
ML is Relation-like Function-like V18([:AG,AG:],AG) Element of bool [:[:AG,AG:],AG:]
AD is Relation-like Function-like V18([:INT,AG:],AG) Element of bool [:[:INT,AG:],AG:]
(AG,ZS,ML,AD) is () ()
op0 is epsilon-transitive epsilon-connected ordinal Element of 1
op2 is Relation-like Function-like V18([:1,1:],1) Element of bool [:[:1,1:],1:]
pr2 (INT,1) is Relation-like Function-like V18([:INT,1:],1) Element of bool [:[:INT,1:],1:]
[:INT,1:] is Relation-like non empty V35() set
[:[:INT,1:],1:] is Relation-like non empty V35() set
bool [:[:INT,1:],1:] is non empty V35() set
(1,op0,op2,(pr2 (INT,1))) is non empty () ()
() is () ()
AG is non empty trivial V50() 1 -element left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () ()
the carrier of AG is non empty trivial V35() V42(1) set
AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
ZS is V31() ext-real V79() integer set
ML is V31() ext-real V79() integer set
ZS + ML is V31() ext-real V79() integer set
(AG,AD,(ZS + ML)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG is Relation-like Function-like V18([:INT, the carrier of AG:], the carrier of AG) Element of bool [:[:INT, the carrier of AG:], the carrier of AG:]
[:INT, the carrier of AG:] is Relation-like non empty V35() set
[:[:INT, the carrier of AG:], the carrier of AG:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of AG:], the carrier of AG:] is non empty V35() set
the of AG . ((ZS + ML),AD) is set
[(ZS + ML),AD] is set
{(ZS + ML),AD} is set
{(ZS + ML)} is non empty trivial V42(1) set
{{(ZS + ML),AD},{(ZS + ML)}} is set
the of AG . [(ZS + ML),AD] is set
(AG,AD,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . (ZS,AD) is set
[ZS,AD] is set
{ZS,AD} is set
{ZS} is non empty trivial V42(1) set
{{ZS,AD},{ZS}} is set
the of AG . [ZS,AD] is set
(AG,AD,ML) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . (ML,AD) is set
[ML,AD] is set
{ML,AD} is set
{ML} is non empty trivial V42(1) set
{{ML,AD},{ML}} is set
the of AG . [ML,AD] is set
(AG,AD,ZS) + (AG,AD,ML) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG is Relation-like Function-like V18([: the carrier of AG, the carrier of AG:], the carrier of AG) Element of bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:]
[: the carrier of AG, the carrier of AG:] is Relation-like non empty set
[:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is Relation-like non empty set
bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is non empty set
the addF of AG . ((AG,AD,ZS),(AG,AD,ML)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[(AG,AD,ZS),(AG,AD,ML)] is set
{(AG,AD,ZS),(AG,AD,ML)} is set
{(AG,AD,ZS)} is non empty trivial V42(1) set
{{(AG,AD,ZS),(AG,AD,ML)},{(AG,AD,ZS)}} is set
the addF of AG . [(AG,AD,ZS),(AG,AD,ML)] is set
ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
ML + AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG is Relation-like Function-like V18([: the carrier of AG, the carrier of AG:], the carrier of AG) Element of bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:]
[: the carrier of AG, the carrier of AG:] is Relation-like non empty set
[:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is Relation-like non empty set
bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is non empty set
the addF of AG . (ML,AD) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[ML,AD] is set
{ML,AD} is set
{ML} is non empty trivial V42(1) set
{{ML,AD},{ML}} is set
the addF of AG . [ML,AD] is set
ZS is V31() ext-real V79() integer set
(AG,(ML + AD),ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG is Relation-like Function-like V18([:INT, the carrier of AG:], the carrier of AG) Element of bool [:[:INT, the carrier of AG:], the carrier of AG:]
[:INT, the carrier of AG:] is Relation-like non empty V35() set
[:[:INT, the carrier of AG:], the carrier of AG:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of AG:], the carrier of AG:] is non empty V35() set
the of AG . (ZS,(ML + AD)) is set
[ZS,(ML + AD)] is set
{ZS,(ML + AD)} is set
{ZS} is non empty trivial V42(1) set
{{ZS,(ML + AD)},{ZS}} is set
the of AG . [ZS,(ML + AD)] is set
(AG,ML,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . (ZS,ML) is set
[ZS,ML] is set
{ZS,ML} is set
{{ZS,ML},{ZS}} is set
the of AG . [ZS,ML] is set
(AG,AD,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . (ZS,AD) is set
[ZS,AD] is set
{ZS,AD} is set
{{ZS,AD},{ZS}} is set
the of AG . [ZS,AD] is set
(AG,ML,ZS) + (AG,AD,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG . ((AG,ML,ZS),(AG,AD,ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[(AG,ML,ZS),(AG,AD,ZS)] is set
{(AG,ML,ZS),(AG,AD,ZS)} is set
{(AG,ML,ZS)} is non empty trivial V42(1) set
{{(AG,ML,ZS),(AG,AD,ZS)},{(AG,ML,ZS)}} is set
the addF of AG . [(AG,ML,ZS),(AG,AD,ZS)] is set
AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
ZS is V31() ext-real V79() integer set
ML is V31() ext-real V79() integer set
ZS * ML is V31() ext-real V79() integer set
(AG,AD,(ZS * ML)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG is Relation-like Function-like V18([:INT, the carrier of AG:], the carrier of AG) Element of bool [:[:INT, the carrier of AG:], the carrier of AG:]
[:INT, the carrier of AG:] is Relation-like non empty V35() set
[:[:INT, the carrier of AG:], the carrier of AG:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of AG:], the carrier of AG:] is non empty V35() set
the of AG . ((ZS * ML),AD) is set
[(ZS * ML),AD] is set
{(ZS * ML),AD} is set
{(ZS * ML)} is non empty trivial V42(1) set
{{(ZS * ML),AD},{(ZS * ML)}} is set
the of AG . [(ZS * ML),AD] is set
(AG,AD,ML) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . (ML,AD) is set
[ML,AD] is set
{ML,AD} is set
{ML} is non empty trivial V42(1) set
{{ML,AD},{ML}} is set
the of AG . [ML,AD] is set
(AG,(AG,AD,ML),ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . (ZS,(AG,AD,ML)) is set
[ZS,(AG,AD,ML)] is set
{ZS,(AG,AD,ML)} is set
{ZS} is non empty trivial V42(1) set
{{ZS,(AG,AD,ML)},{ZS}} is set
the of AG . [ZS,(AG,AD,ML)] is set
ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
(AG,ZS,1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG is Relation-like Function-like V18([:INT, the carrier of AG:], the carrier of AG) Element of bool [:[:INT, the carrier of AG:], the carrier of AG:]
[:INT, the carrier of AG:] is Relation-like non empty V35() set
[:[:INT, the carrier of AG:], the carrier of AG:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of AG:], the carrier of AG:] is non empty V35() set
the of AG . (1,ZS) is set
[1,ZS] is set
{1,ZS} is set
{1} is non empty trivial V42(1) set
{{1,ZS},{1}} is set
the of AG . [1,ZS] is set
AG is V31() ext-real V79() integer set
ZS is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of ZS is non empty set
0. ZS is V51(ZS) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the ZeroF of ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,ML,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS is Relation-like Function-like V18([:INT, the carrier of ZS:], the carrier of ZS) Element of bool [:[:INT, the carrier of ZS:], the carrier of ZS:]
[:INT, the carrier of ZS:] is Relation-like non empty V35() set
[:[:INT, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of ZS:], the carrier of ZS:] is non empty V35() set
the of ZS . (AG,ML) is set
[AG,ML] is set
{AG,ML} is set
{AG} is non empty trivial V42(1) set
{{AG,ML},{AG}} is set
the of ZS . [AG,ML] is set
CA is V31() ext-real V79() integer set
(ZS,ML,CA) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (CA,ML) is set
[CA,ML] is set
{CA,ML} is set
{CA} is non empty trivial V42(1) set
{{CA,ML},{CA}} is set
the of ZS . [CA,ML] is set
ML + (ZS,ML,CA) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS is Relation-like Function-like V18([: the carrier of ZS, the carrier of ZS:], the carrier of ZS) Element of bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:]
[: the carrier of ZS, the carrier of ZS:] is Relation-like non empty set
[:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty set
bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is non empty set
the addF of ZS . (ML,(ZS,ML,CA)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[ML,(ZS,ML,CA)] is set
{ML,(ZS,ML,CA)} is set
{ML} is non empty trivial V42(1) set
{{ML,(ZS,ML,CA)},{ML}} is set
the addF of ZS . [ML,(ZS,ML,CA)] is set
AD is V31() ext-real V79() integer set
(ZS,ML,AD) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AD,ML) is set
[AD,ML] is set
{AD,ML} is set
{AD} is non empty trivial V42(1) set
{{AD,ML},{AD}} is set
the of ZS . [AD,ML] is set
(ZS,ML,AD) + (ZS,ML,CA) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS . ((ZS,ML,AD),(ZS,ML,CA)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(ZS,ML,AD),(ZS,ML,CA)] is set
{(ZS,ML,AD),(ZS,ML,CA)} is set
{(ZS,ML,AD)} is non empty trivial V42(1) set
{{(ZS,ML,AD),(ZS,ML,CA)},{(ZS,ML,AD)}} is set
the addF of ZS . [(ZS,ML,AD),(ZS,ML,CA)] is set
AD + CA is V31() ext-real V79() integer set
(ZS,ML,(AD + CA)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . ((AD + CA),ML) is set
[(AD + CA),ML] is set
{(AD + CA),ML} is set
{(AD + CA)} is non empty trivial V42(1) set
{{(AD + CA),ML},{(AD + CA)}} is set
the of ZS . [(AD + CA),ML] is set
ML + (0. ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS . (ML,(0. ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[ML,(0. ZS)] is set
{ML,(0. ZS)} is set
{{ML,(0. ZS)},{ML}} is set
the addF of ZS . [ML,(0. ZS)] is set
(ZS,(0. ZS),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,(0. ZS)) is set
[AG,(0. ZS)] is set
{AG,(0. ZS)} is set
{{AG,(0. ZS)},{AG}} is set
the of ZS . [AG,(0. ZS)] is set
(ZS,(0. ZS),AG) + (ZS,(0. ZS),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS is Relation-like Function-like V18([: the carrier of ZS, the carrier of ZS:], the carrier of ZS) Element of bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:]
[: the carrier of ZS, the carrier of ZS:] is Relation-like non empty set
[:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty set
bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is non empty set
the addF of ZS . ((ZS,(0. ZS),AG),(ZS,(0. ZS),AG)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(ZS,(0. ZS),AG),(ZS,(0. ZS),AG)] is set
{(ZS,(0. ZS),AG),(ZS,(0. ZS),AG)} is set
{(ZS,(0. ZS),AG)} is non empty trivial V42(1) set
{{(ZS,(0. ZS),AG),(ZS,(0. ZS),AG)},{(ZS,(0. ZS),AG)}} is set
the addF of ZS . [(ZS,(0. ZS),AG),(ZS,(0. ZS),AG)] is set
(0. ZS) + (0. ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS . ((0. ZS),(0. ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(0. ZS),(0. ZS)] is set
{(0. ZS),(0. ZS)} is set
{(0. ZS)} is non empty trivial V42(1) set
{{(0. ZS),(0. ZS)},{(0. ZS)}} is set
the addF of ZS . [(0. ZS),(0. ZS)] is set
(ZS,((0. ZS) + (0. ZS)),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,((0. ZS) + (0. ZS))) is set
[AG,((0. ZS) + (0. ZS))] is set
{AG,((0. ZS) + (0. ZS))} is set
{{AG,((0. ZS) + (0. ZS))},{AG}} is set
the of ZS . [AG,((0. ZS) + (0. ZS))] is set
(ZS,(0. ZS),AG) + (0. ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS . ((ZS,(0. ZS),AG),(0. ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(ZS,(0. ZS),AG),(0. ZS)] is set
{(ZS,(0. ZS),AG),(0. ZS)} is set
{{(ZS,(0. ZS),AG),(0. ZS)},{(ZS,(0. ZS),AG)}} is set
the addF of ZS . [(ZS,(0. ZS),AG),(0. ZS)] is set
- 1 is V31() ext-real non positive V79() integer set
AG is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of AG is non empty set
ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
- ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
(AG,ZS,(- 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG is Relation-like Function-like V18([:INT, the carrier of AG:], the carrier of AG) Element of bool [:[:INT, the carrier of AG:], the carrier of AG:]
[:INT, the carrier of AG:] is Relation-like non empty V35() set
[:[:INT, the carrier of AG:], the carrier of AG:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of AG:], the carrier of AG:] is non empty V35() set
the of AG . ((- 1),ZS) is set
[(- 1),ZS] is set
{(- 1),ZS} is set
{(- 1)} is non empty trivial V42(1) set
{{(- 1),ZS},{(- 1)}} is set
the of AG . [(- 1),ZS] is set
ZS + (AG,ZS,(- 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG is Relation-like Function-like V18([: the carrier of AG, the carrier of AG:], the carrier of AG) Element of bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:]
[: the carrier of AG, the carrier of AG:] is Relation-like non empty set
[:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is Relation-like non empty set
bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is non empty set
the addF of AG . (ZS,(AG,ZS,(- 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[ZS,(AG,ZS,(- 1))] is set
{ZS,(AG,ZS,(- 1))} is set
{ZS} is non empty trivial V42(1) set
{{ZS,(AG,ZS,(- 1))},{ZS}} is set
the addF of AG . [ZS,(AG,ZS,(- 1))] is set
(AG,ZS,1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . (1,ZS) is set
[1,ZS] is set
{1,ZS} is set
{1} is non empty trivial V42(1) set
{{1,ZS},{1}} is set
the of AG . [1,ZS] is set
(AG,ZS,1) + (AG,ZS,(- 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG . ((AG,ZS,1),(AG,ZS,(- 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[(AG,ZS,1),(AG,ZS,(- 1))] is set
{(AG,ZS,1),(AG,ZS,(- 1))} is set
{(AG,ZS,1)} is non empty trivial V42(1) set
{{(AG,ZS,1),(AG,ZS,(- 1))},{(AG,ZS,1)}} is set
the addF of AG . [(AG,ZS,1),(AG,ZS,(- 1))] is set
1 + (- 1) is V31() ext-real V79() integer set
(AG,ZS,(1 + (- 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . ((1 + (- 1)),ZS) is set
[(1 + (- 1)),ZS] is set
{(1 + (- 1)),ZS} is set
{(1 + (- 1))} is non empty trivial V42(1) set
{{(1 + (- 1)),ZS},{(1 + (- 1))}} is set
the of AG . [(1 + (- 1)),ZS] is set
0. AG is V51(AG) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the ZeroF of AG is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
(- ZS) + (ZS + (AG,ZS,(- 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG . ((- ZS),(ZS + (AG,ZS,(- 1)))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[(- ZS),(ZS + (AG,ZS,(- 1)))] is set
{(- ZS),(ZS + (AG,ZS,(- 1)))} is set
{(- ZS)} is non empty trivial V42(1) set
{{(- ZS),(ZS + (AG,ZS,(- 1)))},{(- ZS)}} is set
the addF of AG . [(- ZS),(ZS + (AG,ZS,(- 1)))] is set
(- ZS) + ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG . ((- ZS),ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[(- ZS),ZS] is set
{(- ZS),ZS} is set
{{(- ZS),ZS},{(- ZS)}} is set
the addF of AG . [(- ZS),ZS] is set
((- ZS) + ZS) + (AG,ZS,(- 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG . (((- ZS) + ZS),(AG,ZS,(- 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[((- ZS) + ZS),(AG,ZS,(- 1))] is set
{((- ZS) + ZS),(AG,ZS,(- 1))} is set
{((- ZS) + ZS)} is non empty trivial V42(1) set
{{((- ZS) + ZS),(AG,ZS,(- 1))},{((- ZS) + ZS)}} is set
the addF of AG . [((- ZS) + ZS),(AG,ZS,(- 1))] is set
(0. AG) + (AG,ZS,(- 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG . ((0. AG),(AG,ZS,(- 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[(0. AG),(AG,ZS,(- 1))] is set
{(0. AG),(AG,ZS,(- 1))} is set
{(0. AG)} is non empty trivial V42(1) set
{{(0. AG),(AG,ZS,(- 1))},{(0. AG)}} is set
the addF of AG . [(0. AG),(AG,ZS,(- 1))] is set
AG is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of AG is non empty set
0. AG is V51(AG) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the ZeroF of AG is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
- ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
ZS + ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG is Relation-like Function-like V18([: the carrier of AG, the carrier of AG:], the carrier of AG) Element of bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:]
[: the carrier of AG, the carrier of AG:] is Relation-like non empty set
[:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is Relation-like non empty set
bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is non empty set
the addF of AG . (ZS,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[ZS,ZS] is set
{ZS,ZS} is set
{ZS} is non empty trivial V42(1) set
{{ZS,ZS},{ZS}} is set
the addF of AG . [ZS,ZS] is set
(AG,ZS,1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG is Relation-like Function-like V18([:INT, the carrier of AG:], the carrier of AG) Element of bool [:[:INT, the carrier of AG:], the carrier of AG:]
[:INT, the carrier of AG:] is Relation-like non empty V35() set
[:[:INT, the carrier of AG:], the carrier of AG:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of AG:], the carrier of AG:] is non empty V35() set
the of AG . (1,ZS) is set
[1,ZS] is set
{1,ZS} is set
{1} is non empty trivial V42(1) set
{{1,ZS},{1}} is set
the of AG . [1,ZS] is set
(AG,ZS,1) + ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG . ((AG,ZS,1),ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[(AG,ZS,1),ZS] is set
{(AG,ZS,1),ZS} is set
{(AG,ZS,1)} is non empty trivial V42(1) set
{{(AG,ZS,1),ZS},{(AG,ZS,1)}} is set
the addF of AG . [(AG,ZS,1),ZS] is set
(AG,ZS,1) + (AG,ZS,1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG . ((AG,ZS,1),(AG,ZS,1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[(AG,ZS,1),(AG,ZS,1)] is set
{(AG,ZS,1),(AG,ZS,1)} is set
{{(AG,ZS,1),(AG,ZS,1)},{(AG,ZS,1)}} is set
the addF of AG . [(AG,ZS,1),(AG,ZS,1)] is set
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() ext-real positive non negative V35() V40() V79() integer Element of NAT
(AG,ZS,(1 + 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . ((1 + 1),ZS) is set
[(1 + 1),ZS] is set
{(1 + 1),ZS} is set
{(1 + 1)} is non empty trivial V42(1) set
{{(1 + 1),ZS},{(1 + 1)}} is set
the of AG . [(1 + 1),ZS] is set
(AG,ZS,2) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the of AG . (2,ZS) is set
[2,ZS] is set
{2,ZS} is set
{2} is non empty trivial V42(1) set
{{2,ZS},{2}} is set
the of AG . [2,ZS] is set
AG is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of AG is non empty set
0. AG is V51(AG) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the ZeroF of AG is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
ZS + ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the addF of AG is Relation-like Function-like V18([: the carrier of AG, the carrier of AG:], the carrier of AG) Element of bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:]
[: the carrier of AG, the carrier of AG:] is Relation-like non empty set
[:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is Relation-like non empty set
bool [:[: the carrier of AG, the carrier of AG:], the carrier of AG:] is non empty set
the addF of AG . (ZS,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
[ZS,ZS] is set
{ZS,ZS} is set
{ZS} is non empty trivial V42(1) set
{{ZS,ZS},{ZS}} is set
the addF of AG . [ZS,ZS] is set
- ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
AG is V31() ext-real V79() integer set
- AG is V31() ext-real V79() integer set
ZS is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of ZS is non empty set
ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
- ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,(- ML),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS is Relation-like Function-like V18([:INT, the carrier of ZS:], the carrier of ZS) Element of bool [:[:INT, the carrier of ZS:], the carrier of ZS:]
[:INT, the carrier of ZS:] is Relation-like non empty V35() set
[:[:INT, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of ZS:], the carrier of ZS:] is non empty V35() set
the of ZS . (AG,(- ML)) is set
[AG,(- ML)] is set
{AG,(- ML)} is set
{AG} is non empty trivial V42(1) set
{{AG,(- ML)},{AG}} is set
the of ZS . [AG,(- ML)] is set
(ZS,ML,(- AG)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . ((- AG),ML) is set
[(- AG),ML] is set
{(- AG),ML} is set
{(- AG)} is non empty trivial V42(1) set
{{(- AG),ML},{(- AG)}} is set
the of ZS . [(- AG),ML] is set
(ZS,ML,(- 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . ((- 1),ML) is set
[(- 1),ML] is set
{(- 1),ML} is set
{(- 1)} is non empty trivial V42(1) set
{{(- 1),ML},{(- 1)}} is set
the of ZS . [(- 1),ML] is set
(ZS,(ZS,ML,(- 1)),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,(ZS,ML,(- 1))) is set
[AG,(ZS,ML,(- 1))] is set
{AG,(ZS,ML,(- 1))} is set
{{AG,(ZS,ML,(- 1))},{AG}} is set
the of ZS . [AG,(ZS,ML,(- 1))] is set
AG * (- 1) is V31() ext-real V79() integer set
(ZS,ML,(AG * (- 1))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . ((AG * (- 1)),ML) is set
[(AG * (- 1)),ML] is set
{(AG * (- 1)),ML} is set
{(AG * (- 1))} is non empty trivial V42(1) set
{{(AG * (- 1)),ML},{(AG * (- 1))}} is set
the of ZS . [(AG * (- 1)),ML] is set
AG is V31() ext-real V79() integer set
ZS is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of ZS is non empty set
ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
- ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,(- ML),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS is Relation-like Function-like V18([:INT, the carrier of ZS:], the carrier of ZS) Element of bool [:[:INT, the carrier of ZS:], the carrier of ZS:]
[:INT, the carrier of ZS:] is Relation-like non empty V35() set
[:[:INT, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of ZS:], the carrier of ZS:] is non empty V35() set
the of ZS . (AG,(- ML)) is set
[AG,(- ML)] is set
{AG,(- ML)} is set
{AG} is non empty trivial V42(1) set
{{AG,(- ML)},{AG}} is set
the of ZS . [AG,(- ML)] is set
(ZS,ML,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,ML) is set
[AG,ML] is set
{AG,ML} is set
{{AG,ML},{AG}} is set
the of ZS . [AG,ML] is set
- (ZS,ML,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
1 * AG is V31() ext-real V79() integer set
- (1 * AG) is V31() ext-real V79() integer set
(ZS,ML,(- (1 * AG))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . ((- (1 * AG)),ML) is set
[(- (1 * AG)),ML] is set
{(- (1 * AG)),ML} is set
{(- (1 * AG))} is non empty trivial V42(1) set
{{(- (1 * AG)),ML},{(- (1 * AG))}} is set
the of ZS . [(- (1 * AG)),ML] is set
(- 1) * AG is V31() ext-real V79() integer set
(ZS,ML,((- 1) * AG)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (((- 1) * AG),ML) is set
[((- 1) * AG),ML] is set
{((- 1) * AG),ML} is set
{((- 1) * AG)} is non empty trivial V42(1) set
{{((- 1) * AG),ML},{((- 1) * AG)}} is set
the of ZS . [((- 1) * AG),ML] is set
(ZS,(ZS,ML,AG),(- 1)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . ((- 1),(ZS,ML,AG)) is set
[(- 1),(ZS,ML,AG)] is set
{(- 1),(ZS,ML,AG)} is set
{(- 1)} is non empty trivial V42(1) set
{{(- 1),(ZS,ML,AG)},{(- 1)}} is set
the of ZS . [(- 1),(ZS,ML,AG)] is set
AG is V31() ext-real V79() integer set
- AG is V31() ext-real V79() integer set
ZS is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of ZS is non empty set
ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
- ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,(- ML),(- AG)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS is Relation-like Function-like V18([:INT, the carrier of ZS:], the carrier of ZS) Element of bool [:[:INT, the carrier of ZS:], the carrier of ZS:]
[:INT, the carrier of ZS:] is Relation-like non empty V35() set
[:[:INT, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of ZS:], the carrier of ZS:] is non empty V35() set
the of ZS . ((- AG),(- ML)) is set
[(- AG),(- ML)] is set
{(- AG),(- ML)} is set
{(- AG)} is non empty trivial V42(1) set
{{(- AG),(- ML)},{(- AG)}} is set
the of ZS . [(- AG),(- ML)] is set
(ZS,ML,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,ML) is set
[AG,ML] is set
{AG,ML} is set
{AG} is non empty trivial V42(1) set
{{AG,ML},{AG}} is set
the of ZS . [AG,ML] is set
- (- AG) is V31() ext-real V79() integer set
(ZS,ML,(- (- AG))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . ((- (- AG)),ML) is set
[(- (- AG)),ML] is set
{(- (- AG)),ML} is set
{(- (- AG))} is non empty trivial V42(1) set
{{(- (- AG)),ML},{(- (- AG))}} is set
the of ZS . [(- (- AG)),ML] is set
AG is V31() ext-real V79() integer set
ZS is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of ZS is non empty set
ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,ML,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS is Relation-like Function-like V18([:INT, the carrier of ZS:], the carrier of ZS) Element of bool [:[:INT, the carrier of ZS:], the carrier of ZS:]
[:INT, the carrier of ZS:] is Relation-like non empty V35() set
[:[:INT, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of ZS:], the carrier of ZS:] is non empty V35() set
the of ZS . (AG,ML) is set
[AG,ML] is set
{AG,ML} is set
{AG} is non empty trivial V42(1) set
{{AG,ML},{AG}} is set
the of ZS . [AG,ML] is set
AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
ML - AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
- AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
ML + (- AD) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS is Relation-like Function-like V18([: the carrier of ZS, the carrier of ZS:], the carrier of ZS) Element of bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:]
[: the carrier of ZS, the carrier of ZS:] is Relation-like non empty set
[:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty set
bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is non empty set
the addF of ZS . (ML,(- AD)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[ML,(- AD)] is set
{ML,(- AD)} is set
{ML} is non empty trivial V42(1) set
{{ML,(- AD)},{ML}} is set
the addF of ZS . [ML,(- AD)] is set
(ZS,(ML - AD),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,(ML - AD)) is set
[AG,(ML - AD)] is set
{AG,(ML - AD)} is set
{{AG,(ML - AD)},{AG}} is set
the of ZS . [AG,(ML - AD)] is set
(ZS,AD,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,AD) is set
[AG,AD] is set
{AG,AD} is set
{{AG,AD},{AG}} is set
the of ZS . [AG,AD] is set
(ZS,ML,AG) - (ZS,AD,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
- (ZS,AD,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,ML,AG) + (- (ZS,AD,AG)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS . ((ZS,ML,AG),(- (ZS,AD,AG))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(ZS,ML,AG),(- (ZS,AD,AG))] is set
{(ZS,ML,AG),(- (ZS,AD,AG))} is set
{(ZS,ML,AG)} is non empty trivial V42(1) set
{{(ZS,ML,AG),(- (ZS,AD,AG))},{(ZS,ML,AG)}} is set
the addF of ZS . [(ZS,ML,AG),(- (ZS,AD,AG))] is set
(ZS,(- AD),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,(- AD)) is set
[AG,(- AD)] is set
{AG,(- AD)} is set
{{AG,(- AD)},{AG}} is set
the of ZS . [AG,(- AD)] is set
(ZS,ML,AG) + (ZS,(- AD),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS . ((ZS,ML,AG),(ZS,(- AD),AG)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(ZS,ML,AG),(ZS,(- AD),AG)] is set
{(ZS,ML,AG),(ZS,(- AD),AG)} is set
{{(ZS,ML,AG),(ZS,(- AD),AG)},{(ZS,ML,AG)}} is set
the addF of ZS . [(ZS,ML,AG),(ZS,(- AD),AG)] is set
AG is V31() ext-real V79() integer set
ZS is V31() ext-real V79() integer set
AG - ZS is V31() ext-real V79() integer set
ML is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of ML is non empty set
AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
(ML,AD,(AG - ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the of ML is Relation-like Function-like V18([:INT, the carrier of ML:], the carrier of ML) Element of bool [:[:INT, the carrier of ML:], the carrier of ML:]
[:INT, the carrier of ML:] is Relation-like non empty V35() set
[:[:INT, the carrier of ML:], the carrier of ML:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of ML:], the carrier of ML:] is non empty V35() set
the of ML . ((AG - ZS),AD) is set
[(AG - ZS),AD] is set
{(AG - ZS),AD} is set
{(AG - ZS)} is non empty trivial V42(1) set
{{(AG - ZS),AD},{(AG - ZS)}} is set
the of ML . [(AG - ZS),AD] is set
(ML,AD,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the of ML . (AG,AD) is set
[AG,AD] is set
{AG,AD} is set
{AG} is non empty trivial V42(1) set
{{AG,AD},{AG}} is set
the of ML . [AG,AD] is set
(ML,AD,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the of ML . (ZS,AD) is set
[ZS,AD] is set
{ZS,AD} is set
{ZS} is non empty trivial V42(1) set
{{ZS,AD},{ZS}} is set
the of ML . [ZS,AD] is set
(ML,AD,AG) - (ML,AD,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
- (ML,AD,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
(ML,AD,AG) + (- (ML,AD,ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the addF of ML is Relation-like Function-like V18([: the carrier of ML, the carrier of ML:], the carrier of ML) Element of bool [:[: the carrier of ML, the carrier of ML:], the carrier of ML:]
[: the carrier of ML, the carrier of ML:] is Relation-like non empty set
[:[: the carrier of ML, the carrier of ML:], the carrier of ML:] is Relation-like non empty set
bool [:[: the carrier of ML, the carrier of ML:], the carrier of ML:] is non empty set
the addF of ML . ((ML,AD,AG),(- (ML,AD,ZS))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
[(ML,AD,AG),(- (ML,AD,ZS))] is set
{(ML,AD,AG),(- (ML,AD,ZS))} is set
{(ML,AD,AG)} is non empty trivial V42(1) set
{{(ML,AD,AG),(- (ML,AD,ZS))},{(ML,AD,AG)}} is set
the addF of ML . [(ML,AD,AG),(- (ML,AD,ZS))] is set
- ZS is V31() ext-real V79() integer set
AG + (- ZS) is V31() ext-real V79() integer set
(ML,AD,(AG + (- ZS))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the of ML . ((AG + (- ZS)),AD) is set
[(AG + (- ZS)),AD] is set
{(AG + (- ZS)),AD} is set
{(AG + (- ZS))} is non empty trivial V42(1) set
{{(AG + (- ZS)),AD},{(AG + (- ZS))}} is set
the of ML . [(AG + (- ZS)),AD] is set
(ML,AD,(- ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the of ML . ((- ZS),AD) is set
[(- ZS),AD] is set
{(- ZS),AD} is set
{(- ZS)} is non empty trivial V42(1) set
{{(- ZS),AD},{(- ZS)}} is set
the of ML . [(- ZS),AD] is set
(ML,AD,AG) + (ML,AD,(- ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the addF of ML . ((ML,AD,AG),(ML,AD,(- ZS))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
[(ML,AD,AG),(ML,AD,(- ZS))] is set
{(ML,AD,AG),(ML,AD,(- ZS))} is set
{{(ML,AD,AG),(ML,AD,(- ZS))},{(ML,AD,AG)}} is set
the addF of ML . [(ML,AD,AG),(ML,AD,(- ZS))] is set
- AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
(ML,(- AD),ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the of ML . (ZS,(- AD)) is set
[ZS,(- AD)] is set
{ZS,(- AD)} is set
{{ZS,(- AD)},{ZS}} is set
the of ML . [ZS,(- AD)] is set
(ML,AD,AG) + (ML,(- AD),ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the addF of ML . ((ML,AD,AG),(ML,(- AD),ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
[(ML,AD,AG),(ML,(- AD),ZS)] is set
{(ML,AD,AG),(ML,(- AD),ZS)} is set
{{(ML,AD,AG),(ML,(- AD),ZS)},{(ML,AD,AG)}} is set
the addF of ML . [(ML,AD,AG),(ML,(- AD),ZS)] is set
AG is V31() ext-real V79() integer set
ZS is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of ZS is non empty set
ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,ML,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS is Relation-like Function-like V18([:INT, the carrier of ZS:], the carrier of ZS) Element of bool [:[:INT, the carrier of ZS:], the carrier of ZS:]
[:INT, the carrier of ZS:] is Relation-like non empty V35() set
[:[:INT, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of ZS:], the carrier of ZS:] is non empty V35() set
the of ZS . (AG,ML) is set
[AG,ML] is set
{AG,ML} is set
{AG} is non empty trivial V42(1) set
{{AG,ML},{AG}} is set
the of ZS . [AG,ML] is set
AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,AD,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,AD) is set
[AG,AD] is set
{AG,AD} is set
{{AG,AD},{AG}} is set
the of ZS . [AG,AD] is set
0. ZS is V51(ZS) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the ZeroF of ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,ML,AG) - (ZS,AD,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
- (ZS,AD,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,ML,AG) + (- (ZS,AD,AG)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS is Relation-like Function-like V18([: the carrier of ZS, the carrier of ZS:], the carrier of ZS) Element of bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:]
[: the carrier of ZS, the carrier of ZS:] is Relation-like non empty set
[:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty set
bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is non empty set
the addF of ZS . ((ZS,ML,AG),(- (ZS,AD,AG))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(ZS,ML,AG),(- (ZS,AD,AG))] is set
{(ZS,ML,AG),(- (ZS,AD,AG))} is set
{(ZS,ML,AG)} is non empty trivial V42(1) set
{{(ZS,ML,AG),(- (ZS,AD,AG))},{(ZS,ML,AG)}} is set
the addF of ZS . [(ZS,ML,AG),(- (ZS,AD,AG))] is set
ML - AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
- AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
ML + (- AD) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS . (ML,(- AD)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[ML,(- AD)] is set
{ML,(- AD)} is set
{ML} is non empty trivial V42(1) set
{{ML,(- AD)},{ML}} is set
the addF of ZS . [ML,(- AD)] is set
(ZS,(ML - AD),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,(ML - AD)) is set
[AG,(ML - AD)] is set
{AG,(ML - AD)} is set
{{AG,(ML - AD)},{AG}} is set
the of ZS . [AG,(ML - AD)] is set
AG is V31() ext-real V79() integer set
ZS is V31() ext-real V79() integer set
ML is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of ML is non empty set
0. ML is V51(ML) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the ZeroF of ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
(ML,AD,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the of ML is Relation-like Function-like V18([:INT, the carrier of ML:], the carrier of ML) Element of bool [:[:INT, the carrier of ML:], the carrier of ML:]
[:INT, the carrier of ML:] is Relation-like non empty V35() set
[:[:INT, the carrier of ML:], the carrier of ML:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of ML:], the carrier of ML:] is non empty V35() set
the of ML . (AG,AD) is set
[AG,AD] is set
{AG,AD} is set
{AG} is non empty trivial V42(1) set
{{AG,AD},{AG}} is set
the of ML . [AG,AD] is set
(ML,AD,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the of ML . (ZS,AD) is set
[ZS,AD] is set
{ZS,AD} is set
{ZS} is non empty trivial V42(1) set
{{ZS,AD},{ZS}} is set
the of ML . [ZS,AD] is set
(ML,AD,AG) - (ML,AD,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
- (ML,AD,ZS) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
(ML,AD,AG) + (- (ML,AD,ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the addF of ML is Relation-like Function-like V18([: the carrier of ML, the carrier of ML:], the carrier of ML) Element of bool [:[: the carrier of ML, the carrier of ML:], the carrier of ML:]
[: the carrier of ML, the carrier of ML:] is Relation-like non empty set
[:[: the carrier of ML, the carrier of ML:], the carrier of ML:] is Relation-like non empty set
bool [:[: the carrier of ML, the carrier of ML:], the carrier of ML:] is non empty set
the addF of ML . ((ML,AD,AG),(- (ML,AD,ZS))) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
[(ML,AD,AG),(- (ML,AD,ZS))] is set
{(ML,AD,AG),(- (ML,AD,ZS))} is set
{(ML,AD,AG)} is non empty trivial V42(1) set
{{(ML,AD,AG),(- (ML,AD,ZS))},{(ML,AD,AG)}} is set
the addF of ML . [(ML,AD,AG),(- (ML,AD,ZS))] is set
AG - ZS is V31() ext-real V79() integer set
(ML,AD,(AG - ZS)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ML
the of ML . ((AG - ZS),AD) is set
[(AG - ZS),AD] is set
{(AG - ZS),AD} is set
{(AG - ZS)} is non empty trivial V42(1) set
{{(AG - ZS),AD},{(AG - ZS)}} is set
the of ML . [(AG - ZS),AD] is set
- ZS is V31() ext-real V79() integer set
(- ZS) + AG is V31() ext-real V79() integer set
AG is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of AG is non empty set
<*> the carrier of AG is Relation-like non-empty empty-yielding NAT -defined the carrier of AG -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() ext-real non positive non negative V35() V40() V42( {} ) V79() FinSequence-like FinSubsequence-like FinSequence-membered integer FinSequence of the carrier of AG
[:NAT, the carrier of AG:] is Relation-like non empty V35() set
Sum (<*> the carrier of AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
0. AG is V51(AG) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the ZeroF of AG is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
bool [:NAT, the carrier of AG:] is non empty V35() set
len (<*> the carrier of AG) is Relation-like non-empty empty-yielding functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() ext-real non positive non negative V35() V40() V42( {} ) V79() FinSequence-like FinSequence-membered integer Element of NAT
ML is Relation-like Function-like V18( NAT , the carrier of AG) Element of bool [:NAT, the carrier of AG:]
ML . (len (<*> the carrier of AG)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
ML . 0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
AG is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of AG is non empty set
0. AG is V51(AG) left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
the ZeroF of AG is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
ZS is Relation-like NAT -defined the carrier of AG -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of AG
len ZS is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
Sum ZS is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of AG
<*> the carrier of AG is Relation-like non-empty empty-yielding NAT -defined the carrier of AG -valued Function-like functional empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() ext-real non positive non negative V35() V40() V42( {} ) V79() FinSequence-like FinSubsequence-like FinSequence-membered integer FinSequence of the carrier of AG
[:NAT, the carrier of AG:] is Relation-like non empty V35() set
AG is V31() ext-real V79() integer set
ZS is non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed V129() V130() V131() V132() () () () () ()
the carrier of ZS is non empty set
ML is Relation-like NAT -defined the carrier of ZS -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of ZS
len ML is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
dom ML is Element of bool NAT
Sum ML is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
AD is Relation-like NAT -defined the carrier of ZS -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of ZS
len AD is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
Sum AD is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,(Sum AD),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS is Relation-like Function-like V18([:INT, the carrier of ZS:], the carrier of ZS) Element of bool [:[:INT, the carrier of ZS:], the carrier of ZS:]
[:INT, the carrier of ZS:] is Relation-like non empty V35() set
[:[:INT, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty V35() set
bool [:[:INT, the carrier of ZS:], the carrier of ZS:] is non empty V35() set
the of ZS . (AG,(Sum AD)) is set
[AG,(Sum AD)] is set
{AG,(Sum AD)} is set
{AG} is non empty trivial V42(1) set
{{AG,(Sum AD)},{AG}} is set
the of ZS . [AG,(Sum AD)] is set
Seg (len ML) is V35() V42( len ML) Element of bool NAT
CA is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
Z0 is Relation-like NAT -defined the carrier of ZS -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of ZS
len Z0 is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
MLI is Relation-like NAT -defined the carrier of ZS -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of ZS
len MLI is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
CA + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() ext-real positive non negative V35() V40() V79() integer Element of NAT
Seg (len Z0) is V35() V42( len Z0) Element of bool NAT
Seg CA is V35() V42(CA) Element of bool NAT
Z0 | (Seg CA) is Relation-like NAT -defined Seg CA -defined NAT -defined the carrier of ZS -valued Function-like FinSubsequence-like Element of bool [:NAT, the carrier of ZS:]
[:NAT, the carrier of ZS:] is Relation-like non empty V35() set
bool [:NAT, the carrier of ZS:] is non empty V35() set
MLI | (Seg CA) is Relation-like NAT -defined Seg CA -defined NAT -defined the carrier of ZS -valued Function-like FinSubsequence-like Element of bool [:NAT, the carrier of ZS:]
i is Relation-like NAT -defined the carrier of ZS -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of ZS
len i is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
v is Relation-like NAT -defined the carrier of ZS -valued Function-like V35() FinSequence-like FinSubsequence-like FinSequence of the carrier of ZS
len v is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
Seg (len v) is V35() V42( len v) Element of bool NAT
dom v is Element of bool NAT
v1 is epsilon-transitive epsilon-connected ordinal natural V31() ext-real non negative V35() V40() V79() integer Element of NAT
a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
i . v1 is set
dom i is Element of bool NAT
MLI . v1 is set
Z0 . v1 is set
(ZS,a1,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,a1) is set
[AG,a1] is set
{AG,a1} is set
{{AG,a1},{AG}} is set
the of ZS . [AG,a1] is set
v . v1 is set
dom Z0 is Element of bool NAT
dom MLI is Element of bool NAT
Z0 . (CA + 1) is set
MLI . (CA + 1) is set
v1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,a1,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,a1) is set
[AG,a1] is set
{AG,a1} is set
{{AG,a1},{AG}} is set
the of ZS . [AG,a1] is set
Seg (len i) is V35() V42( len i) Element of bool NAT
Sum Z0 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
Sum v is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(Sum v) + v1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS is Relation-like Function-like V18([: the carrier of ZS, the carrier of ZS:], the carrier of ZS) Element of bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:]
[: the carrier of ZS, the carrier of ZS:] is Relation-like non empty set
[:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is Relation-like non empty set
bool [:[: the carrier of ZS, the carrier of ZS:], the carrier of ZS:] is non empty set
the addF of ZS . ((Sum v),v1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(Sum v),v1] is set
{(Sum v),v1} is set
{(Sum v)} is non empty trivial V42(1) set
{{(Sum v),v1},{(Sum v)}} is set
the addF of ZS . [(Sum v),v1] is set
Sum i is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
(ZS,(Sum i),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,(Sum i)) is set
[AG,(Sum i)] is set
{AG,(Sum i)} is set
{{AG,(Sum i)},{AG}} is set
the of ZS . [AG,(Sum i)] is set
(ZS,(Sum i),AG) + (ZS,a1,AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS . ((ZS,(Sum i),AG),(ZS,a1,AG)) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(ZS,(Sum i),AG),(ZS,a1,AG)] is set
{(ZS,(Sum i),AG),(ZS,a1,AG)} is set
{(ZS,(Sum i),AG)} is non empty trivial V42(1) set
{{(ZS,(Sum i),AG),(ZS,a1,AG)},{(ZS,(Sum i),AG)}} is set
the addF of ZS . [(ZS,(Sum i),AG),(ZS,a1,AG)] is set
(Sum i) + a1 is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the addF of ZS . ((Sum i),a1) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
[(Sum i),a1] is set
{(Sum i),a1} is set
{(Sum i)} is non empty trivial V42(1) set
{{(Sum i),a1},{(Sum i)}} is set
the addF of ZS . [(Sum i),a1] is set
(ZS,((Sum i) + a1),AG) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of ZS
the of ZS . (AG,((Sum i) + a1)) is set
[AG,((Sum i) + a1)] is set
{AG,((Sum i) + a1)} is set
{{AG,((Sum i) + a1)},{AG}} is set
the of ZS . [AG,((Sum i) + a1)] is set
Sum MLI is left_add-cancelable