:: HILBASIS semantic presentation

REAL is V72() V73() V74() V78() V292() V293() V295() set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal V72() V73() V74() V75() V76() V77() V78() V290() V292() Element of bool REAL
bool REAL is non empty set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal V72() V73() V74() V75() V76() V77() V78() V290() V292() set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
COMPLEX is V72() V78() set
RAT is V72() V73() V74() V75() V78() set
INT is V72() V73() V74() V75() V76() V78() set

bool is non empty set

1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
{{},1} is non empty finite V34() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
K377() is set
bool K377() is non empty set
K378() is Element of bool K377()
2 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool is non empty non trivial non finite set
is Relation-like V62() V63() V64() set
bool is non empty set
K239(1,NAT) is M10( NAT )

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool is non empty non trivial non finite set
K859() is set

3 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
Seg 1 is non empty trivial finite 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT
{1} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
Seg 2 is non empty finite 2 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT
{1,2} is non empty finite V34() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set

Bags {} is functional non empty Element of bool ()
Bags {} is non empty set
bool () is non empty set
is functional non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set

rng R is finite set

rng X is finite set
(rng R) \/ (rng X) is finite set

dom f0 is set

rng (R ^ X) is finite set
dom (X * f0) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom X is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT

len cR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT

dom ((R ^ X) * f0) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom (R ^ X) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom (R * f0) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom R is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
len S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set

len tcR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom tcR is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
dom S is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
(S ^ cR) . tcPR is set
S . tcPR is set
R . tcPR is set
f0 . (R . tcPR) is set
(R ^ X) . tcPR is set
f0 . ((R ^ X) . tcPR) is set
tcR . tcPR is set
dom S is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT

(len R) + 0X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR . tcPR is set
(R ^ X) . tcPR is set
f0 . ((R ^ X) . tcPR) is set
X . 0X is set
f0 . (X . 0X) is set
cR . 0X is set
(S ^ cR) . tcPR is set
dom S is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool NAT
len (R ^ X) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(len S) + (len cR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len (S ^ cR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT

Bags 0 is functional non empty Element of bool ()
Bags 0 is non empty set
bool () is non empty set
K239(2,()) is M10( Bags 0)

bool is non empty set
is functional non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set

len () is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
dom () is non empty finite V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT
dom () is non empty finite V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT

len () is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set

tcR is set
{ b1 where b1 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT : not R <= b1 } is set
cR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
{ b1 where b1 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT : not X <= b1 } is set
X is set
R is set

dom cR is Element of bool R
bool R is non empty set
dom S is Element of bool R
tcPR is set
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
S . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcPR is set
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
S . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcPR is set
X is set
R is set

(f0 -' tcR) | R is Relation-like R -defined X -defined RAT -valued Function-like V62() V63() V64() V65() set

(f0 + tcR) | R is Relation-like R -defined X -defined RAT -valued Function-like V62() V63() V64() V65() set

dom f0 is Element of bool X
bool X is non empty set
dom (f0 | R) is Element of bool R
bool R is non empty set
X /\ R is set
dom tcR is Element of bool X
dom (tcR | R) is Element of bool R
dom (f0 + tcR) is Element of bool X
dom ((f0 + tcR) | R) is Element of bool R
tcPR is set
((f0 + tcR) | R) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(f0 + tcR) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(f0 . tcPR) + (tcR . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR . tcPR) + (tcR . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
S . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR . tcPR) + (S . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR + S) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom (f0 -' tcR) is Element of bool X
dom ((f0 -' tcR) | R) is Element of bool R
tcPR is set
((f0 -' tcR) | R) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(f0 -' tcR) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(f0 . tcPR) -' (tcR . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR . tcPR) -' (tcR . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
S . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR . tcPR) -' (S . tcPR) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(cR -' S) . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom (cR -' S) is Element of bool R
dom (cR + S) is Element of bool R

R + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
Bags (R + 1) is non empty set
Bags (R + 1) is functional non empty Element of bool (Bags (R + 1))
bool (Bags (R + 1)) is non empty set

{R} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set

{X} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set

bool [:{R},{X}:] is non empty finite V34() set
f0 +* (R .--> X) is Relation-like RAT -valued Function-like V62() V63() V64() V65() set
dom f0 is finite Element of bool R
bool R is non empty finite V34() set
dom (f0 +* (R .--> X)) is set
dom (R .--> X) is trivial finite V34() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool {R}
bool {R} is non empty finite V34() set
(dom f0) \/ (dom (R .--> X)) is finite set
(dom f0) \/ {R} is non empty finite set
R \/ {R} is non empty finite set
succ R is set
cR is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)

cR . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom (cR | R) is finite Element of bool R
(R + 1) /\ R is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() set
(succ R) /\ R is finite set
(R \/ {R}) /\ R is finite set
S is set
(cR | R) . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R .--> X) . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)

tcR . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)

cR . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom tcR is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool (R + 1)
bool (R + 1) is non empty finite V34() set
S is set
succ R is set
{R} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
R \/ {R} is non empty finite set
tcR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R + 1) /\ R is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() set
dom f0 is finite Element of bool R
bool R is non empty finite V34() set
tcR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom cR is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool (R + 1)
R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
EmptyBag (R + 1) is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)
Bags (R + 1) is non empty set
Bags (R + 1) is functional non empty Element of bool (Bags (R + 1))
bool (Bags (R + 1)) is non empty set

Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
(R,0,()) is Relation-like R + 1 -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags (R + 1)
R + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
Bags (R + 1) is non empty set
Bags (R + 1) is functional non empty Element of bool (Bags (R + 1))
bool (Bags (R + 1)) is non empty set
X is set
succ R is set
{R} is non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of bool NAT
R \/ {R} is non empty finite V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
(EmptyBag (R + 1)) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
() . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT

((R,0,()) | R) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R,0,()) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(EmptyBag (R + 1)) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R,0,()) . R is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(R,0,()) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
dom (EmptyBag (R + 1)) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool (R + 1)
bool (R + 1) is non empty finite V34() set
dom (R,0,()) is finite V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of bool (R + 1)
bool (R + 1) is non empty finite V34() set
R is ordinal set
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set

rng () is functional non empty finite Element of bool (Bags R)
bool (Bags R) is non empty set

[:(Bags R),(Bags R):] is Relation-like non empty set
bool [:(Bags R),(Bags R):] is non empty set
tcR is functional non empty finite Element of bool (Bags R)

field () is set
R is set

Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
X is Element of R

R is non empty set
X is Element of R

Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set

support (R,X) is finite Element of bool R
bool R is non empty set
{X} is non empty trivial finite 1 -element Element of bool R
f0 is set
(() +* (X,1)) . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
() . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT

[:R,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool [:R,NAT:] is non empty non trivial non finite set
is functional non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
[:R,:] is Relation-like RAT -valued INT -valued non empty V62() V63() V64() V65() set
dom () is Element of bool R
(R,X) . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R is non empty set
X is Element of R

Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set

(R,X) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT

[:R,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool [:R,NAT:] is non empty non trivial non finite set
is functional non empty trivial finite V34() 1 -element V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() set
[:R,:] is Relation-like RAT -valued INT -valued non empty V62() V63() V64() V65() set
dom (R --> 0) is non empty Element of bool R
bool R is non empty set
(R --> 0) +* (X,1) is Relation-like R -defined NAT -valued RAT -valued Function-like non empty total quasi_total V62() V63() V64() V65() Element of bool [:R,NAT:]
((R --> 0) +* (X,1)) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
f0 is Element of R
(R,X) . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
() . f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R is non empty set
X is Element of R

Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set

f0 is Element of R

() +* (f0,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(R,f0) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
R is non empty ordinal set
X is Element of R

Bags R is non empty set
Bags R is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set

the carrier of f0 is non empty non trivial set
[:R, the carrier of f0:] is Relation-like non empty set
bool [:R, the carrier of f0:] is non empty set
tcR is Relation-like R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:R, the carrier of f0:]
eval ((R,X),tcR) is Element of the carrier of f0
tcR . X is Element of the carrier of f0
support (R,X) is finite Element of bool R
bool R is non empty set
{X} is non empty trivial finite 1 -element Element of bool R
power f0 is Relation-like [: the carrier of f0,NAT:] -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of f0,NAT:], the carrier of f0:]
[: the carrier of f0,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
[:[: the carrier of f0,NAT:], the carrier of f0:] is Relation-like non empty non trivial non finite set
bool [:[: the carrier of f0,NAT:], the carrier of f0:] is non empty non trivial non finite set
(R,X) . X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
(power f0) . ((tcR . X),((R,X) . X)) is Element of the carrier of f0
0 + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
(power f0) . ((tcR . X),(0 + 1)) is Element of the carrier of f0
cR is Element of the carrier of f0
(power f0) . (cR,0) is Element of the carrier of f0
((power f0) . (cR,0)) * cR is Element of the carrier of f0
1_ f0 is Element of the carrier of f0
K409(f0) is Element of the carrier of f0
the OneF of f0 is Element of the carrier of f0
(1_ f0) * cR is Element of the carrier of f0
R is set
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set
f0 is non empty unital multLoopStr_0
the carrier of f0 is non empty set
0_ (R,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
[:(Bags R), the carrier of f0:] is Relation-like non empty set
bool [:(Bags R), the carrier of f0:] is non empty set
X is Element of R

1_ f0 is Element of the carrier of f0
(0_ (R,f0)) +* ((R,X),(1_ f0)) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
R is set
X is non empty non trivial unital doubleLoopStr
1_ X is Element of the carrier of X
the carrier of X is non empty non trivial set
0. X is V102(X) Element of the carrier of X
the ZeroF of X is Element of the carrier of X
f0 is Element of R
(R,f0,X) is Relation-like Bags R -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of X:]
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set
[:(Bags R), the carrier of X:] is Relation-like non empty set
bool [:(Bags R), the carrier of X:] is non empty set
0_ (R,X) is Relation-like Bags R -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of X:]

() +* (f0,1) is Relation-like R -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(0_ (R,X)) +* ((R,f0),(1_ X)) is Relation-like Bags R -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of X:]
(R,f0,X) . (R,f0) is Element of the carrier of X
dom (0_ (R,X)) is functional non empty Element of bool (Bags R)
bool (Bags R) is non empty set
(Bags R) --> (0. X) is Relation-like Bags R -defined the carrier of X -valued Function-like constant non empty total quasi_total Element of bool [:(Bags R), the carrier of X:]
{(0. X)} is non empty trivial finite 1 -element set
[:(Bags R),{(0. X)}:] is Relation-like non empty set
dom ((Bags R) --> (0. X)) is functional non empty Element of bool (Bags R)

(R,f0,X) . tcR is Element of the carrier of X
(0_ (R,X)) . tcR is Element of the carrier of X
R is set
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set
X is Element of R

{(R,X)} is functional non empty trivial finite 1 -element Element of bool (Bags R)
bool (Bags R) is non empty set

(R,X,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
the carrier of f0 is non empty non trivial set
[:(Bags R), the carrier of f0:] is Relation-like non empty set
bool [:(Bags R), the carrier of f0:] is non empty set
0_ (R,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]

(0_ (R,f0)) +* ((R,X),(1_ f0)) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
Support (R,X,f0) is functional Element of bool (Bags R)
tcR is set

(R,X,f0) . tcR is set
R is ordinal set
Bags R is functional non empty Element of bool (Bags R)
Bags R is non empty set
bool (Bags R) is non empty set

X is Element of R
(R,X,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
the carrier of f0 is non empty non trivial set
[:(Bags R), the carrier of f0:] is Relation-like non empty set
bool [:(Bags R), the carrier of f0:] is non empty set
0_ (R,f0) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total finite-Support Element of bool [:(Bags R), the carrier of f0:]

(0_ (R,f0)) +* ((R,X),(1_ f0)) is Relation-like Bags R -defined the carrier of f0 -valued Function-like non empty total quasi_total Element of bool [:(Bags R), the carrier of f0:]
Support (R,X,f0) is functional Element of bool (Bags R)
bool (Bags R) is non empty set
{(R,X)} is functional non empty trivial finite 1 -element Element of bool (Bags R)

the carrier of R is non empty non trivial set
X is non empty set
Bags X is functional non empty Element of bool (Bags X)
Bags X is non empty set
bool (Bags X) is non empty set
f0 is Element of X
(X,f0,R) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]
[:(Bags X), the carrier of R:] is Relation-like non empty set
bool [:(Bags X), the carrier of R:] is non empty set
0_ (X,R) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]

() +* (f0,1) is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set

(0_ (X,R)) +* ((X,f0),(1_ R)) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]
tcR is Element of X
(X,tcR,R) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]
(X,tcR) is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support Element of Bags X
() +* (tcR,1) is Relation-like X -defined RAT -valued Function-like total V62() V63() V64() V65() finite-support set
(0_ (X,R)) +* ((X,tcR),(1_ R)) is Relation-like Bags X -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:(Bags X), the carrier of R:]

the carrier of () is non empty set
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set

f0 is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
- f0 is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
cR is set
f0 - f0 is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
f0 + (- f0) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
(f0 - f0) . cR is set
S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT

(f0 . S) - (f0 . S) is left_add-cancelable right_add-cancelable add-cancelable right_complementable Element of the carrier of R

{(0. R)} is non empty trivial finite 1 -element set
[:NAT,{(0. R)}:] is Relation-like non empty non trivial non finite set
(0_. R) . cR is set

dom (0_. R) is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT
dom (f0 - f0) is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT

tcR + (- tcR) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]

the carrier of () is non empty set
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set

tcR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
cR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
tcR - cR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
- cR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]
tcR + (- cR) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]

the carrier of () is non empty set
bool the carrier of () is non empty set
X is non empty Element of bool the carrier of ()
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
{ b1 where b1 is Element of X : for b2, b3 being Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:] holds
( not b2 = b1 or not b3 in X or len b2 <= len b3 )
}
is set

bool X is non empty set
cR is Element of X

len S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcPR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
len tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
[:X,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V62() V63() V64() V65() set
bool [:X,NAT:] is non empty non trivial non finite set

f0 is non empty Element of bool X
cR .: f0 is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT
min (cR .: f0) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() set
cR .: X is V72() V73() V74() V75() V76() V77() V292() Element of bool NAT
dom cR is non empty Element of bool X
S is set
cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT

tcPR is Element of X

cR . S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR . tcPR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len 0X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len S is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
0X is set
S is Element of X

the carrier of () is non empty set
bool the carrier of () is non empty set
the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
X is non empty Element of bool the carrier of ()
(R,X) is non empty Element of bool X
bool X is non empty set
{ b1 where b1 is Element of X : for b2, b3 being Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:] holds
( not b2 = b1 or not b3 in X or len b2 <= len b3 )
}
is set

len f0 is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
len tcR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
cR is Element of X

the carrier of R is non empty set
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set

{(0. R)} is non empty trivial finite 1 -element set
[:NAT,{(0. R)}:] is Relation-like non empty non trivial non finite set
(0_. R) +* (X,f0) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]

X + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT
tcR is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of R:]

dom (0_. R) is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT

S is set
tcR . S is set
cR . S is set
tcR . S is set
cR . S is set
dom tcR is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT
dom cR is non empty V72() V73() V74() V75() V76() V77() V290() V292() Element of bool NAT

the carrier of R is non empty set

X is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
X + 1 is non empty ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V290() V291() V292() V293() V294() Element of NAT

(R,X,f0) is Relation-like NAT -defined the carrier of R -valued Function-like non empty total quasi_total finite-Support Element of bool [:NAT, the carrier of R:]
[:NAT, the carrier of R:] is Relation-like non empty non trivial non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite set
len (R,X,f0) is ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V292() V293() V294() Element of NAT
tcR is ordinal natural finite cardinal V42() V43() V44() ext-real non negative set