:: ZMODUL01 semantic presentation

REAL is non empty V35() set

bool REAL is non empty V35() set
{} is set

{{},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

bool omega is non empty V35() set
bool NAT is non empty V35() set
COMPLEX is non empty V35() set

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} is non empty trivial V42(1) 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:]

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 () ()

the carrier of AG is non empty trivial V35() V42(1) set

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
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)} is non empty trivial V42(1) set
{{(ZS + ML),AD},{(ZS + ML)}} is set
the of AG . [(ZS + ML),AD] is set
the of AG . (ZS,AD) is set
{ZS} is non empty trivial V42(1) set
the of AG . [ZS,AD] is set
the of AG . (ML,AD) is set
{ML} is non empty trivial V42(1) set
the of AG . [ML,AD] is set
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
{(AG,AD,ZS)} is non empty trivial V42(1) set

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
{ML} is non empty trivial V42(1) set
ZS is V31() ext-real V79() integer 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
the of AG . (ZS,(ML + AD)) is set
{ZS} is non empty trivial V42(1) set
the of AG . [ZS,(ML + AD)] is set
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
the of AG . (ZS,AD) is set
the of AG . [ZS,AD] is set
{(AG,ML,ZS)} is non empty trivial V42(1) set

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
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)} is non empty trivial V42(1) set
{{(ZS * ML),AD},{(ZS * ML)}} is set
the of AG . [(ZS * ML),AD] is set
the of AG . (ML,AD) is set
{ML} is non empty trivial V42(1) set
the of AG . [ML,AD] is set
the of AG . (ZS,(AG,AD,ML)) is set
{ZS} is non empty trivial V42(1) set
the of AG . [ZS,(AG,AD,ML)] is 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
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
the carrier of ZS is non empty set

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
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
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
[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
the of ZS . (AD,ML) is set
{AD} is non empty trivial V42(1) set
the of ZS . [AD,ML] is set
{(ZS,ML,AD)} is non empty trivial V42(1) set
AD + CA is V31() ext-real V79() integer set
the of ZS . ((AD + CA),ML) is set
{(AD + CA)} is non empty trivial V42(1) set
the of ZS . [(AD + CA),ML] is set

[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
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
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
[(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 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
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 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
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
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
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
[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
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 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
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

(- 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 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
[((- 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 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
the carrier of AG is non empty set

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
[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
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 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 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

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
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
the carrier of AG is non empty set

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
[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 is V31() ext-real V79() integer set
- AG is V31() ext-real V79() integer set
the carrier of ZS is non empty set

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
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
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
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
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
the carrier of ZS is non empty set

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
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
1 * AG is V31() ext-real V79() integer set
- (1 * AG) is V31() ext-real V79() integer set
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
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
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
the carrier of ZS is non empty set

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
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
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
the carrier of ZS is non empty set

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

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
{ML} is non empty trivial V42(1) set
the of ZS . (AG,(ML - AD)) is set
the of ZS . [AG,(ML - AD)] is set
the of ZS . (AG,AD) is set
the of ZS . [AG,AD] is set
{(ZS,ML,AG)} is non empty trivial V42(1) set
the of ZS . (AG,(- AD)) is set
the of ZS . [AG,(- AD)] 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
the carrier of ML is non empty set

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)} is non empty trivial V42(1) set
{{(AG - ZS),AD},{(AG - ZS)}} is set
the of ML . [(AG - ZS),AD] is set
the of ML . (AG,AD) is set
{AG} is non empty trivial V42(1) set
the of ML . [AG,AD] is set
the of ML . (ZS,AD) is set
{ZS} is non empty trivial V42(1) set
the of ML . [ZS,AD] is set
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
{(ML,AD,AG)} is non empty trivial V42(1) set
- ZS is V31() ext-real V79() integer set
AG + (- ZS) is V31() ext-real V79() integer 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
the of ML . ((- ZS),AD) is set
{(- ZS)} is non empty trivial V42(1) set
the of ML . [(- ZS),AD] is set

the of ML . (ZS,(- AD)) is set
the of ML . [ZS,(- AD)] is set
AG is V31() ext-real V79() integer set
the carrier of ZS is non empty set

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

the of ZS . (AG,AD) is set
the of ZS . [AG,AD] is set

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
{(ZS,ML,AG)} is non empty trivial V42(1) set

{ML} is non empty trivial V42(1) set
the of ZS . (AG,(ML - AD)) 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
the carrier of ML is non empty set

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} is non empty trivial V42(1) set
the of ML . [AG,AD] is set
the of ML . (ZS,AD) is set
{ZS} is non empty trivial V42(1) set
the of ML . [ZS,AD] is set
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
{(ML,AD,AG)} is non empty trivial V42(1) set
AG - ZS is V31() ext-real V79() integer set
the of ML . ((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
the carrier of AG is non empty set

[: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

bool [:NAT, the carrier of AG:] is non empty V35() set

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

the carrier of AG is non empty set

[:NAT, the carrier of AG:] is Relation-like non empty V35() set
AG is V31() ext-real V79() integer set
the carrier of ZS is non empty set

dom ML is Element of bool NAT

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} is non empty trivial V42(1) set
the of ZS . [AG,(Sum AD)] is set
Seg (len ML) is V35() V42( len ML) Element of bool 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:]

Seg (len v) is V35() V42( len v) Element of bool NAT
dom v is Element of bool NAT

i . v1 is set
dom i is Element of bool NAT
MLI . v1 is set
Z0 . v1 is set
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

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

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
[(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

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 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