:: PARTIT1 semantic presentation

REAL is V36() V37() V38() V42() set
NAT is V36() V37() V38() V39() V40() V41() V42() Element of bool REAL
bool REAL is non empty set
NAT is V36() V37() V38() V39() V40() V41() V42() set
bool NAT is non empty set
bool NAT is non empty set
{} is empty V36() V37() V38() V39() V40() V41() V42() set
1 is non empty ext-real positive V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
union {} is set
2 is non empty ext-real positive V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
0 is empty ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() V42() Element of NAT
Seg 1 is V36() V37() V38() V39() V40() V41() Element of bool NAT
3 is non empty ext-real positive V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is set
a is set
the Element of z is Element of z
{{}} is non empty set
Y is set
Y \ {{}} is Element of bool Y
bool Y is non empty set
union (Y \ {{}}) is set
union Y is set
PA is set
z is set
PA is set
z is set
Y is non empty set
z is non empty with_non-empty_elements a_partition of Y
PA is non empty with_non-empty_elements a_partition of Y
a is set
x is set
b is set
Y is non empty set
z is non empty with_non-empty_elements a_partition of Y
PA is non empty with_non-empty_elements a_partition of Y
Y is non empty set
z is non empty with_non-empty_elements a_partition of Y
PA is non empty with_non-empty_elements a_partition of Y
a is set
the Element of a is Element of a
union z is Element of bool Y
bool Y is non empty set
b is set
x1 is set
Y is non empty set
Y is non empty set
Y is non empty set
z is non empty with_non-empty_elements a_partition of Y
PA is non empty with_non-empty_elements a_partition of Y
union z is Element of bool Y
bool Y is non empty set
a is set
{ b₁ where b₁ is Element of bool Y : ( b₁ in z & b₁ c= a ) } is set
b is set
x1 is set
C is Element of bool Y
union { b₁ where b₁ is Element of bool Y : ( b₁ in z & b₁ c= a ) } is set
x1 is set
C is set
Ca is set
x1 is set
C is set
Ca is Element of bool Y
a is set
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
{Y} is non empty set
bool Y is non empty set
bool (bool Y) is non empty set
union {Y} is set
z is Element of bool Y
a is Element of bool Y
z is set
the Element of z is Element of z
x is set
Y is non empty set
bool Y is non empty set
bool (bool Y) is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is Element of bool (bool Y)
Intersect z is Element of bool Y
x is set
x is Relation-like Function-like set
dom x is set
rng x is set
bool Y is non empty Element of bool (bool Y)
bool (bool Y) is non empty Element of bool (bool (bool Y))
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
b is set
x1 is set
x . x1 is set
a is non empty Element of bool (bool Y)
[:a,(bool (bool Y)):] is non empty set
bool [:a,(bool (bool Y)):] is non empty set
b is Relation-like a -defined bool (bool Y) -valued Function-like V21(a, bool (bool Y)) Element of bool [:a,(bool (bool Y)):]
{ H₁(b₁) where b₁ is Element of a : S₂[b₁] } is set
x1 is Element of bool (bool (bool Y))
C is Element of bool (bool (bool Y))
Intersect C is Element of bool (bool Y)
Ca is Element of bool (bool Y)
union Ca is set
pb is set
Cb is set
b . Cb is set
pb is set
b . pb is set
Cb is set
x9 is Element of Y
EqClass (x9,PA) is Element of bool Y
meet z is Element of bool Y
y5 is set
z5 is Element of a
b . z5 is Element of bool (bool Y)
union (b . z5) is Element of bool Y
y1 is set
meet C is Element of bool (bool Y)
union Ca is Element of bool Y
pb is set
meet z is Element of bool Y
Cb is Element of Y
x9 is non empty with_non-empty_elements a_partition of Y
EqClass (Cb,x9) is Element of bool Y
y5 is set
b . y5 is set
z5 is set
y1 is Element of a
b . y1 is Element of bool (bool Y)
union (b . y1) is Element of bool Y
q is set
meet C is Element of bool (bool Y)
pb is set
Cb is set
b . Cb is set
x9 is set
meet C is Element of bool (bool Y)
fx is set
b . fx is set
union (b . fx) is set
meet z is Element of bool Y
Y is non empty set
bool Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is Element of bool Y
a is Element of bool Y
z /\ a is Element of bool Y
x is set
union x is set
b is set
union b is set
x /\ b is set
union (x /\ b) is set
x1 is set
C is set
Ca is set
x1 is set
C is set
x \/ b is set
x1 is set
Y is non empty set
bool Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is Element of bool Y
z ` is Element of bool Y
a is set
union a is set
PA \ a is Element of bool (bool Y)
bool (bool Y) is non empty set
union (PA \ a) is set
union PA is Element of bool Y
(union PA) \ (union a) is Element of bool Y
bool PA is non empty set
x is Element of bool PA
PA \ x is Element of bool (bool Y)
Y is non empty set
bool Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
a is Element of Y
union PA is Element of bool Y
x is set
b is set
bool (bool Y) is non empty set
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool Y : S<sub>1</sub>[b<sub>1</sub>] } is set
x is Element of bool (bool Y)
b is Element of bool (bool Y)
x1 is set
C is Element of bool Y
meet b is Element of bool Y
Intersect b is Element of bool Y
x1 is set
C is Element of bool Y
x1 is set
C is Element of bool Y
x1 is set
C is set
union C is set
Ca is set
Ca is Element of bool Y
Ca ` is Element of bool Y
Y \ Ca is Element of bool Y
Ca /\ (Ca `) is Element of bool Y
pb is set
Ca /\ (Intersect b) is Element of bool Y
Ca /\ Ca is Element of bool Y
pb is set
Y is non empty set
bool Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is Element of Y
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
a is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
Class a is non empty with_non-empty_elements a_partition of Y
Class (a,z) is Element of bool Y
{z} is non empty set
a .: {z} is set
Y is set
bool Y is non empty Element of bool (bool Y)
bool Y is non empty set
bool (bool Y) is non empty set
bool (bool Y) is non empty Element of bool (bool (bool Y))
bool (bool Y) is non empty set
bool (bool (bool Y)) is non empty set
PA is set
z is set
PA is set
z is set
a is set
Y is set
(Y) is set
PA is non empty set
{PA} is non empty set
bool PA is non empty set
bool (bool PA) is non empty set
union {PA} is set
z is Element of bool PA
a is Element of bool PA
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,z) is set
(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))
bool (INTERSECTION (PA,z)) is non empty set
bool Y is non empty set
bool (bool Y) is non empty set
bool Y is non empty Element of bool (bool Y)
b is set
x1 is set
C is set
x1 /\ C is set
b is Element of bool (bool Y)
a is Element of bool (bool Y)
b \ a is Element of bool (bool Y)
union PA is Element of bool Y
union z is Element of bool Y
x1 is Element of bool (bool Y)
union x1 is Element of bool Y
union (INTERSECTION (PA,z)) is set
(union PA) /\ (union z) is Element of bool Y
C is Element of bool Y
Ca is set
pb is set
Ca /\ pb is set
Cb is set
x9 is set
Cb /\ x9 is set
(Ca /\ pb) /\ (Cb /\ x9) is set
pb /\ Cb is set
(pb /\ Cb) /\ x9 is set
Ca /\ ((pb /\ Cb) /\ x9) is set
pb /\ (Cb /\ x9) is set
Ca /\ (pb /\ (Cb /\ x9)) is set
Ca is Element of bool Y
pb is set
Cb is set
pb /\ Cb is set
x9 is set
fx is set
x9 /\ fx is set
pb /\ x9 is set
Cb /\ fx is set
(pb /\ x9) /\ (Cb /\ fx) is set
x9 /\ Cb is set
(x9 /\ Cb) /\ fx is set
pb /\ ((x9 /\ Cb) /\ fx) is set
(pb /\ Cb) /\ (x9 /\ fx) is set
Ca is Element of bool Y
a is non empty with_non-empty_elements a_partition of Y
x is non empty with_non-empty_elements a_partition of Y
b is non empty with_non-empty_elements a_partition of Y
INTERSECTION (x,b) is set
(INTERSECTION (x,b)) \ {{}} is Element of bool (INTERSECTION (x,b))
bool (INTERSECTION (x,b)) is non empty set
INTERSECTION (b,x) is set
(INTERSECTION (b,x)) \ {{}} is Element of bool (INTERSECTION (b,x))
bool (INTERSECTION (b,x)) is non empty set
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
(Y,PA,PA) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,PA) is set
(INTERSECTION (PA,PA)) \ {{}} is Element of bool (INTERSECTION (PA,PA))
bool (INTERSECTION (PA,PA)) is non empty set
z is set
a is set
x is set
a /\ x is set
z is set
z /\ z is set
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,z) is set
(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))
bool (INTERSECTION (PA,z)) is non empty set
a is non empty with_non-empty_elements a_partition of Y
(Y,(Y,PA,z),a) is non empty with_non-empty_elements a_partition of Y
INTERSECTION ((Y,PA,z),a) is set
(INTERSECTION ((Y,PA,z),a)) \ {{}} is Element of bool (INTERSECTION ((Y,PA,z),a))
bool (INTERSECTION ((Y,PA,z),a)) is non empty set
(Y,z,a) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (z,a) is set
(INTERSECTION (z,a)) \ {{}} is Element of bool (INTERSECTION (z,a))
bool (INTERSECTION (z,a)) is non empty set
(Y,PA,(Y,z,a)) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,(Y,z,a)) is set
(INTERSECTION (PA,(Y,z,a))) \ {{}} is Element of bool (INTERSECTION (PA,(Y,z,a)))
bool (INTERSECTION (PA,(Y,z,a))) is non empty set
x is non empty with_non-empty_elements a_partition of Y
b is non empty with_non-empty_elements a_partition of Y
(Y,x,a) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (x,a) is set
(INTERSECTION (x,a)) \ {{}} is Element of bool (INTERSECTION (x,a))
bool (INTERSECTION (x,a)) is non empty set
(Y,PA,b) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,b) is set
(INTERSECTION (PA,b)) \ {{}} is Element of bool (INTERSECTION (PA,b))
bool (INTERSECTION (PA,b)) is non empty set
x1 is set
C is set
Ca is set
C /\ Ca is set
pb is set
Cb is set
pb /\ Cb is set
Cb /\ Ca is set
(pb /\ Cb) /\ Ca is set
fx is set
y5 is set
x9 is set
y5 /\ fx is set
pb /\ fx is set
x1 is set
C is set
Ca is set
C /\ Ca is set
pb is set
Cb is set
pb /\ Cb is set
C /\ pb is set
(C /\ pb) /\ Cb is set
fx is set
y5 is set
x9 is set
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,z) is set
(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))
bool (INTERSECTION (PA,z)) is non empty set
a is set
x is set
b is set
x /\ b is set
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
union PA is Element of bool Y
bool Y is non empty set
a is set
x is set
bool Y is non empty Element of bool (bool Y)
bool (bool Y) is non empty set
a is set
x is set
b is set
x1 is set
union x1 is set
union a is set
x is set
b is Element of bool Y
x is set
b is set
x1 is set
union x1 is set
x is Element of bool Y
b is set
union b is set
x1 is set
C is Element of bool Y
x /\ C is Element of bool Y
Ca is set
Ca is set
x is set
b is set
union b is set
x is Element of bool (bool Y)
b is set
x1 is set
a is non empty with_non-empty_elements a_partition of Y
x is non empty with_non-empty_elements a_partition of Y
b is set
a is non empty with_non-empty_elements a_partition of Y
x is non empty with_non-empty_elements a_partition of Y
b is non empty with_non-empty_elements a_partition of Y
x1 is set
C is set
x1 is set
C is set
x1 is set
C is set
x1 is set
C is set
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
a is set
the Element of a is Element of a
union (Y,PA,z) is Element of bool Y
bool Y is non empty set
b is set
x1 is set
union x1 is set
C is set
a /\ C is set
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
(Y,PA,PA) is non empty with_non-empty_elements a_partition of Y
z is set
a is set
union a is set
the Element of z is Element of z
union PA is Element of bool Y
bool Y is non empty set
b is set
x1 is set
b /\ x1 is set
Y is non empty set
PA is set
z is set
a is set
x is non empty with_non-empty_elements a_partition of Y
b is non empty with_non-empty_elements a_partition of Y
x1 is set
Y is non empty set
PA is set
x is non empty with_non-empty_elements a_partition of Y
b is non empty with_non-empty_elements a_partition of Y
(Y,x,b) is non empty with_non-empty_elements a_partition of Y
z is set
a is set
Y is non empty set
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
bool Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
union PA is Element of bool Y
z is set
a is set
a is non empty set
x is Element of bool Y
x is Element of bool Y
z is set
a is set
z is set
a is set
x is set
b is Element of bool Y
x1 is Element of bool Y
z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
a is set
x is set
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
C is Element of bool Y
b is set
x1 is set
[b,x1] is set
{b,x1} is non empty set
{b} is non empty set
{{b,x1},{b}} is non empty set
z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
a is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
x is set
b is set
[x,b] is set
{x,b} is non empty set
{x} is non empty set
{{x,b},{x}} is non empty set
x1 is Element of bool Y
x1 is Element of bool Y
Y is non empty set
(Y) is non empty set
PA is set
z is non empty with_non-empty_elements a_partition of Y
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
PA is Relation-like Function-like set
dom PA is set
z is Relation-like Function-like set
dom z is set
a is set
PA . a is set
z . a is set
x is non empty with_non-empty_elements a_partition of Y
(Y,x) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
b is non empty with_non-empty_elements a_partition of Y
(Y,b) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
b is set
x1 is set
[b,x1] is set
{b,x1} is non empty set
{b} is non empty set
{{b,x1},{b}} is non empty set
bool Y is non empty set
C is Element of bool Y
Ca is set
b is set
the Element of b is Element of b
{ b₁ where b₁ is Element of Y : [ the Element of b,b₁] in (Y,z) } is set
Ca is set
[ the Element of b,Ca] is set
{ the Element of b,Ca} is non empty set
{ the Element of b} is non empty set
{{ the Element of b,Ca},{ the Element of b}} is non empty set
[ the Element of b, the Element of b] is set
{ the Element of b, the Element of b} is non empty set
{ the Element of b} is non empty set
{{ the Element of b, the Element of b},{ the Element of b}} is non empty set
bool Y is non empty set
pb is Element of bool Y
Cb is set
x9 is Element of Y
[ the Element of b,x9] is set
{ the Element of b,x9} is non empty set
{{ the Element of b,x9},{ the Element of b}} is non empty set
x9 is Element of bool Y
Cb is set
[ the Element of b,Cb] is set
{ the Element of b,Cb} is non empty set
{{ the Element of b,Cb},{ the Element of b}} is non empty set
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
a is set
x is set
b is set
x1 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
x1 . 1 is set
len x1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
x1 . (len x1) is set
C is set
union C is set
Ca is set
union Ca is set
union PA is Element of bool Y
bool Y is non empty set
pb is set
Cb is set
pb is set
Cb is set
x1 . 0 is set
pb is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
x1 . pb is set
pb + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
x1 . (pb + 1) is set
Cb is set
x9 is set
fx is set
y5 is set
z5 is set
y1 is set
q is set
Y is non empty set
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
PA is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
PA \/ z is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]
PA "\/" z is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
a is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
a . 1 is set
len a is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
a . (len a) is set
x is set
b is set
[x,b] is set
{x,b} is non empty set
{x} is non empty set
{{x,b},{x}} is non empty set
a . 0 is set
[(a . 1),(a . 0)] is set
{(a . 1),(a . 0)} is non empty set
{(a . 1)} is non empty set
{{(a . 1),(a . 0)},{(a . 1)}} is non empty set
x1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
a . x1 is set
[(a . 1),(a . x1)] is set
{(a . 1),(a . x1)} is non empty set
{{(a . 1),(a . x1)},{(a . 1)}} is non empty set
x1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
a . (x1 + 1) is set
[(a . 1),(a . (x1 + 1))] is set
{(a . 1),(a . (x1 + 1))} is non empty set
{{(a . 1),(a . (x1 + 1))},{(a . 1)}} is non empty set
C is set
[(a . x1),C] is set
{(a . x1),C} is non empty set
{(a . x1)} is non empty set
{{(a . x1),C},{(a . x1)}} is non empty set
[C,(a . (x1 + 1))] is set
{C,(a . (x1 + 1))} is non empty set
{C} is non empty set
{{C,(a . (x1 + 1))},{C}} is non empty set
dom a is V36() V37() V38() V39() V40() V41() Element of bool NAT
Seg (len a) is V36() V37() V38() V39() V40() V41() Element of bool NAT
pb is Element of Y
Ca is Element of Y
Cb is Element of Y
<*pb,Ca,Cb*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
x9 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len x9 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
x9 . 1 is set
x9 . 3 is set
fx is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
x9 . fx is set
fx + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
x9 . (fx + 1) is set
[(x9 . fx),(x9 . (fx + 1))] is set
{(x9 . fx),(x9 . (fx + 1))} is non empty set
{(x9 . fx)} is non empty set
{{(x9 . fx),(x9 . (fx + 1))},{(x9 . fx)}} is non empty set
2 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
[(a . x1),(a . (x1 + 1))] is set
{(a . x1),(a . (x1 + 1))} is non empty set
{{(a . x1),(a . (x1 + 1))},{(a . x1)}} is non empty set
[(a . 1),(a . 1)] is set
{(a . 1),(a . 1)} is non empty set
{{(a . 1),(a . 1)},{(a . 1)}} is non empty set
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) "\/" (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
union PA is Element of bool Y
bool Y is non empty set
union z is Element of bool Y
a is set
x is set
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
b is Element of bool Y
x1 is set
union x1 is set
C is set
{ b₁ where b₁ is Element of PA : ex b₂ being Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y st
( 1 <= len b₂ & b₂ . 1 = a & b₂ . (len b₂) in b₁ & ( for b₃ being ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT holds
( not 1 <= b₃ or len b₂ <= b₃ or ex b₄, b₅, b₆ being set st
( b₄ in PA & b₅ in z & b₂ . b₃ in b₄ & b₆ in b₄ /\ b₅ & b₂ . (b₃ + 1) in b₅ ) ) ) ) } is set
Ca is set
union Ca is set
{ b₁ where b₁ is Element of z : ex b₂ being set st
( b₂ in Ca & not b₁ /\ b₂ = {} ) } is set
x9 is Element of Y
<*x9*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
fx is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
fx . 1 is set
len fx is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
fx . (len fx) is set
y5 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
fx . y5 is set
y5 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
fx . (y5 + 1) is set
y5 is set
z5 is set
y5 /\ z5 is set
Cb is set
y1 is set
q is Element of PA
fd is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len fd is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
fd . 1 is set
fd . (len fd) is set
pb is set
union Cb is set
y1 is set
q is set
fd is Element of PA
y9 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len y9 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
y9 . 1 is set
y9 . (len y9) is set
fd is set
q /\ fd is set
y1 is set
q is set
fd is Element of z
y9 is set
fd /\ y9 is Element of bool Y
fd is set
q /\ fd is set
y9 is Element of z
f is set
y9 /\ f is Element of bool Y
y9 is set
f is Element of PA
z0 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len z0 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
z0 . 1 is set
z0 . (len z0) is set
f is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len f is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . 1 is set
f . (len f) is set
i is Element of z
p1 is set
i /\ p1 is Element of bool Y
z0 is Element of Y
<*z0*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
f ^ <*z0*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
i is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
len <*z0*> is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
(len f) + (len <*z0*>) is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
(len f) + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
i . ((len f) + 1) is set
p1 is set
dom f is V36() V37() V38() V39() V40() V41() Element of bool NAT
Seg (len f) is V36() V37() V38() V39() V40() V41() Element of bool NAT
p2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
i . p2 is set
f . p2 is set
(f ^ <*z0*>) . ((len f) + 1) is set
i . 1 is set
i . (len f) is set
p2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
i . p2 is set
p2 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
i . (p2 + 1) is set
f . p2 is set
f . (p2 + 1) is set
p2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
i . p2 is set
p2 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
i . (p2 + 1) is set
u is Element of z
x2 is set
u /\ x2 is Element of bool Y
y2 is Element of PA
c₂₈ is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len c₂₈ is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
c₂₈ . 1 is set
c₂₈ . (len c₂₈) is set
u is set
x2 is set
y2 is set
u /\ x2 is set
c₂₈ is set
c₂₉ is set
c₃₀ is set
c₂₈ /\ c₂₉ is set
y1 is set
q is Element of z
fd is set
q /\ fd is Element of bool Y
pb \ b is Element of bool pb
bool pb is non empty set
y1 is set
q is set
fd is Element of z
y9 is set
fd /\ y9 is Element of bool Y
fd is set
q /\ fd is set
y9 is Element of PA
f is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len f is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . 1 is set
f . (len f) is set
y9 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len y9 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
y9 . 1 is set
y9 . (len y9) is set
z0 is Element of z
i is set
z0 /\ i is Element of bool Y
f is Element of Y
<*f*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
y9 ^ <*f*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
z0 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len z0 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
len <*f*> is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
(len y9) + (len <*f*>) is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
(len y9) + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
z0 . ((len y9) + 1) is set
i is set
dom y9 is V36() V37() V38() V39() V40() V41() Element of bool NAT
Seg (len y9) is V36() V37() V38() V39() V40() V41() Element of bool NAT
p1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
z0 . p1 is set
y9 . p1 is set
(y9 ^ <*f*>) . ((len y9) + 1) is set
z0 . 1 is set
z0 . (len y9) is set
p1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
z0 . p1 is set
p1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
z0 . (p1 + 1) is set
y9 . p1 is set
y9 . (p1 + 1) is set
p1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
z0 . p1 is set
p1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
z0 . (p1 + 1) is set
p2 is Element of z
u is set
p2 /\ u is Element of bool Y
x2 is Element of PA
y2 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len y2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
y2 . 1 is set
y2 . (len y2) is set
p2 is set
u is set
x2 is set
p2 /\ u is set
y2 is set
c₂₈ is set
c₂₉ is set
y2 /\ c₂₈ is set
p1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
z0 . p1 is set
p1 + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
z0 . (p1 + 1) is set
p2 is set
u is set
x2 is set
p2 /\ u is set
y1 is set
q is Element of z
fd is set
q /\ fd is Element of bool Y
q is set
y1 /\ q is set
fd is Element of PA
y9 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len y9 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
y9 . 1 is set
y9 . (len y9) is set
fd is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len fd is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
fd . 1 is set
fd . (len fd) is set
y9 is Element of Y
<*y9*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
fd ^ <*y9*> is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
f is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len f is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
len <*y9*> is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
(len fd) + (len <*y9*>) is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
(len fd) + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . ((len fd) + 1) is set
z0 is set
dom fd is V36() V37() V38() V39() V40() V41() Element of bool NAT
Seg (len fd) is V36() V37() V38() V39() V40() V41() Element of bool NAT
i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . i is set
fd . i is set
f . (len fd) is set
i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . i is set
i + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . (i + 1) is set
fd . i is set
fd . (i + 1) is set
i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . i is set
i + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . (i + 1) is set
p1 is Element of z
p2 is set
p1 /\ p2 is Element of bool Y
u is Element of PA
x2 is Relation-like NAT -defined Y -valued Function-like FinSequence-like FinSequence of Y
len x2 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
x2 . 1 is set
x2 . (len x2) is set
p1 is set
p2 is set
u is set
p1 /\ p2 is set
x2 is set
y2 is set
c₂₈ is set
x2 /\ y2 is set
(fd ^ <*y9*>) . ((len fd) + 1) is set
f . 1 is set
(Y,PA) \/ (Y,z) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]
i is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . i is set
i + 1 is ext-real V27() V34() V35() V36() V37() V38() V39() V40() V41() Element of NAT
f . (i + 1) is set
p1 is set
p2 is set
u is set
p1 /\ p2 is set
x2 is set
[x2,u] is set
{x2,u} is non empty set
{x2} is non empty set
{{x2,u},{x2}} is non empty set
y2 is set
[u,y2] is set
{u,y2} is non empty set
{u} is non empty set
{{u,y2},{u}} is non empty set
[x9,y9] is set
{x9,y9} is non empty set
{x9} is non empty set
{{x9,y9},{x9}} is non empty set
(Y,PA) \/ (Y,z) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]
a is set
x is set
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
b is Element of bool Y
b is Element of bool Y
x1 is set
b is Element of bool Y
b is Element of bool Y
x1 is set
b is Element of bool Y
x1 is Element of bool Y
b is Element of bool Y
x1 is Element of bool Y
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,z) is set
(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))
bool (INTERSECTION (PA,z)) is non empty set
(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) /\ (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
a is set
x is set
[a,x] is set
{a,x} is non empty set
{a} is non empty set
{{a,x},{a}} is non empty set
bool Y is non empty set
b is Element of bool Y
x1 is set
x1 is set
b is Element of bool Y
x1 is Element of bool Y
b /\ x1 is Element of bool Y
C is Element of bool Y
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
z is non empty with_non-empty_elements a_partition of Y
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
a is non empty with_non-empty_elements a_partition of Y
(Y,(Y,PA,z),a) is non empty with_non-empty_elements a_partition of Y
(Y,z,a) is non empty with_non-empty_elements a_partition of Y
(Y,PA,(Y,z,a)) is non empty with_non-empty_elements a_partition of Y
(Y,(Y,(Y,PA,z),a)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y,PA,z)) "\/" (Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) "\/" (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
((Y,PA) "\/" (Y,z)) "\/" (Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,z) "\/" (Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) "\/" ((Y,z) "\/" (Y,a)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y,z,a)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) "\/" (Y,(Y,z,a)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y,PA,(Y,z,a))) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
(Y,PA,(Y,PA,z)) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,(Y,PA,z)) is set
(INTERSECTION (PA,(Y,PA,z))) \ {{}} is Element of bool (INTERSECTION (PA,(Y,PA,z)))
bool (INTERSECTION (PA,(Y,PA,z))) is non empty set
(Y,(Y,PA,(Y,PA,z))) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) /\ (Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) "\/" (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) /\ ((Y,PA) "\/" (Y,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,z) is set
(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))
bool (INTERSECTION (PA,z)) is non empty set
(Y,PA,(Y,PA,z)) is non empty with_non-empty_elements a_partition of Y
(Y,(Y,PA,(Y,PA,z))) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) "\/" (Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) /\ (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) "\/" ((Y,PA) /\ (Y,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
Y is non empty set
PA is non empty with_non-empty_elements a_partition of Y
a is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
(Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) "\/" (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) \/ (Y,z) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]
Y is non empty set
a is non empty with_non-empty_elements a_partition of Y
PA is non empty with_non-empty_elements a_partition of Y
z is non empty with_non-empty_elements a_partition of Y
(Y,PA,z) is non empty with_non-empty_elements a_partition of Y
INTERSECTION (PA,z) is set
(INTERSECTION (PA,z)) \ {{}} is Element of bool (INTERSECTION (PA,z))
bool (INTERSECTION (PA,z)) is non empty set
(Y,a) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y,PA,z)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) /\ (Y,z) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
Y is non empty set
{Y} is non empty set
bool Y is non empty set
bool (bool Y) is non empty set
union {Y} is set
PA is Element of bool Y
z is Element of bool Y
Y is non empty set
SmallestPartition Y is non empty with_non-empty_elements a_partition of Y
K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
Class K51(Y) is non empty with_non-empty_elements a_partition of Y
bool Y is non empty set
{ b₁ where b₁ is Element of bool Y : ex b₂ being set st
( b₁ = {b₂} & b₂ in Y ) } is set
z is set
{ {b₁} where b₁ is Element of Y : verum } is set
a is Element of Y
{a} is non empty set
x is Element of Y
{x} is non empty set
b is Element of bool Y
z is set
{ {b₁} where b₁ is Element of Y : verum } is set
a is Element of bool Y
x is set
{x} is non empty set
Y is non empty set
(Y) is non empty with_non-empty_elements a_partition of Y
{Y} is non empty set
SmallestPartition Y is non empty with_non-empty_elements a_partition of Y
K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
Class K51(Y) is non empty with_non-empty_elements a_partition of Y
PA is non empty with_non-empty_elements a_partition of Y
z is set
the Element of z is Element of z
union (Y) is Element of bool Y
bool Y is non empty set
x is set
z is set
{ {b₁} where b₁ is Element of Y : verum } is set
a is Element of Y
{a} is non empty set
the Element of z is Element of z
union PA is Element of bool Y
bool Y is non empty set
b is set
x1 is set
Y is non empty set
(Y) is non empty with_non-empty_elements a_partition of Y
{Y} is non empty set
(Y,(Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
nabla Y is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
PA is set
z is set
[PA,z] is set
{PA,z} is non empty set
{PA} is non empty set
{{PA,z},{PA}} is non empty set
Y is non empty set
SmallestPartition Y is non empty with_non-empty_elements a_partition of Y
K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
Class K51(Y) is non empty with_non-empty_elements a_partition of Y
(Y,(SmallestPartition Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
id Y is non empty Relation-like V43() V45() V46() V50() set
union (SmallestPartition Y) is Element of bool Y
bool Y is non empty set
PA is set
z is set
[PA,z] is set
{PA,z} is non empty set
{PA} is non empty set
{{PA,z},{PA}} is non empty set
a is Element of bool Y
{ {b₁} where b₁ is Element of Y : verum } is set
x is Element of Y
{x} is non empty set
PA is set
z is set
[PA,z] is set
{PA,z} is non empty set
{PA} is non empty set
{{PA,z},{PA}} is non empty set
a is set
Y is non empty set
SmallestPartition Y is non empty with_non-empty_elements a_partition of Y
K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
Class K51(Y) is non empty with_non-empty_elements a_partition of Y
(Y) is non empty with_non-empty_elements a_partition of Y
{Y} is non empty set
(Y,(Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
nabla Y is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(SmallestPartition Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
Y is non empty set
(Y) is non empty with_non-empty_elements a_partition of Y
{Y} is non empty set
PA is non empty with_non-empty_elements a_partition of Y
(Y,(Y),PA) is non empty with_non-empty_elements a_partition of Y
(Y,(Y),PA) is non empty with_non-empty_elements a_partition of Y
INTERSECTION ((Y),PA) is set
(INTERSECTION ((Y),PA)) \ {{}} is Element of bool (INTERSECTION ((Y),PA))
bool (INTERSECTION ((Y),PA)) is non empty set
(Y,(Y,(Y),PA)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
(Y,(Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y)) "\/" (Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
nabla Y is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y)) \/ (Y,PA) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]
(Y,PA,(Y)) is non empty with_non-empty_elements a_partition of Y
(Y,(Y,(Y),PA)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(Y)) /\ (Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
Y is non empty set
SmallestPartition Y is non empty with_non-empty_elements a_partition of Y
K51(Y) is non empty Relation-like Y -defined Y -valued V17(Y) V43() V45() V46() V50() Element of bool [:Y,Y:]
[:Y,Y:] is non empty set
bool [:Y,Y:] is non empty set
Class K51(Y) is non empty with_non-empty_elements a_partition of Y
PA is non empty with_non-empty_elements a_partition of Y
(Y,(SmallestPartition Y),PA) is non empty with_non-empty_elements a_partition of Y
(Y,(SmallestPartition Y),PA) is non empty with_non-empty_elements a_partition of Y
INTERSECTION ((SmallestPartition Y),PA) is set
(INTERSECTION ((SmallestPartition Y),PA)) \ {{}} is Element of bool (INTERSECTION ((SmallestPartition Y),PA))
bool (INTERSECTION ((SmallestPartition Y),PA)) is non empty set
(Y,(SmallestPartition Y)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
id Y is non empty Relation-like V43() V45() V46() V50() set
(Y,(Y,(SmallestPartition Y),PA)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(SmallestPartition Y)) "\/" (Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(SmallestPartition Y)) \/ (Y,PA) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]
(id Y) \/ (Y,PA) is non empty set
z is set
(Y,(Y,(SmallestPartition Y),PA)) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(Y,(SmallestPartition Y)) /\ (Y,PA) is Relation-like Y -defined Y -valued V17(Y) V43() V45() V50() Element of bool [:Y,Y:]
(id Y) /\ (Y,PA) is Relation-like Y -defined Y -valued Element of bool [:Y,Y:]