:: SETWISEO semantic presentation

{} is Relation-like non-empty empty-yielding empty finite finite-yielding V30() set
union {} is finite set
X is set
{X} is non empty finite set
Y is set
Z is set
{X,Y,Z} is non empty finite set
{Y,Z} is non empty finite set
{X} \/ {Y,Z} is non empty finite set
X is set
Y is set
{X,Y} is non empty finite set
Z is set
{X,Y,Z} is non empty finite set
{Z} is non empty finite set
{X,Y} \/ {Z} is non empty finite set
X is set
Y is set
Z is Relation-like Function-like set
Z " X is set
Y \ (Z " X) is Element of K27(Y)
K27(Y) is non empty cup-closed diff-closed preBoolean set
Z .: (Y \ (Z " X)) is set
Z .: Y is set
(Z .: Y) \ X is Element of K27((Z .: Y))
K27((Z .: Y)) is non empty cup-closed diff-closed preBoolean set
f is set
dom Z is set
g is set
Z . g is set
dom Z is set
g is set
Z . g is set
X is non empty set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
f is Element of Y
Z . f is Element of X
{(Z . f)} is non empty finite set
Z " {(Z . f)} is Element of K27(Y)
K27(Y) is non empty cup-closed diff-closed preBoolean set
X is non empty set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
f is Element of Y
Im (Z,f) is set
{f} is non empty finite set
Z .: {f} is finite set
Z . f is Element of X
{(Z . f)} is non empty finite set
Z .: {f} is finite Element of K27(X)
K27(X) is non empty cup-closed diff-closed preBoolean set
g is set
dom Z is non empty Element of K27(Y)
K27(Y) is non empty cup-closed diff-closed preBoolean set
B is set
Z . B is set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
Z is set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin X
f is set
g is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
g .: Z is finite Element of K27(Y)
K27(Y) is non empty cup-closed diff-closed preBoolean set
B is set
dom g is non empty Element of K27(X)
K27(X) is non empty cup-closed diff-closed preBoolean set
y is set
g . y is set
i is Element of X
g . i is Element of Y
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
Z is set
X is non empty set
Y is non empty set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
Fin X is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
f is finite Element of Fin X
Z .: f is finite Element of K27(Y)
K27(Y) is non empty cup-closed diff-closed preBoolean set
Fin Y is non empty cup-closed diff-closed preBoolean set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
the Element of Y is Element of Y
f is Element of X
X is non empty set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Fin Y is non empty cup-closed diff-closed preBoolean set
Z is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
f is finite Element of Fin Y
Z .: f is finite Element of K27(X)
K27(X) is non empty cup-closed diff-closed preBoolean set
g is Element of Y
Z . g is Element of X
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
F₁() is non empty set
Fin F₁() is non empty cup-closed diff-closed preBoolean set
K28(F₁(),(Fin F₁())) is Relation-like non empty set
K27(K28(F₁(),(Fin F₁()))) is non empty cup-closed diff-closed preBoolean set
F₂() is finite Element of Fin F₁()
K27(F₁()) is non empty cup-closed diff-closed preBoolean set
Y is Element of F₁()
Z is Element of K27(F₁())
X is Element of K27(F₁())
f is Element of F₁()
f is finite Element of Fin F₁()
g is finite Element of Fin F₁()
B is Element of F₁()
y is Element of F₁()
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
the_unity_wrt Y is Element of X
Z is Element of X
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
the_unity_wrt Y is Element of X
Z is Element of X
Y . ((the_unity_wrt Y),Z) is Element of X
[(the_unity_wrt Y),Z] is set
{(the_unity_wrt Y),Z} is non empty finite set
{(the_unity_wrt Y)} is non empty finite set
{{(the_unity_wrt Y),Z},{(the_unity_wrt Y)}} is non empty finite V30() set
Y . [(the_unity_wrt Y),Z] is set
Y . (Z,(the_unity_wrt Y)) is Element of X
[Z,(the_unity_wrt Y)] is set
{Z,(the_unity_wrt Y)} is non empty finite set
{Z} is non empty finite set
{{Z,(the_unity_wrt Y)},{Z}} is non empty finite V30() set
Y . [Z,(the_unity_wrt Y)] is set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
the Element of X is Element of X
{ the Element of X} is non empty finite set
K27(X) is non empty cup-closed diff-closed preBoolean set
X is non empty set
X is non empty set
Y is Element of X
{Y} is non empty finite set
Fin X is non empty cup-closed diff-closed preBoolean set
K27(X) is non empty cup-closed diff-closed preBoolean set
Z is Element of X
{Y,Z} is non empty finite set
K27(X) is non empty cup-closed diff-closed preBoolean set
f is Element of X
{Y,Z,f} is non empty finite set
K27(X) is non empty cup-closed diff-closed preBoolean set
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
Z is finite Element of Fin X
Y \/ Z is finite set
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
Z is finite Element of Fin X
Y \ Z is finite set
F₁() is non empty set
(F₁()) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin F₁()
Fin F₁() is non empty cup-closed diff-closed preBoolean set
X is finite Element of Fin F₁()
Y is set
Z is set
{Y} is non empty finite set
Z \/ {Y} is non empty set
g is finite Element of Fin F₁()
f is Element of F₁()
(F₁(),f) is non empty finite Element of Fin F₁()
(F₁(),g,(F₁(),f)) is non empty finite Element of Fin F₁()
{f} is non empty finite set
g \/ {f} is non empty finite set
B is finite Element of Fin F₁()
Y is finite Element of Fin F₁()
F₁() is non empty set
Fin F₁() is non empty cup-closed diff-closed preBoolean set
X is non empty finite Element of Fin F₁()
Y is set
Z is set
{Y} is non empty finite set
Z \/ {Y} is non empty set
g is finite Element of Fin F₁()
f is Element of F₁()
(F₁(),f) is non empty finite Element of Fin F₁()
(F₁(),g,(F₁(),f)) is non empty finite Element of Fin F₁()
B is finite Element of Fin F₁()
Y is finite Element of Fin F₁()
F₁() is non empty set
(F₁()) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin F₁()
Fin F₁() is non empty cup-closed diff-closed preBoolean set
X is finite Element of Fin F₁()
Y is Element of F₁()
{Y} is non empty finite set
X \/ {Y} is non empty finite set
Y is non empty set
K28(Y,Y) is Relation-like non empty set
K28(K28(Y,Y),Y) is Relation-like non empty set
K27(K28(K28(Y,Y),Y)) is non empty cup-closed diff-closed preBoolean set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
f is finite Element of Fin X
Z is Relation-like K28(Y,Y) -defined Y -valued Function-like non empty V14(K28(Y,Y)) V18(K28(Y,Y),Y) Element of K27(K28(K28(Y,Y),Y))
K28((Fin X),Y) is Relation-like non empty set
K27(K28((Fin X),Y)) is non empty cup-closed diff-closed preBoolean set
g is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
B is finite Element of Fin X
y is Element of X
{y} is non empty finite set
B \/ {y} is non empty finite set
i is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
i . {} is set
(X,y) is non empty finite Element of Fin X
g . y is Element of Y
i9 is finite Element of Fin X
i . i9 is set
B2 is finite Element of Fin X
B2 \/ {y} is non empty finite set
i . B2 is Element of Y
Z . ((i . B2),(g . y)) is Element of Y
[(i . B2),(g . y)] is set
{(i . B2),(g . y)} is non empty finite set
{(i . B2)} is non empty finite set
{{(i . B2),(g . y)},{(i . B2)}} is non empty finite V30() set
Z . [(i . B2),(g . y)] is set
x9 is Element of Y
i9 \ {y} is finite Element of K27(i9)
K27(i9) is non empty finite V30() cup-closed diff-closed preBoolean set
B2 \ {y} is finite Element of K27(B2)
K27(B2) is non empty finite V30() cup-closed diff-closed preBoolean set
x9 is finite Element of Fin X
x9 \/ {y} is non empty finite set
i . x9 is Element of Y
Z . ((i . x9),(g . y)) is Element of Y
[(i . x9),(g . y)] is set
{(i . x9),(g . y)} is non empty finite set
{(i . x9)} is non empty finite set
{{(i . x9),(g . y)},{(i . x9)}} is non empty finite V30() set
Z . [(i . x9),(g . y)] is set
x9 \ {y} is finite Element of K27(x9)
K27(x9) is non empty finite V30() cup-closed diff-closed preBoolean set
i . i9 is Element of Y
B2 is Element of Y
x9 is finite Element of Fin X
x9 \/ {y} is non empty finite set
i . x9 is Element of Y
Z . ((i . x9),(g . y)) is Element of Y
[(i . x9),(g . y)] is set
{(i . x9),(g . y)} is non empty finite set
{(i . x9)} is non empty finite set
{{(i . x9),(g . y)},{(i . x9)}} is non empty finite V30() set
Z . [(i . x9),(g . y)] is set
B2 is finite Element of Fin X
B2 \/ {y} is non empty finite set
x9 is Element of Y
x9 is finite Element of Fin X
x9 \/ {y} is non empty finite set
c₁₄ is Element of Y
c₁₅ is finite Element of Fin X
(X,c₁₅,(X,y)) is non empty finite Element of Fin X
i9 is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
B2 is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
B2 . {} is set
x9 is finite Element of Fin X
x9 \/ {y} is non empty finite set
B2 . {y} is set
i . (X,y) is Element of Y
x9 is finite Element of Fin X
x9 is finite Element of Fin X
x9 \/ {y} is non empty finite set
B2 . x9 is Element of Y
i . x9 is Element of Y
x9 is Element of Y
x9 is Element of X
{x9} is non empty finite set
B2 . {x9} is set
g . x9 is Element of Y
x9 is finite Element of Fin X
x9 \/ {y} is non empty finite set
(X,x9) is non empty finite Element of Fin X
i . (X,x9) is Element of Y
x9 is finite Element of Fin X
(B \/ {y}) \ x9 is finite Element of K27((B \/ {y}))
K27((B \/ {y})) is non empty finite V30() cup-closed diff-closed preBoolean set
B2 . x9 is Element of Y
x9 is Element of X
{x9} is non empty finite set
x9 \/ {x9} is non empty finite set
B2 . (x9 \/ {x9}) is set
g . x9 is Element of Y
Z . ((B2 . x9),(g . x9)) is Element of Y
[(B2 . x9),(g . x9)] is set
{(B2 . x9),(g . x9)} is non empty finite set
{(B2 . x9)} is non empty finite set
{{(B2 . x9),(g . x9)},{(B2 . x9)}} is non empty finite V30() set
Z . [(B2 . x9),(g . x9)] is set
(X,x9) is non empty finite Element of Fin X
(X,x9,(X,x9)) is non empty finite Element of Fin X
B2 . (X,x9,(X,x9)) is Element of Y
i . (X,x9) is Element of Y
Z . ((i . (X,x9)),(g . y)) is Element of Y
[(i . (X,x9)),(g . y)] is set
{(i . (X,x9)),(g . y)} is non empty finite set
{(i . (X,x9))} is non empty finite set
{{(i . (X,x9)),(g . y)},{(i . (X,x9))}} is non empty finite V30() set
Z . [(i . (X,x9)),(g . y)] is set
Z . ((g . x9),(g . y)) is Element of Y
[(g . x9),(g . y)] is set
{(g . x9),(g . y)} is non empty finite set
{(g . x9)} is non empty finite set
{{(g . x9),(g . y)},{(g . x9)}} is non empty finite V30() set
Z . [(g . x9),(g . y)] is set
Z . ((g . y),(g . x9)) is Element of Y
[(g . y),(g . x9)] is set
{(g . y),(g . x9)} is non empty finite set
{(g . y)} is non empty finite set
{{(g . y),(g . x9)},{(g . y)}} is non empty finite V30() set
Z . [(g . y),(g . x9)] is set
x9 \ {y} is finite Element of K27(x9)
K27(x9) is non empty finite V30() cup-closed diff-closed preBoolean set
(X,x9,(X,y)) is finite Element of Fin X
(X,x9) is non empty finite Element of Fin X
(X,(X,x9,(X,y)),(X,x9)) is non empty finite Element of Fin X
B \ (x9 \ {y}) is finite Element of K27(B)
K27(B) is non empty finite V30() cup-closed diff-closed preBoolean set
(X,x9,(X,x9)) is non empty finite Element of Fin X
x9 \/ {y} is non empty finite set
(x9 \/ {y}) \/ {x9} is non empty finite set
(x9 \ {y}) \/ {y} is non empty finite set
((x9 \ {y}) \/ {y}) \/ {x9} is non empty finite set
(X,(X,(X,x9,(X,y)),(X,x9)),(X,y)) is non empty finite Element of Fin X
B2 . (X,x9,(X,x9)) is Element of Y
i . (X,(X,x9,(X,y)),(X,x9)) is Element of Y
Z . ((i . (X,(X,x9,(X,y)),(X,x9))),(g . y)) is Element of Y
[(i . (X,(X,x9,(X,y)),(X,x9))),(g . y)] is set
{(i . (X,(X,x9,(X,y)),(X,x9))),(g . y)} is non empty finite set
{(i . (X,(X,x9,(X,y)),(X,x9)))} is non empty finite set
{{(i . (X,(X,x9,(X,y)),(X,x9))),(g . y)},{(i . (X,(X,x9,(X,y)),(X,x9)))}} is non empty finite V30() set
Z . [(i . (X,(X,x9,(X,y)),(X,x9))),(g . y)] is set
i . (X,x9,(X,y)) is Element of Y
Z . ((i . (X,x9,(X,y))),(g . x9)) is Element of Y
[(i . (X,x9,(X,y))),(g . x9)] is set
{(i . (X,x9,(X,y))),(g . x9)} is non empty finite set
{(i . (X,x9,(X,y)))} is non empty finite set
{{(i . (X,x9,(X,y))),(g . x9)},{(i . (X,x9,(X,y)))}} is non empty finite V30() set
Z . [(i . (X,x9,(X,y))),(g . x9)] is set
Z . ((Z . ((i . (X,x9,(X,y))),(g . x9))),(g . y)) is Element of Y
[(Z . ((i . (X,x9,(X,y))),(g . x9))),(g . y)] is set
{(Z . ((i . (X,x9,(X,y))),(g . x9))),(g . y)} is non empty finite set
{(Z . ((i . (X,x9,(X,y))),(g . x9)))} is non empty finite set
{{(Z . ((i . (X,x9,(X,y))),(g . x9))),(g . y)},{(Z . ((i . (X,x9,(X,y))),(g . x9)))}} is non empty finite V30() set
Z . [(Z . ((i . (X,x9,(X,y))),(g . x9))),(g . y)] is set
Z . ((g . x9),(g . y)) is Element of Y
[(g . x9),(g . y)] is set
{(g . x9),(g . y)} is non empty finite set
{(g . x9)} is non empty finite set
{{(g . x9),(g . y)},{(g . x9)}} is non empty finite V30() set
Z . [(g . x9),(g . y)] is set
Z . ((i . (X,x9,(X,y))),(Z . ((g . x9),(g . y)))) is Element of Y
[(i . (X,x9,(X,y))),(Z . ((g . x9),(g . y)))] is set
{(i . (X,x9,(X,y))),(Z . ((g . x9),(g . y)))} is non empty finite set
{{(i . (X,x9,(X,y))),(Z . ((g . x9),(g . y)))},{(i . (X,x9,(X,y)))}} is non empty finite V30() set
Z . [(i . (X,x9,(X,y))),(Z . ((g . x9),(g . y)))] is set
i . (x9 \ {y}) is set
Z . ((g . y),(g . x9)) is Element of Y
[(g . y),(g . x9)] is set
{(g . y),(g . x9)} is non empty finite set
{(g . y)} is non empty finite set
{{(g . y),(g . x9)},{(g . y)}} is non empty finite V30() set
Z . [(g . y),(g . x9)] is set
Z . ((i . (x9 \ {y})),(Z . ((g . y),(g . x9)))) is set
[(i . (x9 \ {y})),(Z . ((g . y),(g . x9)))] is set
{(i . (x9 \ {y})),(Z . ((g . y),(g . x9)))} is non empty finite set
{(i . (x9 \ {y}))} is non empty finite set
{{(i . (x9 \ {y})),(Z . ((g . y),(g . x9)))},{(i . (x9 \ {y}))}} is non empty finite V30() set
Z . [(i . (x9 \ {y})),(Z . ((g . y),(g . x9)))] is set
Z . ((i . (X,x9,(X,y))),(g . y)) is Element of Y
[(i . (X,x9,(X,y))),(g . y)] is set
{(i . (X,x9,(X,y))),(g . y)} is non empty finite set
{{(i . (X,x9,(X,y))),(g . y)},{(i . (X,x9,(X,y)))}} is non empty finite V30() set
Z . [(i . (X,x9,(X,y))),(g . y)] is set
Z . ((Z . ((i . (X,x9,(X,y))),(g . y))),(g . x9)) is Element of Y
[(Z . ((i . (X,x9,(X,y))),(g . y))),(g . x9)] is set
{(Z . ((i . (X,x9,(X,y))),(g . y))),(g . x9)} is non empty finite set
{(Z . ((i . (X,x9,(X,y))),(g . y)))} is non empty finite set
{{(Z . ((i . (X,x9,(X,y))),(g . y))),(g . x9)},{(Z . ((i . (X,x9,(X,y))),(g . y)))}} is non empty finite V30() set
Z . [(Z . ((i . (X,x9,(X,y))),(g . y))),(g . x9)] is set
(X,(X,x9,(X,y)),(X,y)) is non empty finite Element of Fin X
B2 . (X,(X,x9,(X,y)),(X,y)) is Element of Y
Z . ((B2 . (X,(X,x9,(X,y)),(X,y))),(g . x9)) is Element of Y
[(B2 . (X,(X,x9,(X,y)),(X,y))),(g . x9)] is set
{(B2 . (X,(X,x9,(X,y)),(X,y))),(g . x9)} is non empty finite set
{(B2 . (X,(X,x9,(X,y)),(X,y)))} is non empty finite set
{{(B2 . (X,(X,x9,(X,y)),(X,y))),(g . x9)},{(B2 . (X,(X,x9,(X,y)),(X,y)))}} is non empty finite V30() set
Z . [(B2 . (X,(X,x9,(X,y)),(X,y))),(g . x9)] is set
B2 . (x9 \/ {y}) is set
Z . ((B2 . (x9 \/ {y})),(g . x9)) is set
[(B2 . (x9 \/ {y})),(g . x9)] is set
{(B2 . (x9 \/ {y})),(g . x9)} is non empty finite set
{(B2 . (x9 \/ {y}))} is non empty finite set
{{(B2 . (x9 \/ {y})),(g . x9)},{(B2 . (x9 \/ {y}))}} is non empty finite V30() set
Z . [(B2 . (x9 \/ {y})),(g . x9)] is set
C is finite Element of Fin X
C \/ {y} is non empty finite set
(X,B,x9) is finite Element of Fin X
C is finite Element of Fin X
C \/ {y} is non empty finite set
(X,x9) is non empty finite Element of Fin X
(X,x9,(X,x9)) is non empty finite Element of Fin X
B2 . (X,x9,(X,x9)) is Element of Y
i . (X,x9,(X,x9)) is Element of Y
i . x9 is Element of Y
Z . ((i . x9),(g . x9)) is Element of Y
[(i . x9),(g . x9)] is set
{(i . x9),(g . x9)} is non empty finite set
{(i . x9)} is non empty finite set
{{(i . x9),(g . x9)},{(i . x9)}} is non empty finite V30() set
Z . [(i . x9),(g . x9)] is set
(X,x9) is non empty finite Element of Fin X
(X,x9,(X,x9)) is non empty finite Element of Fin X
B2 . (X,x9,(X,x9)) is Element of Y
i . x9 is Element of Y
Z . ((i . x9),(g . x9)) is Element of Y
[(i . x9),(g . x9)] is set
{(i . x9),(g . x9)} is non empty finite set
{(i . x9)} is non empty finite set
{{(i . x9),(g . x9)},{(i . x9)}} is non empty finite V30() set
Z . [(i . x9),(g . x9)] is set
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
the_unity_wrt Z is Element of Y
B is Element of Y
B is Element of Y
y is finite Element of Fin X
i is Element of X
{i} is non empty finite set
g . i is Element of Y
i9 is Element of Y
B2 is Element of X
{B2} is non empty finite set
g . B2 is Element of Y
i is Element of Y
i9 is Element of X
{i9} is non empty finite set
g . i9 is Element of Y
i is Element of X
{i} is non empty finite set
i9 is Element of Y
B2 is Element of X
{B2} is non empty finite set
x9 is Element of Y
x9 is Element of X
{x9} is non empty finite set
y is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
i is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
i . {} is set
B2 is Element of Y
i9 is finite Element of Fin X
x9 is Element of X
{x9} is non empty finite set
i9 is Element of X
(X,i9) is non empty finite Element of Fin X
i . (X,i9) is Element of Y
g . i9 is Element of Y
i9 is finite Element of Fin X
B2 is Element of X
(X,(X),i9) is Relation-like finite Element of Fin X
{B2} is non empty finite set
i9 \/ {B2} is non empty finite set
i . (i9 \/ {B2}) is set
i . i9 is Element of Y
g . B2 is Element of Y
Z . ((i . i9),(g . B2)) is Element of Y
[(i . i9),(g . B2)] is set
{(i . i9),(g . B2)} is non empty finite set
{(i . i9)} is non empty finite set
{{(i . i9),(g . B2)},{(i . i9)}} is non empty finite V30() set
Z . [(i . i9),(g . B2)] is set
B is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
B . {} is set
B . f is Element of Y
y is Element of Y
i is Element of X
{i} is non empty finite set
B . {i} is set
g . i is Element of Y
i9 is finite Element of Fin X
B2 is Element of X
(X,f,i9) is finite Element of Fin X
{B2} is non empty finite set
i9 \/ {B2} is non empty finite set
B . (i9 \/ {B2}) is set
B . i9 is Element of Y
g . B2 is Element of Y
Z . ((B . i9),(g . B2)) is Element of Y
[(B . i9),(g . B2)] is set
{(B . i9),(g . B2)} is non empty finite set
{(B . i9)} is non empty finite set
{{(B . i9),(g . B2)},{(B . i9)}} is non empty finite V30() set
Z . [(B . i9),(g . B2)] is set
B is Element of Y
y is Element of Y
i is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
i . f is Element of Y
i . {} is set
i9 is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
i9 . f is Element of Y
i9 . {} is set
the_unity_wrt Z is Element of Y
B2 is finite Element of Fin X
i . B2 is set
i9 . B2 is set
x9 is Element of X
{x9} is non empty finite set
B2 \/ {x9} is non empty finite set
i . (B2 \/ {x9}) is set
i9 . (B2 \/ {x9}) is set
i . B2 is Element of Y
i9 . B2 is Element of Y
(X,f,B2) is finite Element of Fin X
g . x9 is Element of Y
g . x9 is Element of Y
Z . ((i . B2),(g . x9)) is Element of Y
[(i . B2),(g . x9)] is set
{(i . B2),(g . x9)} is non empty finite set
{(i . B2)} is non empty finite set
{{(i . B2),(g . x9)},{(i . B2)}} is non empty finite V30() set
Z . [(i . B2),(g . x9)] is set
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
i . (X) is set
i9 . (X) is set
Y is non empty set
K28(Y,Y) is Relation-like non empty set
K28(K28(Y,Y),Y) is Relation-like non empty set
K27(K28(K28(Y,Y),Y)) is non empty cup-closed diff-closed preBoolean set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
K28((Fin X),Y) is Relation-like non empty set
K27(K28((Fin X),Y)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(Y,Y) -defined Y -valued Function-like non empty V14(K28(Y,Y)) V18(K28(Y,Y),Y) Element of K27(K28(K28(Y,Y),Y))
f is finite Element of Fin X
g is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
(X,Y,Z,f,g) is Element of Y
B is Element of Y
y is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
y . f is Element of Y
y . {} is set
i is finite Element of Fin X
y . i is Element of Y
i9 is Element of X
{i9} is non empty finite set
i \/ {i9} is non empty finite set
y . (i \/ {i9}) is set
g . i9 is Element of Y
Z . ((y . i),(g . i9)) is Element of Y
[(y . i),(g . i9)] is set
{(y . i),(g . i9)} is non empty finite set
{(y . i)} is non empty finite set
{{(y . i),(g . i9)},{(y . i)}} is non empty finite V30() set
Z . [(y . i),(g . i9)] is set
i \ {i9} is finite Element of K27(i)
K27(i) is non empty finite V30() cup-closed diff-closed preBoolean set
f \ (i \ {i9}) is finite Element of K27(f)
K27(f) is non empty finite V30() cup-closed diff-closed preBoolean set
Z . ((g . i9),(g . i9)) is Element of Y
[(g . i9),(g . i9)] is set
{(g . i9),(g . i9)} is non empty finite set
{(g . i9)} is non empty finite set
{{(g . i9),(g . i9)},{(g . i9)}} is non empty finite V30() set
Z . [(g . i9),(g . i9)] is set
(X,i9) is non empty finite Element of Fin X
(X,i,(X,i9)) is finite Element of Fin X
(X,(X,i,(X,i9)),(X,i9)) is non empty finite Element of Fin X
y . (X,(X,i,(X,i9)),(X,i9)) is Element of Y
y . (X,i,(X,i9)) is Element of Y
Z . ((y . (X,i,(X,i9))),(g . i9)) is Element of Y
[(y . (X,i,(X,i9))),(g . i9)] is set
{(y . (X,i,(X,i9))),(g . i9)} is non empty finite set
{(y . (X,i,(X,i9)))} is non empty finite set
{{(y . (X,i,(X,i9))),(g . i9)},{(y . (X,i,(X,i9)))}} is non empty finite V30() set
Z . [(y . (X,i,(X,i9))),(g . i9)] is set
y . (i \ {i9}) is set
Z . ((g . i9),(g . i9)) is Element of Y
[(g . i9),(g . i9)] is set
{(g . i9),(g . i9)} is non empty finite set
{(g . i9)} is non empty finite set
{{(g . i9),(g . i9)},{(g . i9)}} is non empty finite V30() set
Z . [(g . i9),(g . i9)] is set
Z . ((y . (i \ {i9})),(Z . ((g . i9),(g . i9)))) is set
[(y . (i \ {i9})),(Z . ((g . i9),(g . i9)))] is set
{(y . (i \ {i9})),(Z . ((g . i9),(g . i9)))} is non empty finite set
{(y . (i \ {i9}))} is non empty finite set
{{(y . (i \ {i9})),(Z . ((g . i9),(g . i9)))},{(y . (i \ {i9}))}} is non empty finite V30() set
Z . [(y . (i \ {i9})),(Z . ((g . i9),(g . i9)))] is set
Z . ((Z . ((y . (X,i,(X,i9))),(g . i9))),(g . i9)) is Element of Y
[(Z . ((y . (X,i,(X,i9))),(g . i9))),(g . i9)] is set
{(Z . ((y . (X,i,(X,i9))),(g . i9))),(g . i9)} is non empty finite set
{(Z . ((y . (X,i,(X,i9))),(g . i9)))} is non empty finite set
{{(Z . ((y . (X,i,(X,i9))),(g . i9))),(g . i9)},{(Z . ((y . (X,i,(X,i9))),(g . i9)))}} is non empty finite V30() set
Z . [(Z . ((y . (X,i,(X,i9))),(g . i9))),(g . i9)] is set
(X,f,i) is finite Element of Fin X
y is Relation-like Fin X -defined Y -valued Function-like non empty V14( Fin X) V18( Fin X,Y) Element of K27(K28((Fin X),Y))
y . f is Element of Y
y . {} is set
i is finite Element of Fin X
(X,f,i) is finite Element of Fin X
y . i is Element of Y
i9 is Element of X
{i9} is non empty finite set
i \/ {i9} is non empty finite set
y . (i \/ {i9}) is set
g . i9 is Element of Y
Z . ((y . i),(g . i9)) is Element of Y
[(y . i),(g . i9)] is set
{(y . i),(g . i9)} is non empty finite set
{(y . i)} is non empty finite set
{{(y . i),(g . i9)},{(y . i)}} is non empty finite V30() set
Z . [(y . i),(g . i9)] is set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
g is Element of Y
(Y,g) is non empty finite Element of Fin Y
Fin Y is non empty cup-closed diff-closed preBoolean set
(Y,X,Z,(Y,g),f) is Element of X
f . g is Element of X
K28((Fin Y),X) is Relation-like non empty set
K27(K28((Fin Y),X)) is non empty cup-closed diff-closed preBoolean set
{g} is non empty finite set
B is Relation-like Fin Y -defined X -valued Function-like non empty V14( Fin Y) V18( Fin Y,X) Element of K27(K28((Fin Y),X))
B . {g} is set
B . {} is set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
g is Element of Y
B is Element of Y
(Y,g,B) is non empty finite Element of Fin Y
Fin Y is non empty cup-closed diff-closed preBoolean set
(Y,X,Z,(Y,g,B),f) is Element of X
f . g is Element of X
f . B is Element of X
Z . ((f . g),(f . B)) is Element of X
[(f . g),(f . B)] is set
{(f . g),(f . B)} is non empty finite set
{(f . g)} is non empty finite set
{{(f . g),(f . B)},{(f . g)}} is non empty finite V30() set
Z . [(f . g),(f . B)] is set
K28((Fin Y),X) is Relation-like non empty set
K27(K28((Fin Y),X)) is non empty cup-closed diff-closed preBoolean set
{g,B} is non empty finite set
y is Relation-like Fin Y -defined X -valued Function-like non empty V14( Fin Y) V18( Fin Y,X) Element of K27(K28((Fin Y),X))
y . {g,B} is set
y . {} is set
(Y,g) is non empty finite Element of Fin Y
(Y,B) is non empty finite Element of Fin Y
(Y,(Y,g),(Y,B)) is non empty finite Element of Fin Y
y . (Y,(Y,g),(Y,B)) is Element of X
y . (Y,g) is Element of X
Z . ((y . (Y,g)),(f . B)) is Element of X
[(y . (Y,g)),(f . B)] is set
{(y . (Y,g)),(f . B)} is non empty finite set
{(y . (Y,g))} is non empty finite set
{{(y . (Y,g)),(f . B)},{(y . (Y,g))}} is non empty finite V30() set
Z . [(y . (Y,g)),(f . B)] is set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
g is Element of Y
B is Element of Y
y is Element of Y
(Y,g,B,y) is non empty finite Element of Fin Y
Fin Y is non empty cup-closed diff-closed preBoolean set
(Y,X,Z,(Y,g,B,y),f) is Element of X
f . g is Element of X
f . B is Element of X
Z . ((f . g),(f . B)) is Element of X
[(f . g),(f . B)] is set
{(f . g),(f . B)} is non empty finite set
{(f . g)} is non empty finite set
{{(f . g),(f . B)},{(f . g)}} is non empty finite V30() set
Z . [(f . g),(f . B)] is set
f . y is Element of X
Z . ((Z . ((f . g),(f . B))),(f . y)) is Element of X
[(Z . ((f . g),(f . B))),(f . y)] is set
{(Z . ((f . g),(f . B))),(f . y)} is non empty finite set
{(Z . ((f . g),(f . B)))} is non empty finite set
{{(Z . ((f . g),(f . B))),(f . y)},{(Z . ((f . g),(f . B)))}} is non empty finite V30() set
Z . [(Z . ((f . g),(f . B))),(f . y)] is set
K28((Fin Y),X) is Relation-like non empty set
K27(K28((Fin Y),X)) is non empty cup-closed diff-closed preBoolean set
{g,B,y} is non empty finite set
i is Relation-like Fin Y -defined X -valued Function-like non empty V14( Fin Y) V18( Fin Y,X) Element of K27(K28((Fin Y),X))
i . {g,B,y} is set
i . {} is set
{g,B} is non empty finite set
i . {g,B} is set
{g} is non empty finite set
{B} is non empty finite set
{g} \/ {B} is non empty finite set
i . ({g} \/ {B}) is set
(Y,g) is non empty finite Element of Fin Y
i . (Y,g) is Element of X
Z . ((i . (Y,g)),(f . B)) is Element of X
[(i . (Y,g)),(f . B)] is set
{(i . (Y,g)),(f . B)} is non empty finite set
{(i . (Y,g))} is non empty finite set
{{(i . (Y,g)),(f . B)},{(i . (Y,g))}} is non empty finite V30() set
Z . [(i . (Y,g)),(f . B)] is set
(Y,g,B) is non empty finite Element of Fin Y
(Y,y) is non empty finite Element of Fin Y
(Y,(Y,g,B),(Y,y)) is non empty finite Element of Fin Y
i . (Y,(Y,g,B),(Y,y)) is Element of X
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is finite Element of Fin Y
g is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
(Y,X,Z,f,g) is Element of X
K28((Fin Y),X) is Relation-like non empty set
K27(K28((Fin Y),X)) is non empty cup-closed diff-closed preBoolean set
B is Relation-like Fin Y -defined X -valued Function-like non empty V14( Fin Y) V18( Fin Y,X) Element of K27(K28((Fin Y),X))
B . f is Element of X
B . {} is set
y is Element of Y
(Y,y) is non empty finite Element of Fin Y
(Y,f,(Y,y)) is non empty finite Element of Fin Y
(Y,X,Z,(Y,f,(Y,y)),g) is Element of X
g . y is Element of X
Z . ((Y,X,Z,f,g),(g . y)) is Element of X
[(Y,X,Z,f,g),(g . y)] is set
{(Y,X,Z,f,g),(g . y)} is non empty finite set
{(Y,X,Z,f,g)} is non empty finite set
{{(Y,X,Z,f,g),(g . y)},{(Y,X,Z,f,g)}} is non empty finite V30() set
Z . [(Y,X,Z,f,g),(g . y)] is set
{y} is non empty finite set
f \/ {y} is non empty finite set
i is Relation-like Fin Y -defined X -valued Function-like non empty V14( Fin Y) V18( Fin Y,X) Element of K27(K28((Fin Y),X))
i . (Y,f,(Y,y)) is Element of X
i . {} is set
i9 is finite Element of Fin Y
i . i9 is set
B . i9 is set
B2 is Element of Y
{B2} is non empty finite set
i9 \/ {B2} is non empty finite set
i . (i9 \/ {B2}) is set
B . (i9 \/ {B2}) is set
i . i9 is Element of X
B . i9 is Element of X
g . B2 is Element of X
g . B2 is Element of X
Z . ((B . i9),(g . B2)) is Element of X
[(B . i9),(g . B2)] is set
{(B . i9),(g . B2)} is non empty finite set
{(B . i9)} is non empty finite set
{{(B . i9),(g . B2)},{(B . i9)}} is non empty finite V30() set
Z . [(B . i9),(g . B2)] is set
(Y) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Y
i . (Y) is set
B . (Y) is set
i . f is Element of X
Z . ((i . f),(g . y)) is Element of X
[(i . f),(g . y)] is set
{(i . f),(g . y)} is non empty finite set
{(i . f)} is non empty finite set
{{(i . f),(g . y)},{(i . f)}} is non empty finite V30() set
Z . [(i . f),(g . y)] is set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Fin Y is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
g is finite Element of Fin Y
B is finite Element of Fin Y
(Y,g,B) is finite Element of Fin Y
(Y,X,Z,(Y,g,B),f) is Element of X
(Y,X,Z,g,f) is Element of X
(Y,X,Z,B,f) is Element of X
Z . ((Y,X,Z,g,f),(Y,X,Z,B,f)) is Element of X
[(Y,X,Z,g,f),(Y,X,Z,B,f)] is set
{(Y,X,Z,g,f),(Y,X,Z,B,f)} is non empty finite set
{(Y,X,Z,g,f)} is non empty finite set
{{(Y,X,Z,g,f),(Y,X,Z,B,f)},{(Y,X,Z,g,f)}} is non empty finite V30() set
Z . [(Y,X,Z,g,f),(Y,X,Z,B,f)] is set
y is finite Element of Fin Y
(Y,g,y) is finite Element of Fin Y
(Y,X,Z,(Y,g,y),f) is Element of X
(Y,X,Z,y,f) is Element of X
Z . ((Y,X,Z,g,f),(Y,X,Z,y,f)) is Element of X
[(Y,X,Z,g,f),(Y,X,Z,y,f)] is set
{(Y,X,Z,g,f),(Y,X,Z,y,f)} is non empty finite set
{{(Y,X,Z,g,f),(Y,X,Z,y,f)},{(Y,X,Z,g,f)}} is non empty finite V30() set
Z . [(Y,X,Z,g,f),(Y,X,Z,y,f)] is set
i is Element of Y
(Y,i) is non empty finite Element of Fin Y
(Y,y,(Y,i)) is non empty finite Element of Fin Y
(Y,g,(Y,y,(Y,i))) is non empty finite Element of Fin Y
(Y,X,Z,(Y,g,(Y,y,(Y,i))),f) is Element of X
(Y,X,Z,(Y,y,(Y,i)),f) is Element of X
Z . ((Y,X,Z,g,f),(Y,X,Z,(Y,y,(Y,i)),f)) is Element of X
[(Y,X,Z,g,f),(Y,X,Z,(Y,y,(Y,i)),f)] is set
{(Y,X,Z,g,f),(Y,X,Z,(Y,y,(Y,i)),f)} is non empty finite set
{{(Y,X,Z,g,f),(Y,X,Z,(Y,y,(Y,i)),f)},{(Y,X,Z,g,f)}} is non empty finite V30() set
Z . [(Y,X,Z,g,f),(Y,X,Z,(Y,y,(Y,i)),f)] is set
{i} is non empty finite set
y \/ {i} is non empty finite set
f . i is Element of X
Z . ((Y,X,Z,g,f),(f . i)) is Element of X
[(Y,X,Z,g,f),(f . i)] is set
{(Y,X,Z,g,f),(f . i)} is non empty finite set
{{(Y,X,Z,g,f),(f . i)},{(Y,X,Z,g,f)}} is non empty finite V30() set
Z . [(Y,X,Z,g,f),(f . i)] is set
(Y,(Y,g,y),(Y,i)) is non empty finite Element of Fin Y
(Y,X,Z,(Y,(Y,g,y),(Y,i)),f) is Element of X
f . i is Element of X
Z . ((Z . ((Y,X,Z,g,f),(Y,X,Z,y,f))),(f . i)) is Element of X
[(Z . ((Y,X,Z,g,f),(Y,X,Z,y,f))),(f . i)] is set
{(Z . ((Y,X,Z,g,f),(Y,X,Z,y,f))),(f . i)} is non empty finite set
{(Z . ((Y,X,Z,g,f),(Y,X,Z,y,f)))} is non empty finite set
{{(Z . ((Y,X,Z,g,f),(Y,X,Z,y,f))),(f . i)},{(Z . ((Y,X,Z,g,f),(Y,X,Z,y,f)))}} is non empty finite V30() set
Z . [(Z . ((Y,X,Z,g,f),(Y,X,Z,y,f))),(f . i)] is set
Z . ((Y,X,Z,y,f),(f . i)) is Element of X
[(Y,X,Z,y,f),(f . i)] is set
{(Y,X,Z,y,f),(f . i)} is non empty finite set
{(Y,X,Z,y,f)} is non empty finite set
{{(Y,X,Z,y,f),(f . i)},{(Y,X,Z,y,f)}} is non empty finite V30() set
Z . [(Y,X,Z,y,f),(f . i)] is set
Z . ((Y,X,Z,g,f),(Z . ((Y,X,Z,y,f),(f . i)))) is Element of X
[(Y,X,Z,g,f),(Z . ((Y,X,Z,y,f),(f . i)))] is set
{(Y,X,Z,g,f),(Z . ((Y,X,Z,y,f),(f . i)))} is non empty finite set
{{(Y,X,Z,g,f),(Z . ((Y,X,Z,y,f),(f . i)))},{(Y,X,Z,g,f)}} is non empty finite V30() set
Z . [(Y,X,Z,g,f),(Z . ((Y,X,Z,y,f),(f . i)))] is set
(Y) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Y
(Y,g,(Y)) is finite Element of Fin Y
(Y,X,Z,(Y,g,(Y)),f) is Element of X
(Y,X,Z,(Y),f) is Element of X
Z . ((Y,X,Z,g,f),(Y,X,Z,(Y),f)) is Element of X
[(Y,X,Z,g,f),(Y,X,Z,(Y),f)] is set
{(Y,X,Z,g,f),(Y,X,Z,(Y),f)} is non empty finite set
{{(Y,X,Z,g,f),(Y,X,Z,(Y),f)},{(Y,X,Z,g,f)}} is non empty finite V30() set
Z . [(Y,X,Z,g,f),(Y,X,Z,(Y),f)] is set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is finite Element of Fin Y
g is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
(Y,X,Z,f,g) is Element of X
B is Element of Y
g . B is Element of X
Z . ((g . B),(Y,X,Z,f,g)) is Element of X
[(g . B),(Y,X,Z,f,g)] is set
{(g . B),(Y,X,Z,f,g)} is non empty finite set
{(g . B)} is non empty finite set
{{(g . B),(Y,X,Z,f,g)},{(g . B)}} is non empty finite V30() set
Z . [(g . B),(Y,X,Z,f,g)] is set
(Y,B) is non empty finite Element of Fin Y
(Y,X,Z,(Y,B),g) is Element of X
Z . ((Y,X,Z,(Y,B),g),(Y,X,Z,f,g)) is Element of X
[(Y,X,Z,(Y,B),g),(Y,X,Z,f,g)] is set
{(Y,X,Z,(Y,B),g),(Y,X,Z,f,g)} is non empty finite set
{(Y,X,Z,(Y,B),g)} is non empty finite set
{{(Y,X,Z,(Y,B),g),(Y,X,Z,f,g)},{(Y,X,Z,(Y,B),g)}} is non empty finite V30() set
Z . [(Y,X,Z,(Y,B),g),(Y,X,Z,f,g)] is set
(Y,(Y,B),f) is non empty finite Element of Fin Y
(Y,X,Z,(Y,(Y,B),f),g) is Element of X
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Fin Y is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
g is finite Element of Fin Y
B is finite Element of Fin Y
(Y,X,Z,g,f) is Element of X
(Y,X,Z,B,f) is Element of X
Z . ((Y,X,Z,g,f),(Y,X,Z,B,f)) is Element of X
[(Y,X,Z,g,f),(Y,X,Z,B,f)] is set
{(Y,X,Z,g,f),(Y,X,Z,B,f)} is non empty finite set
{(Y,X,Z,g,f)} is non empty finite set
{{(Y,X,Z,g,f),(Y,X,Z,B,f)},{(Y,X,Z,g,f)}} is non empty finite V30() set
Z . [(Y,X,Z,g,f),(Y,X,Z,B,f)] is set
(Y,g,B) is finite Element of Fin Y
(Y,X,Z,(Y,g,B),f) is Element of X
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is finite Element of Fin Y
g is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
(Y,X,Z,f,g) is Element of X
B is Element of X
y is non empty finite Element of Fin Y
(Y,X,Z,y,g) is Element of X
i is non empty finite Element of Fin Y
(Y,X,Z,i,g) is Element of X
(Y,y,i) is non empty finite Element of Fin Y
(Y,X,Z,(Y,y,i),g) is Element of X
i9 is Element of Y
g . i9 is Element of X
i9 is Element of Y
g . i9 is Element of X
Z . (B,B) is Element of X
[B,B] is set
{B,B} is non empty finite set
{B} is non empty finite set
{{B,B},{B}} is non empty finite V30() set
Z . [B,B] is set
i9 is Element of Y
g . i9 is Element of X
B2 is Element of Y
g . B2 is Element of X
y is Element of Y
(Y,y) is non empty finite Element of Fin Y
(Y,X,Z,(Y,y),g) is Element of X
{y} is non empty finite set
g . y is Element of X
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,Y) is Relation-like non empty set
K28(K28(Y,Y),Y) is Relation-like non empty set
K27(K28(K28(Y,Y),Y)) is non empty cup-closed diff-closed preBoolean set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(Y,Y) -defined Y -valued Function-like non empty V14(K28(Y,Y)) V18(K28(Y,Y),Y) Element of K27(K28(K28(Y,Y),Y))
f is finite Element of Fin X
g is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
g .: f is finite Element of K27(Y)
K27(Y) is non empty cup-closed diff-closed preBoolean set
(X,Y,Z,f,g) is Element of Y
B is Element of Y
{B} is non empty finite set
y is Element of X
g . y is Element of Y
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,Y) is Relation-like non empty set
K28(K28(Y,Y),Y) is Relation-like non empty set
K27(K28(K28(Y,Y),Y)) is non empty cup-closed diff-closed preBoolean set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(Y,Y) -defined Y -valued Function-like non empty V14(K28(Y,Y)) V18(K28(Y,Y),Y) Element of K27(K28(K28(Y,Y),Y))
f is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
g is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
B is finite Element of Fin X
f .: B is finite Element of K27(Y)
K27(Y) is non empty cup-closed diff-closed preBoolean set
(X,Y,Z,B,f) is Element of Y
y is Element of X
(X,y) is non empty finite Element of Fin X
(X,B,(X,y)) is non empty finite Element of Fin X
f .: (X,B,(X,y)) is finite Element of K27(Y)
(X,Y,Z,(X,B,(X,y)),f) is Element of Y
{y} is non empty finite set
B \/ {y} is non empty finite set
i is finite Element of Fin X
g .: i is finite Element of K27(Y)
(X,Y,Z,i,g) is Element of Y
f .: (B \/ {y}) is finite Element of K27(Y)
f . y is Element of Y
i9 is Element of X
f . i9 is Element of Y
Im (f,y) is set
f .: {y} is finite set
(f .: B) \/ (Im (f,y)) is set
{(f . y)} is non empty finite set
(f .: B) \/ {(f . y)} is non empty finite set
Z . ((X,Y,Z,B,f),(f . y)) is Element of Y
[(X,Y,Z,B,f),(f . y)] is set
{(X,Y,Z,B,f),(f . y)} is non empty finite set
{(X,Y,Z,B,f)} is non empty finite set
{{(X,Y,Z,B,f),(f . y)},{(X,Y,Z,B,f)}} is non empty finite V30() set
Z . [(X,Y,Z,B,f),(f . y)] is set
(X,i9) is non empty finite Element of Fin X
(X,B,(X,i9)) is non empty finite Element of Fin X
(X,Y,Z,(X,B,(X,i9)),f) is Element of Y
Z . ((X,Y,Z,(X,B,(X,i9)),f),(f . y)) is Element of Y
[(X,Y,Z,(X,B,(X,i9)),f),(f . y)] is set
{(X,Y,Z,(X,B,(X,i9)),f),(f . y)} is non empty finite set
{(X,Y,Z,(X,B,(X,i9)),f)} is non empty finite set
{{(X,Y,Z,(X,B,(X,i9)),f),(f . y)},{(X,Y,Z,(X,B,(X,i9)),f)}} is non empty finite V30() set
Z . [(X,Y,Z,(X,B,(X,i9)),f),(f . y)] is set
Z . ((X,Y,Z,B,f),(f . i9)) is Element of Y
[(X,Y,Z,B,f),(f . i9)] is set
{(X,Y,Z,B,f),(f . i9)} is non empty finite set
{{(X,Y,Z,B,f),(f . i9)},{(X,Y,Z,B,f)}} is non empty finite V30() set
Z . [(X,Y,Z,B,f),(f . i9)] is set
Z . ((Z . ((X,Y,Z,B,f),(f . i9))),(f . y)) is Element of Y
[(Z . ((X,Y,Z,B,f),(f . i9))),(f . y)] is set
{(Z . ((X,Y,Z,B,f),(f . i9))),(f . y)} is non empty finite set
{(Z . ((X,Y,Z,B,f),(f . i9)))} is non empty finite set
{{(Z . ((X,Y,Z,B,f),(f . i9))),(f . y)},{(Z . ((X,Y,Z,B,f),(f . i9)))}} is non empty finite V30() set
Z . [(Z . ((X,Y,Z,B,f),(f . i9))),(f . y)] is set
Z . ((f . i9),(f . i9)) is Element of Y
[(f . i9),(f . i9)] is set
{(f . i9),(f . i9)} is non empty finite set
{(f . i9)} is non empty finite set
{{(f . i9),(f . i9)},{(f . i9)}} is non empty finite V30() set
Z . [(f . i9),(f . i9)] is set
Z . ((X,Y,Z,B,f),(Z . ((f . i9),(f . i9)))) is Element of Y
[(X,Y,Z,B,f),(Z . ((f . i9),(f . i9)))] is set
{(X,Y,Z,B,f),(Z . ((f . i9),(f . i9)))} is non empty finite set
{{(X,Y,Z,B,f),(Z . ((f . i9),(f . i9)))},{(X,Y,Z,B,f)}} is non empty finite V30() set
Z . [(X,Y,Z,B,f),(Z . ((f . i9),(f . i9)))] is set
f . y is Element of Y
Im (f,y) is set
f .: {y} is finite set
{(f . y)} is non empty finite set
{(f . y)} is non empty finite set
g " {(f . y)} is Element of K27(X)
K27(X) is non empty cup-closed diff-closed preBoolean set
i \ (g " {(f . y)}) is finite Element of K27(i)
K27(i) is non empty finite V30() cup-closed diff-closed preBoolean set
i9 is finite Element of Fin X
g .: (g " {(f . y)}) is Element of K27(Y)
f .: {y} is finite Element of K27(Y)
(f .: B) \/ (f .: {y}) is finite Element of K27(Y)
(f .: B) /\ {(f . y)} is finite Element of K27(Y)
i /\ (g " {(f . y)}) is finite Element of K27(X)
B2 is finite Element of Fin X
(X,i9,B2) is finite Element of Fin X
x9 is Element of X
g . x9 is Element of Y
(f .: B) \ {(f . y)} is finite Element of K27(Y)
Im (f,y) is set
f .: {y} is finite set
(f .: B) \ (Im (f,y)) is finite Element of K27(Y)
((f .: B) \/ (f .: {y})) \ (f .: {y}) is finite Element of K27(Y)
(f .: (B \/ {y})) \ (Im (f,y)) is finite Element of K27(Y)
(g .: i) \ {(f . y)} is finite Element of K27(Y)
g .: i9 is finite Element of K27(Y)
x9 is Element of X
g . x9 is Element of Y
Z . ((X,Y,Z,B,f),(f . y)) is Element of Y
[(X,Y,Z,B,f),(f . y)] is set
{(X,Y,Z,B,f),(f . y)} is non empty finite set
{(X,Y,Z,B,f)} is non empty finite set
{{(X,Y,Z,B,f),(f . y)},{(X,Y,Z,B,f)}} is non empty finite V30() set
Z . [(X,Y,Z,B,f),(f . y)] is set
(X,Y,Z,i9,g) is Element of Y
Z . ((X,Y,Z,i9,g),(f . y)) is Element of Y
[(X,Y,Z,i9,g),(f . y)] is set
{(X,Y,Z,i9,g),(f . y)} is non empty finite set
{(X,Y,Z,i9,g)} is non empty finite set
{{(X,Y,Z,i9,g),(f . y)},{(X,Y,Z,i9,g)}} is non empty finite V30() set
Z . [(X,Y,Z,i9,g),(f . y)] is set
(X,Y,Z,B2,g) is Element of Y
Z . ((X,Y,Z,i9,g),(X,Y,Z,B2,g)) is Element of Y
[(X,Y,Z,i9,g),(X,Y,Z,B2,g)] is set
{(X,Y,Z,i9,g),(X,Y,Z,B2,g)} is non empty finite set
{{(X,Y,Z,i9,g),(X,Y,Z,B2,g)},{(X,Y,Z,i9,g)}} is non empty finite V30() set
Z . [(X,Y,Z,i9,g),(X,Y,Z,B2,g)] is set
f . y is Element of Y
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
f .: (X) is Relation-like non-empty empty-yielding empty proper finite finite-yielding V30() Element of K27(Y)
K27(Y) is non empty cup-closed diff-closed preBoolean set
(X,Y,Z,(X),f) is Element of Y
B is finite Element of Fin X
g .: B is finite Element of K27(Y)
(X,Y,Z,B,g) is Element of Y
B is finite Element of Fin X
f .: B is finite Element of K27(Y)
y is finite Element of Fin X
g .: y is finite Element of K27(Y)
(X,Y,Z,B,f) is Element of Y
(X,Y,Z,y,g) is Element of Y
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
g is finite Element of Fin Y
B is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
(Y,X,Z,g,B) is Element of X
y is Element of X
f . (y,(Y,X,Z,g,B)) is Element of X
[y,(Y,X,Z,g,B)] is set
{y,(Y,X,Z,g,B)} is non empty finite set
{y} is non empty finite set
{{y,(Y,X,Z,g,B)},{y}} is non empty finite V30() set
f . [y,(Y,X,Z,g,B)] is set
f [;] (y,B) is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
(Y,X,Z,g,(f [;] (y,B))) is Element of X
i is non empty finite Element of Fin Y
(Y,X,Z,i,B) is Element of X
f . (y,(Y,X,Z,i,B)) is Element of X
[y,(Y,X,Z,i,B)] is set
{y,(Y,X,Z,i,B)} is non empty finite set
{{y,(Y,X,Z,i,B)},{y}} is non empty finite V30() set
f . [y,(Y,X,Z,i,B)] is set
(Y,X,Z,i,(f [;] (y,B))) is Element of X
i9 is non empty finite Element of Fin Y
(Y,X,Z,i9,B) is Element of X
f . (y,(Y,X,Z,i9,B)) is Element of X
[y,(Y,X,Z,i9,B)] is set
{y,(Y,X,Z,i9,B)} is non empty finite set
{{y,(Y,X,Z,i9,B)},{y}} is non empty finite V30() set
f . [y,(Y,X,Z,i9,B)] is set
(Y,X,Z,i9,(f [;] (y,B))) is Element of X
(Y,i,i9) is non empty finite Element of Fin Y
(Y,X,Z,(Y,i,i9),B) is Element of X
f . (y,(Y,X,Z,(Y,i,i9),B)) is Element of X
[y,(Y,X,Z,(Y,i,i9),B)] is set
{y,(Y,X,Z,(Y,i,i9),B)} is non empty finite set
{{y,(Y,X,Z,(Y,i,i9),B)},{y}} is non empty finite V30() set
f . [y,(Y,X,Z,(Y,i,i9),B)] is set
(Y,X,Z,(Y,i,i9),(f [;] (y,B))) is Element of X
Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B)) is Element of X
[(Y,X,Z,i,B),(Y,X,Z,i9,B)] is set
{(Y,X,Z,i,B),(Y,X,Z,i9,B)} is non empty finite set
{(Y,X,Z,i,B)} is non empty finite set
{{(Y,X,Z,i,B),(Y,X,Z,i9,B)},{(Y,X,Z,i,B)}} is non empty finite V30() set
Z . [(Y,X,Z,i,B),(Y,X,Z,i9,B)] is set
f . (y,(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B)))) is Element of X
[y,(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B)))] is set
{y,(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B)))} is non empty finite set
{{y,(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B)))},{y}} is non empty finite V30() set
f . [y,(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B)))] is set
Z . ((Y,X,Z,i,(f [;] (y,B))),(Y,X,Z,i9,(f [;] (y,B)))) is Element of X
[(Y,X,Z,i,(f [;] (y,B))),(Y,X,Z,i9,(f [;] (y,B)))] is set
{(Y,X,Z,i,(f [;] (y,B))),(Y,X,Z,i9,(f [;] (y,B)))} is non empty finite set
{(Y,X,Z,i,(f [;] (y,B)))} is non empty finite set
{{(Y,X,Z,i,(f [;] (y,B))),(Y,X,Z,i9,(f [;] (y,B)))},{(Y,X,Z,i,(f [;] (y,B)))}} is non empty finite V30() set
Z . [(Y,X,Z,i,(f [;] (y,B))),(Y,X,Z,i9,(f [;] (y,B)))] is set
i is Element of Y
(Y,i) is non empty finite Element of Fin Y
(Y,X,Z,(Y,i),B) is Element of X
f . (y,(Y,X,Z,(Y,i),B)) is Element of X
[y,(Y,X,Z,(Y,i),B)] is set
{y,(Y,X,Z,(Y,i),B)} is non empty finite set
{{y,(Y,X,Z,(Y,i),B)},{y}} is non empty finite V30() set
f . [y,(Y,X,Z,(Y,i),B)] is set
(Y,X,Z,(Y,i),(f [;] (y,B))) is Element of X
B . i is Element of X
f . (y,(B . i)) is Element of X
[y,(B . i)] is set
{y,(B . i)} is non empty finite set
{{y,(B . i)},{y}} is non empty finite V30() set
f . [y,(B . i)] is set
(f [;] (y,B)) . i is Element of X
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
g is finite Element of Fin Y
B is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
(Y,X,Z,g,B) is Element of X
y is Element of X
f . ((Y,X,Z,g,B),y) is Element of X
[(Y,X,Z,g,B),y] is set
{(Y,X,Z,g,B),y} is non empty finite set
{(Y,X,Z,g,B)} is non empty finite set
{{(Y,X,Z,g,B),y},{(Y,X,Z,g,B)}} is non empty finite V30() set
f . [(Y,X,Z,g,B),y] is set
f [:] (B,y) is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
(Y,X,Z,g,(f [:] (B,y))) is Element of X
i is non empty finite Element of Fin Y
(Y,X,Z,i,B) is Element of X
f . ((Y,X,Z,i,B),y) is Element of X
[(Y,X,Z,i,B),y] is set
{(Y,X,Z,i,B),y} is non empty finite set
{(Y,X,Z,i,B)} is non empty finite set
{{(Y,X,Z,i,B),y},{(Y,X,Z,i,B)}} is non empty finite V30() set
f . [(Y,X,Z,i,B),y] is set
(Y,X,Z,i,(f [:] (B,y))) is Element of X
i9 is non empty finite Element of Fin Y
(Y,X,Z,i9,B) is Element of X
f . ((Y,X,Z,i9,B),y) is Element of X
[(Y,X,Z,i9,B),y] is set
{(Y,X,Z,i9,B),y} is non empty finite set
{(Y,X,Z,i9,B)} is non empty finite set
{{(Y,X,Z,i9,B),y},{(Y,X,Z,i9,B)}} is non empty finite V30() set
f . [(Y,X,Z,i9,B),y] is set
(Y,X,Z,i9,(f [:] (B,y))) is Element of X
(Y,i,i9) is non empty finite Element of Fin Y
(Y,X,Z,(Y,i,i9),B) is Element of X
f . ((Y,X,Z,(Y,i,i9),B),y) is Element of X
[(Y,X,Z,(Y,i,i9),B),y] is set
{(Y,X,Z,(Y,i,i9),B),y} is non empty finite set
{(Y,X,Z,(Y,i,i9),B)} is non empty finite set
{{(Y,X,Z,(Y,i,i9),B),y},{(Y,X,Z,(Y,i,i9),B)}} is non empty finite V30() set
f . [(Y,X,Z,(Y,i,i9),B),y] is set
(Y,X,Z,(Y,i,i9),(f [:] (B,y))) is Element of X
Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B)) is Element of X
[(Y,X,Z,i,B),(Y,X,Z,i9,B)] is set
{(Y,X,Z,i,B),(Y,X,Z,i9,B)} is non empty finite set
{{(Y,X,Z,i,B),(Y,X,Z,i9,B)},{(Y,X,Z,i,B)}} is non empty finite V30() set
Z . [(Y,X,Z,i,B),(Y,X,Z,i9,B)] is set
f . ((Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B))),y) is Element of X
[(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B))),y] is set
{(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B))),y} is non empty finite set
{(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B)))} is non empty finite set
{{(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B))),y},{(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B)))}} is non empty finite V30() set
f . [(Z . ((Y,X,Z,i,B),(Y,X,Z,i9,B))),y] is set
Z . ((Y,X,Z,i,(f [:] (B,y))),(Y,X,Z,i9,(f [:] (B,y)))) is Element of X
[(Y,X,Z,i,(f [:] (B,y))),(Y,X,Z,i9,(f [:] (B,y)))] is set
{(Y,X,Z,i,(f [:] (B,y))),(Y,X,Z,i9,(f [:] (B,y)))} is non empty finite set
{(Y,X,Z,i,(f [:] (B,y)))} is non empty finite set
{{(Y,X,Z,i,(f [:] (B,y))),(Y,X,Z,i9,(f [:] (B,y)))},{(Y,X,Z,i,(f [:] (B,y)))}} is non empty finite V30() set
Z . [(Y,X,Z,i,(f [:] (B,y))),(Y,X,Z,i9,(f [:] (B,y)))] is set
i is Element of Y
(Y,i) is non empty finite Element of Fin Y
(Y,X,Z,(Y,i),B) is Element of X
f . ((Y,X,Z,(Y,i),B),y) is Element of X
[(Y,X,Z,(Y,i),B),y] is set
{(Y,X,Z,(Y,i),B),y} is non empty finite set
{(Y,X,Z,(Y,i),B)} is non empty finite set
{{(Y,X,Z,(Y,i),B),y},{(Y,X,Z,(Y,i),B)}} is non empty finite V30() set
f . [(Y,X,Z,(Y,i),B),y] is set
(Y,X,Z,(Y,i),(f [:] (B,y))) is Element of X
B . i is Element of X
f . ((B . i),y) is Element of X
[(B . i),y] is set
{(B . i),y} is non empty finite set
{(B . i)} is non empty finite set
{{(B . i),y},{(B . i)}} is non empty finite V30() set
f . [(B . i),y] is set
(f [:] (B,y)) . i is Element of X
X is non empty set
Y is non empty set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
Fin X is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
f is finite Element of Fin X
Z .: f is finite set
Fin Y is non empty cup-closed diff-closed preBoolean set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
Fin Y is non empty cup-closed diff-closed preBoolean set
Z is non empty set
K28(Y,Z) is Relation-like non empty set
K27(K28(Y,Z)) is non empty cup-closed diff-closed preBoolean set
K28(Z,X) is Relation-like non empty set
K27(K28(Z,X)) is non empty cup-closed diff-closed preBoolean set
f is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
g is finite Element of Fin Y
B is Relation-like Y -defined Z -valued Function-like non empty V14(Y) V18(Y,Z) Element of K27(K28(Y,Z))
(Y,Z,B,g) is finite Element of Fin Z
Fin Z is non empty cup-closed diff-closed preBoolean set
y is Relation-like Z -defined X -valued Function-like non empty V14(Z) V18(Z,X) Element of K27(K28(Z,X))
(Z,X,f,(Y,Z,B,g),y) is Element of X
y * B is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
(Y,X,f,g,(y * B)) is Element of X
dom B is non empty Element of K27(Y)
K27(Y) is non empty cup-closed diff-closed preBoolean set
i is non empty finite Element of Fin Y
(Y,Z,B,i) is finite Element of Fin Z
(Z,X,f,(Y,Z,B,i),y) is Element of X
(Y,X,f,i,(y * B)) is Element of X
i9 is non empty finite Element of Fin Y
(Y,Z,B,i9) is finite Element of Fin Z
(Z,X,f,(Y,Z,B,i9),y) is Element of X
(Y,X,f,i9,(y * B)) is Element of X
(Y,i,i9) is non empty finite Element of Fin Y
(Y,Z,B,(Y,i,i9)) is finite Element of Fin Z
(Z,X,f,(Y,Z,B,(Y,i,i9)),y) is Element of X
(Y,X,f,(Y,i,i9),(y * B)) is Element of X
(Z,(Y,Z,B,i),(Y,Z,B,i9)) is finite Element of Fin Z
(Z,X,f,(Z,(Y,Z,B,i),(Y,Z,B,i9)),y) is Element of X
f . ((Z,X,f,(Y,Z,B,i),y),(Z,X,f,(Y,Z,B,i9),y)) is Element of X
[(Z,X,f,(Y,Z,B,i),y),(Z,X,f,(Y,Z,B,i9),y)] is set
{(Z,X,f,(Y,Z,B,i),y),(Z,X,f,(Y,Z,B,i9),y)} is non empty finite set
{(Z,X,f,(Y,Z,B,i),y)} is non empty finite set
{{(Z,X,f,(Y,Z,B,i),y),(Z,X,f,(Y,Z,B,i9),y)},{(Z,X,f,(Y,Z,B,i),y)}} is non empty finite V30() set
f . [(Z,X,f,(Y,Z,B,i),y),(Z,X,f,(Y,Z,B,i9),y)] is set
i is Element of Y
(Y,i) is non empty finite Element of Fin Y
(Y,Z,B,(Y,i)) is finite Element of Fin Z
(Z,X,f,(Y,Z,B,(Y,i)),y) is Element of X
(Y,X,f,(Y,i),(y * B)) is Element of X
Im (B,i) is set
{i} is non empty finite set
B .: {i} is finite set
B . i is Element of Z
(Z,(B . i)) is non empty finite Element of Fin Z
(Z,X,f,(Z,(B . i)),y) is Element of X
y . (B . i) is Element of X
(y * B) . i is Element of X
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,Y) is Relation-like non empty set
K28(K28(Y,Y),Y) is Relation-like non empty set
K27(K28(K28(Y,Y),Y)) is non empty cup-closed diff-closed preBoolean set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(Y,Y) -defined Y -valued Function-like non empty V14(K28(Y,Y)) V18(K28(Y,Y),Y) Element of K27(K28(K28(Y,Y),Y))
f is non empty set
K28(f,f) is Relation-like non empty set
K28(K28(f,f),f) is Relation-like non empty set
K27(K28(K28(f,f),f)) is non empty cup-closed diff-closed preBoolean set
K28(Y,f) is Relation-like non empty set
K27(K28(Y,f)) is non empty cup-closed diff-closed preBoolean set
g is Relation-like K28(f,f) -defined f -valued Function-like non empty V14(K28(f,f)) V18(K28(f,f),f) Element of K27(K28(K28(f,f),f))
B is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
y is Relation-like Y -defined f -valued Function-like non empty V14(Y) V18(Y,f) Element of K27(K28(Y,f))
y * B is Relation-like X -defined f -valued Function-like non empty V14(X) V18(X,f) Element of K27(K28(X,f))
K28(X,f) is Relation-like non empty set
K27(K28(X,f)) is non empty cup-closed diff-closed preBoolean set
i is finite Element of Fin X
(X,Y,Z,i,B) is Element of Y
y . (X,Y,Z,i,B) is Element of f
(X,f,g,i,(y * B)) is Element of f
i9 is Element of X
(X,i9) is non empty finite Element of Fin X
(X,i,(X,i9)) is non empty finite Element of Fin X
(X,Y,Z,(X,i,(X,i9)),B) is Element of Y
y . (X,Y,Z,(X,i,(X,i9)),B) is Element of f
(X,f,g,(X,i,(X,i9)),(y * B)) is Element of f
{i9} is non empty finite set
i \/ {i9} is non empty finite set
B . i9 is Element of Y
y . (B . i9) is Element of f
(y * B) . i9 is Element of f
B . i9 is Element of Y
Z . ((X,Y,Z,i,B),(B . i9)) is Element of Y
[(X,Y,Z,i,B),(B . i9)] is set
{(X,Y,Z,i,B),(B . i9)} is non empty finite set
{(X,Y,Z,i,B)} is non empty finite set
{{(X,Y,Z,i,B),(B . i9)},{(X,Y,Z,i,B)}} is non empty finite V30() set
Z . [(X,Y,Z,i,B),(B . i9)] is set
y . (Z . ((X,Y,Z,i,B),(B . i9))) is Element of f
y . (B . i9) is Element of f
g . ((y . (X,Y,Z,i,B)),(y . (B . i9))) is Element of f
[(y . (X,Y,Z,i,B)),(y . (B . i9))] is set
{(y . (X,Y,Z,i,B)),(y . (B . i9))} is non empty finite set
{(y . (X,Y,Z,i,B))} is non empty finite set
{{(y . (X,Y,Z,i,B)),(y . (B . i9))},{(y . (X,Y,Z,i,B))}} is non empty finite V30() set
g . [(y . (X,Y,Z,i,B)),(y . (B . i9))] is set
(y * B) . i9 is Element of f
g . ((X,f,g,i,(y * B)),((y * B) . i9)) is Element of f
[(X,f,g,i,(y * B)),((y * B) . i9)] is set
{(X,f,g,i,(y * B)),((y * B) . i9)} is non empty finite set
{(X,f,g,i,(y * B))} is non empty finite set
{{(X,f,g,i,(y * B)),((y * B) . i9)},{(X,f,g,i,(y * B))}} is non empty finite V30() set
g . [(X,f,g,i,(y * B)),((y * B) . i9)] is set
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
(X,Y,Z,(X),B) is Element of Y
y . (X,Y,Z,(X),B) is Element of f
(X,f,g,(X),(y * B)) is Element of f
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
(Y) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Y
Fin Y is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
the_unity_wrt Z is Element of X
f is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
(Y,X,Z,(Y),f) is Element of X
K28((Fin Y),X) is Relation-like non empty set
K27(K28((Fin Y),X)) is non empty cup-closed diff-closed preBoolean set
g is Relation-like Fin Y -defined X -valued Function-like non empty V14( Fin Y) V18( Fin Y,X) Element of K27(K28((Fin Y),X))
g . (Y) is Element of X
g . {} is set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is finite Element of Fin Y
g is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
(Y,X,Z,f,g) is Element of X
B is Element of Y
(Y,B) is non empty finite Element of Fin Y
(Y,f,(Y,B)) is non empty finite Element of Fin Y
(Y,X,Z,(Y,f,(Y,B)),g) is Element of X
g . B is Element of X
Z . ((Y,X,Z,f,g),(g . B)) is Element of X
[(Y,X,Z,f,g),(g . B)] is set
{(Y,X,Z,f,g),(g . B)} is non empty finite set
{(Y,X,Z,f,g)} is non empty finite set
{{(Y,X,Z,f,g),(g . B)},{(Y,X,Z,f,g)}} is non empty finite V30() set
Z . [(Y,X,Z,f,g),(g . B)] is set
(Y) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Y
the_unity_wrt Z is Element of X
Z . ((the_unity_wrt Z),(g . B)) is Element of X
[(the_unity_wrt Z),(g . B)] is set
{(the_unity_wrt Z),(g . B)} is non empty finite set
{(the_unity_wrt Z)} is non empty finite set
{{(the_unity_wrt Z),(g . B)},{(the_unity_wrt Z)}} is non empty finite V30() set
Z . [(the_unity_wrt Z),(g . B)] is set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
Fin Y is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
f is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
g is finite Element of Fin Y
B is finite Element of Fin Y
(Y,g,B) is finite Element of Fin Y
(Y,X,Z,(Y,g,B),f) is Element of X
(Y,X,Z,g,f) is Element of X
(Y,X,Z,B,f) is Element of X
Z . ((Y,X,Z,g,f),(Y,X,Z,B,f)) is Element of X
[(Y,X,Z,g,f),(Y,X,Z,B,f)] is set
{(Y,X,Z,g,f),(Y,X,Z,B,f)} is non empty finite set
{(Y,X,Z,g,f)} is non empty finite set
{{(Y,X,Z,g,f),(Y,X,Z,B,f)},{(Y,X,Z,g,f)}} is non empty finite V30() set
Z . [(Y,X,Z,g,f),(Y,X,Z,B,f)] is set
(Y) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Y
the_unity_wrt Z is Element of X
Z . ((Y,X,Z,g,f),(the_unity_wrt Z)) is Element of X
[(Y,X,Z,g,f),(the_unity_wrt Z)] is set
{(Y,X,Z,g,f),(the_unity_wrt Z)} is non empty finite set
{{(Y,X,Z,g,f),(the_unity_wrt Z)},{(Y,X,Z,g,f)}} is non empty finite V30() set
Z . [(Y,X,Z,g,f),(the_unity_wrt Z)] is set
the_unity_wrt Z is Element of X
Z . ((the_unity_wrt Z),(Y,X,Z,B,f)) is Element of X
[(the_unity_wrt Z),(Y,X,Z,B,f)] is set
{(the_unity_wrt Z),(Y,X,Z,B,f)} is non empty finite set
{(the_unity_wrt Z)} is non empty finite set
{{(the_unity_wrt Z),(Y,X,Z,B,f)},{(the_unity_wrt Z)}} is non empty finite V30() set
Z . [(the_unity_wrt Z),(Y,X,Z,B,f)] is set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,Y) is Relation-like non empty set
K28(K28(Y,Y),Y) is Relation-like non empty set
K27(K28(K28(Y,Y),Y)) is non empty cup-closed diff-closed preBoolean set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(Y,Y) -defined Y -valued Function-like non empty V14(K28(Y,Y)) V18(K28(Y,Y),Y) Element of K27(K28(K28(Y,Y),Y))
f is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
g is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
B is finite Element of Fin X
(X,Y,f,B) is finite Element of Fin Y
Fin Y is non empty cup-closed diff-closed preBoolean set
y is finite Element of Fin X
(X,Y,g,y) is finite Element of Fin Y
(X,Y,Z,B,f) is Element of Y
(X,Y,Z,y,g) is Element of Y
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
the_unity_wrt Z is Element of Y
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
Fin Y is non empty cup-closed diff-closed preBoolean set
Z is non empty set
K28(Y,Z) is Relation-like non empty set
K27(K28(Y,Z)) is non empty cup-closed diff-closed preBoolean set
K28(Z,X) is Relation-like non empty set
K27(K28(Z,X)) is non empty cup-closed diff-closed preBoolean set
f is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
g is finite Element of Fin Y
B is Relation-like Y -defined Z -valued Function-like non empty V14(Y) V18(Y,Z) Element of K27(K28(Y,Z))
(Y,Z,B,g) is finite Element of Fin Z
Fin Z is non empty cup-closed diff-closed preBoolean set
y is Relation-like Z -defined X -valued Function-like non empty V14(Z) V18(Z,X) Element of K27(K28(Z,X))
(Z,X,f,(Y,Z,B,g),y) is Element of X
y * B is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
(Y,X,f,g,(y * B)) is Element of X
(Z) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Z
the_unity_wrt f is Element of X
(Y) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Y
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,Y) is Relation-like non empty set
K28(K28(Y,Y),Y) is Relation-like non empty set
K27(K28(K28(Y,Y),Y)) is non empty cup-closed diff-closed preBoolean set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like K28(Y,Y) -defined Y -valued Function-like non empty V14(K28(Y,Y)) V18(K28(Y,Y),Y) Element of K27(K28(K28(Y,Y),Y))
the_unity_wrt Z is Element of Y
f is non empty set
K28(f,f) is Relation-like non empty set
K28(K28(f,f),f) is Relation-like non empty set
K27(K28(K28(f,f),f)) is non empty cup-closed diff-closed preBoolean set
K28(Y,f) is Relation-like non empty set
K27(K28(Y,f)) is non empty cup-closed diff-closed preBoolean set
g is Relation-like K28(f,f) -defined f -valued Function-like non empty V14(K28(f,f)) V18(K28(f,f),f) Element of K27(K28(K28(f,f),f))
the_unity_wrt g is Element of f
B is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
y is Relation-like Y -defined f -valued Function-like non empty V14(Y) V18(Y,f) Element of K27(K28(Y,f))
y . (the_unity_wrt Z) is Element of f
y * B is Relation-like X -defined f -valued Function-like non empty V14(X) V18(X,f) Element of K27(K28(X,f))
K28(X,f) is Relation-like non empty set
K27(K28(X,f)) is non empty cup-closed diff-closed preBoolean set
i is finite Element of Fin X
(X,Y,Z,i,B) is Element of Y
y . (X,Y,Z,i,B) is Element of f
(X,f,g,i,(y * B)) is Element of f
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
K28((Fin X),(Fin X)) is Relation-like non empty set
K28(K28((Fin X),(Fin X)),(Fin X)) is Relation-like non empty set
K27(K28(K28((Fin X),(Fin X)),(Fin X))) is non empty cup-closed diff-closed preBoolean set
Y is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
Y is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
Z is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
f is finite Element of Fin X
g is finite Element of Fin X
Y . (f,g) is finite Element of Fin X
[f,g] is set
{f,g} is non empty finite V30() set
{f} is non empty finite V30() set
{{f,g},{f}} is non empty finite V30() set
Y . [f,g] is set
(X,f,g) is finite Element of Fin X
Z . (f,g) is finite Element of Fin X
Z . [f,g] is set
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
K28((Fin X),(Fin X)) is Relation-like non empty set
K28(K28((Fin X),(Fin X)),(Fin X)) is Relation-like non empty set
K27(K28(K28((Fin X),(Fin X)),(Fin X))) is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
(X) . (Y,Y) is finite Element of Fin X
[Y,Y] is set
{Y,Y} is non empty finite V30() set
{Y} is non empty finite V30() set
{{Y,Y},{Y}} is non empty finite V30() set
(X) . [Y,Y] is set
(X) . (Y,Y) is finite Element of Fin X
(X,Y,Y) is finite Element of Fin X
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
K28((Fin X),(Fin X)) is Relation-like non empty set
K28(K28((Fin X),(Fin X)),(Fin X)) is Relation-like non empty set
K27(K28(K28((Fin X),(Fin X)),(Fin X))) is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
Z is finite Element of Fin X
(X) . (Y,Z) is finite Element of Fin X
[Y,Z] is set
{Y,Z} is non empty finite V30() set
{Y} is non empty finite V30() set
{{Y,Z},{Y}} is non empty finite V30() set
(X) . [Y,Z] is set
(X) . (Z,Y) is finite Element of Fin X
[Z,Y] is set
{Z,Y} is non empty finite V30() set
{Z} is non empty finite V30() set
{{Z,Y},{Z}} is non empty finite V30() set
(X) . [Z,Y] is set
(X) . (Y,Z) is finite Element of Fin X
(X,Z,Y) is finite Element of Fin X
(X) . (Z,Y) is finite Element of Fin X
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
K28((Fin X),(Fin X)) is Relation-like non empty set
K28(K28((Fin X),(Fin X)),(Fin X)) is Relation-like non empty set
K27(K28(K28((Fin X),(Fin X)),(Fin X))) is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
Z is finite Element of Fin X
(X) . (Y,Z) is finite Element of Fin X
[Y,Z] is set
{Y,Z} is non empty finite V30() set
{Y} is non empty finite V30() set
{{Y,Z},{Y}} is non empty finite V30() set
(X) . [Y,Z] is set
f is finite Element of Fin X
(X) . (Z,f) is finite Element of Fin X
[Z,f] is set
{Z,f} is non empty finite V30() set
{Z} is non empty finite V30() set
{{Z,f},{Z}} is non empty finite V30() set
(X) . [Z,f] is set
(X) . (Y,((X) . (Z,f))) is finite Element of Fin X
[Y,((X) . (Z,f))] is set
{Y,((X) . (Z,f))} is non empty finite V30() set
{{Y,((X) . (Z,f))},{Y}} is non empty finite V30() set
(X) . [Y,((X) . (Z,f))] is set
(X) . (((X) . (Y,Z)),f) is finite Element of Fin X
[((X) . (Y,Z)),f] is set
{((X) . (Y,Z)),f} is non empty finite V30() set
{((X) . (Y,Z))} is non empty finite V30() set
{{((X) . (Y,Z)),f},{((X) . (Y,Z))}} is non empty finite V30() set
(X) . [((X) . (Y,Z)),f] is set
(X) . (Y,Z) is finite Element of Fin X
(X) . (((X) . (Y,Z)),f) is finite Element of Fin X
[((X) . (Y,Z)),f] is set
{((X) . (Y,Z)),f} is non empty finite V30() set
{((X) . (Y,Z))} is non empty finite V30() set
{{((X) . (Y,Z)),f},{((X) . (Y,Z))}} is non empty finite V30() set
(X) . [((X) . (Y,Z)),f] is set
(X,Y,Z) is finite Element of Fin X
(X) . ((X,Y,Z),f) is finite Element of Fin X
[(X,Y,Z),f] is set
{(X,Y,Z),f} is non empty finite V30() set
{(X,Y,Z)} is non empty finite V30() set
{{(X,Y,Z),f},{(X,Y,Z)}} is non empty finite V30() set
(X) . [(X,Y,Z),f] is set
(X,(X,Y,Z),f) is finite Element of Fin X
(X,Z,f) is finite Element of Fin X
(X,Y,(X,Z,f)) is finite Element of Fin X
(X) . (Y,(X,Z,f)) is finite Element of Fin X
[Y,(X,Z,f)] is set
{Y,(X,Z,f)} is non empty finite V30() set
{{Y,(X,Z,f)},{Y}} is non empty finite V30() set
(X) . [Y,(X,Z,f)] is set
(X) . (Z,f) is finite Element of Fin X
(X) . (Y,((X) . (Z,f))) is finite Element of Fin X
[Y,((X) . (Z,f))] is set
{Y,((X) . (Z,f))} is non empty finite V30() set
{{Y,((X) . (Z,f))},{Y}} is non empty finite V30() set
(X) . [Y,((X) . (Z,f))] is set
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
(X) is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
K28((Fin X),(Fin X)) is Relation-like non empty set
K28(K28((Fin X),(Fin X)),(Fin X)) is Relation-like non empty set
K27(K28(K28((Fin X),(Fin X)),(Fin X))) is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
(X) . ((X),Y) is finite Element of Fin X
[(X),Y] is set
{(X),Y} is non empty finite V30() set
{(X)} is non empty finite V30() set
{{(X),Y},{(X)}} is non empty finite V30() set
(X) . [(X),Y] is set
{} \/ Y is finite set
Y is finite Element of Fin X
(X) . (Y,(X)) is finite Element of Fin X
[Y,(X)] is set
{Y,(X)} is non empty finite V30() set
{Y} is non empty finite V30() set
{{Y,(X)},{Y}} is non empty finite V30() set
(X) . [Y,(X)] is set
(X) . (Y,(X)) is finite Element of Fin X
Y \/ {} is finite set
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
K28((Fin X),(Fin X)) is Relation-like non empty set
K28(K28((Fin X),(Fin X)),(Fin X)) is Relation-like non empty set
K27(K28(K28((Fin X),(Fin X)),(Fin X))) is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
K28((Fin X),(Fin X)) is Relation-like non empty set
K28(K28((Fin X),(Fin X)),(Fin X)) is Relation-like non empty set
K27(K28(K28((Fin X),(Fin X)),(Fin X))) is non empty cup-closed diff-closed preBoolean set
the_unity_wrt (X) is finite Element of Fin X
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
K28((Fin X),(Fin X)) is Relation-like non empty set
K28(K28((Fin X),(Fin X)),(Fin X)) is Relation-like non empty set
K27(K28(K28((Fin X),(Fin X)),(Fin X))) is non empty cup-closed diff-closed preBoolean set
the_unity_wrt (X) is finite Element of Fin X
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is finite Element of Fin X
f is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
(X,(Fin Y),(Y),Z,f) is finite Element of Fin Y
X is non empty set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
f is Element of X
(X,f) is non empty finite Element of Fin X
Fin X is non empty cup-closed diff-closed preBoolean set
(X,Y,(X,f),Z) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),(X,f),Z) is finite Element of Fin Y
Z . f is finite Element of Fin Y
X is non empty set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
f is Element of X
Z . f is finite Element of Fin Y
g is Element of X
(X,f,g) is non empty finite Element of Fin X
Fin X is non empty cup-closed diff-closed preBoolean set
(X,Y,(X,f,g),Z) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),(X,f,g),Z) is finite Element of Fin Y
Z . g is finite Element of Fin Y
(Y,(Z . f),(Z . g)) is finite Element of Fin Y
(Y) . ((Z . f),(Z . g)) is finite Element of Fin Y
[(Z . f),(Z . g)] is set
{(Z . f),(Z . g)} is non empty finite V30() set
{(Z . f)} is non empty finite V30() set
{{(Z . f),(Z . g)},{(Z . f)}} is non empty finite V30() set
(Y) . [(Z . f),(Z . g)] is set
X is non empty set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
f is Element of X
Z . f is finite Element of Fin Y
g is Element of X
Z . g is finite Element of Fin Y
(Y,(Z . f),(Z . g)) is finite Element of Fin Y
B is Element of X
(X,f,g,B) is non empty finite Element of Fin X
Fin X is non empty cup-closed diff-closed preBoolean set
(X,Y,(X,f,g,B),Z) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),(X,f,g,B),Z) is finite Element of Fin Y
Z . B is finite Element of Fin Y
(Y,(Y,(Z . f),(Z . g)),(Z . B)) is finite Element of Fin Y
(Y) . ((Z . f),(Z . g)) is finite Element of Fin Y
[(Z . f),(Z . g)] is set
{(Z . f),(Z . g)} is non empty finite V30() set
{(Z . f)} is non empty finite V30() set
{{(Z . f),(Z . g)},{(Z . f)}} is non empty finite V30() set
(Y) . [(Z . f),(Z . g)] is set
(Y) . (((Y) . ((Z . f),(Z . g))),(Z . B)) is finite Element of Fin Y
[((Y) . ((Z . f),(Z . g))),(Z . B)] is set
{((Y) . ((Z . f),(Z . g))),(Z . B)} is non empty finite V30() set
{((Y) . ((Z . f),(Z . g)))} is non empty finite V30() set
{{((Y) . ((Z . f),(Z . g))),(Z . B)},{((Y) . ((Z . f),(Z . g)))}} is non empty finite V30() set
(Y) . [((Y) . ((Z . f),(Z . g))),(Z . B)] is set
(Y) . ((Y,(Z . f),(Z . g)),(Z . B)) is finite Element of Fin Y
[(Y,(Z . f),(Z . g)),(Z . B)] is set
{(Y,(Z . f),(Z . g)),(Z . B)} is non empty finite V30() set
{(Y,(Z . f),(Z . g))} is non empty finite V30() set
{{(Y,(Z . f),(Z . g)),(Z . B)},{(Y,(Z . f),(Z . g))}} is non empty finite V30() set
(Y) . [(Y,(Z . f),(Z . g)),(Z . B)] is set
X is non empty set
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
Fin X is non empty cup-closed diff-closed preBoolean set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
(X,Y,(X),Z) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),(X),Z) is finite Element of Fin Y
the_unity_wrt (Y) is finite Element of Fin Y
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
f is Element of X
(X,f) is non empty finite Element of Fin X
Z . f is finite Element of Fin Y
g is finite Element of Fin X
(X,g,(X,f)) is non empty finite Element of Fin X
(X,Y,(X,g,(X,f)),Z) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),(X,g,(X,f)),Z) is finite Element of Fin Y
(X,Y,g,Z) is finite Element of Fin Y
(X,(Fin Y),(Y),g,Z) is finite Element of Fin Y
(Y,(X,Y,g,Z),(Z . f)) is finite Element of Fin Y
(Y) . ((X,Y,g,Z),(Z . f)) is finite Element of Fin Y
[(X,Y,g,Z),(Z . f)] is set
{(X,Y,g,Z),(Z . f)} is non empty finite V30() set
{(X,Y,g,Z)} is non empty finite V30() set
{{(X,Y,g,Z),(Z . f)},{(X,Y,g,Z)}} is non empty finite V30() set
(Y) . [(X,Y,g,Z),(Z . f)] is set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
f is finite Element of Fin X
(X,Y,f,Z) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),f,Z) is finite Element of Fin Y
(X,(Fin Y),Z,f) is finite Element of Fin (Fin Y)
Fin (Fin Y) is non empty cup-closed diff-closed preBoolean set
union (X,(Fin Y),Z,f) is set
g is Element of X
(X,g) is non empty finite Element of Fin X
(X,f,(X,g)) is non empty finite Element of Fin X
(X,Y,(X,f,(X,g)),Z) is finite Element of Fin Y
(X,(Fin Y),(Y),(X,f,(X,g)),Z) is finite Element of Fin Y
(X,(Fin Y),Z,(X,f,(X,g))) is finite Element of Fin (Fin Y)
union (X,(Fin Y),Z,(X,f,(X,g))) is set
Z . g is finite Element of Fin Y
(union (X,(Fin Y),Z,f)) \/ (Z . g) is set
{(Z . g)} is non empty finite V30() set
union {(Z . g)} is finite set
(union (X,(Fin Y),Z,f)) \/ (union {(Z . g)}) is set
(X,(Fin Y),Z,f) \/ {(Z . g)} is non empty finite set
union ((X,(Fin Y),Z,f) \/ {(Z . g)}) is set
Im (Z,g) is set
{g} is non empty finite set
Z .: {g} is finite set
(X,(Fin Y),Z,f) \/ (Im (Z,g)) is set
union ((X,(Fin Y),Z,f) \/ (Im (Z,g))) is set
f \/ {g} is non empty finite set
Z .: (f \/ {g}) is finite Element of K27((Fin Y))
K27((Fin Y)) is non empty cup-closed diff-closed preBoolean set
union (Z .: (f \/ {g})) is set
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
(X,Y,(X),Z) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),(X),Z) is finite Element of Fin Y
(X,(Fin Y),Z,(X)) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin (Fin Y)
Fin (Fin Y) is non empty cup-closed diff-closed preBoolean set
union (X,(Fin Y),Z,(X)) is finite set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
f is finite Element of Fin X
g is finite Element of Fin X
(X,f,g) is finite Element of Fin X
(X,Y,(X,f,g),Z) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),(X,f,g),Z) is finite Element of Fin Y
(X,Y,f,Z) is finite Element of Fin Y
(X,(Fin Y),(Y),f,Z) is finite Element of Fin Y
(X,Y,g,Z) is finite Element of Fin Y
(X,(Fin Y),(Y),g,Z) is finite Element of Fin Y
(Y,(X,Y,f,Z),(X,Y,g,Z)) is finite Element of Fin Y
(X,(Fin Y),Z,(X,f,g)) is finite Element of Fin (Fin Y)
Fin (Fin Y) is non empty cup-closed diff-closed preBoolean set
union (X,(Fin Y),Z,(X,f,g)) is set
(X,(Fin Y),Z,f) is finite Element of Fin (Fin Y)
(X,(Fin Y),Z,g) is finite Element of Fin (Fin Y)
((Fin Y),(X,(Fin Y),Z,f),(X,(Fin Y),Z,g)) is finite Element of Fin (Fin Y)
union ((Fin Y),(X,(Fin Y),Z,f),(X,(Fin Y),Z,g)) is set
union (X,(Fin Y),Z,f) is set
union (X,(Fin Y),Z,g) is set
(union (X,(Fin Y),Z,f)) \/ (union (X,(Fin Y),Z,g)) is set
(X,Y,f,Z) \/ (union (X,(Fin Y),Z,g)) is set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
Z is set
Fin Z is non empty cup-closed diff-closed preBoolean set
K28(Y,(Fin Z)) is Relation-like non empty set
K27(K28(Y,(Fin Z))) is non empty cup-closed diff-closed preBoolean set
f is finite Element of Fin X
g is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
(X,Y,g,f) is finite Element of Fin Y
Fin Y is non empty cup-closed diff-closed preBoolean set
B is Relation-like Y -defined Fin Z -valued Function-like non empty V14(Y) V18(Y, Fin Z) Element of K27(K28(Y,(Fin Z)))
(Y,Z,(X,Y,g,f),B) is finite Element of Fin Z
(Z) is Relation-like K28((Fin Z),(Fin Z)) -defined Fin Z -valued Function-like non empty V14(K28((Fin Z),(Fin Z))) V18(K28((Fin Z),(Fin Z)), Fin Z) Element of K27(K28(K28((Fin Z),(Fin Z)),(Fin Z)))
K28((Fin Z),(Fin Z)) is Relation-like non empty set
K28(K28((Fin Z),(Fin Z)),(Fin Z)) is Relation-like non empty set
K27(K28(K28((Fin Z),(Fin Z)),(Fin Z))) is non empty cup-closed diff-closed preBoolean set
(Y,(Fin Z),(Z),(X,Y,g,f),B) is finite Element of Fin Z
B * g is Relation-like X -defined Fin Z -valued Function-like non empty V14(X) V18(X, Fin Z) Element of K27(K28(X,(Fin Z)))
K28(X,(Fin Z)) is Relation-like non empty set
K27(K28(X,(Fin Z))) is non empty cup-closed diff-closed preBoolean set
(X,Z,f,(B * g)) is finite Element of Fin Z
(X,(Fin Z),(Z),f,(B * g)) is finite Element of Fin Z
(Y,(Fin Z),B,(X,Y,g,f)) is finite Element of Fin (Fin Z)
Fin (Fin Z) is non empty cup-closed diff-closed preBoolean set
union (Y,(Fin Z),B,(X,Y,g,f)) is set
(X,(Fin Z),(B * g),f) is finite Element of Fin (Fin Z)
union (X,(Fin Z),(B * g),f) is set
X is non empty set
K28(X,X) is Relation-like non empty set
K28(K28(X,X),X) is Relation-like non empty set
K27(K28(K28(X,X),X)) is non empty cup-closed diff-closed preBoolean set
Y is non empty set
Fin Y is non empty cup-closed diff-closed preBoolean set
Z is set
Fin Z is non empty cup-closed diff-closed preBoolean set
K28(Y,(Fin Z)) is Relation-like non empty set
K27(K28(Y,(Fin Z))) is non empty cup-closed diff-closed preBoolean set
K28((Fin Z),X) is Relation-like non empty set
K27(K28((Fin Z),X)) is non empty cup-closed diff-closed preBoolean set
f is Relation-like K28(X,X) -defined X -valued Function-like non empty V14(K28(X,X)) V18(K28(X,X),X) Element of K27(K28(K28(X,X),X))
g is finite Element of Fin Y
B is Relation-like Y -defined Fin Z -valued Function-like non empty V14(Y) V18(Y, Fin Z) Element of K27(K28(Y,(Fin Z)))
(Y,Z,g,B) is finite Element of Fin Z
(Z) is Relation-like K28((Fin Z),(Fin Z)) -defined Fin Z -valued Function-like non empty V14(K28((Fin Z),(Fin Z))) V18(K28((Fin Z),(Fin Z)), Fin Z) Element of K27(K28(K28((Fin Z),(Fin Z)),(Fin Z)))
K28((Fin Z),(Fin Z)) is Relation-like non empty set
K28(K28((Fin Z),(Fin Z)),(Fin Z)) is Relation-like non empty set
K27(K28(K28((Fin Z),(Fin Z)),(Fin Z))) is non empty cup-closed diff-closed preBoolean set
(Y,(Fin Z),(Z),g,B) is finite Element of Fin Z
y is Relation-like Fin Z -defined X -valued Function-like non empty V14( Fin Z) V18( Fin Z,X) Element of K27(K28((Fin Z),X))
y . (Y,Z,g,B) is Element of X
y * B is Relation-like Y -defined X -valued Function-like non empty V14(Y) V18(Y,X) Element of K27(K28(Y,X))
K28(Y,X) is Relation-like non empty set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
(Y,X,f,g,(y * B)) is Element of X
i is finite Element of Fin Z
i9 is finite Element of Fin Z
(Z) . (i,i9) is finite Element of Fin Z
[i,i9] is set
{i,i9} is non empty finite V30() set
{i} is non empty finite V30() set
{{i,i9},{i}} is non empty finite V30() set
(Z) . [i,i9] is set
y . ((Z) . (i,i9)) is Element of X
(Z,i,i9) is finite Element of Fin Z
y . (Z,i,i9) is Element of X
y . i is Element of X
y . i9 is Element of X
f . ((y . i),(y . i9)) is Element of X
[(y . i),(y . i9)] is set
{(y . i),(y . i9)} is non empty finite set
{(y . i)} is non empty finite set
{{(y . i),(y . i9)},{(y . i)}} is non empty finite V30() set
f . [(y . i),(y . i9)] is set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is non empty set
K28(Y,Y) is Relation-like non empty set
K28(K28(Y,Y),Y) is Relation-like non empty set
K27(K28(K28(Y,Y),Y)) is non empty cup-closed diff-closed preBoolean set
Z is set
Fin Z is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Z)) is Relation-like non empty set
K27(K28(X,(Fin Z))) is non empty cup-closed diff-closed preBoolean set
K28((Fin Z),Y) is Relation-like non empty set
K27(K28((Fin Z),Y)) is non empty cup-closed diff-closed preBoolean set
(Z) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Z
f is Relation-like K28(Y,Y) -defined Y -valued Function-like non empty V14(K28(Y,Y)) V18(K28(Y,Y),Y) Element of K27(K28(K28(Y,Y),Y))
the_unity_wrt f is Element of Y
g is Relation-like X -defined Fin Z -valued Function-like non empty V14(X) V18(X, Fin Z) Element of K27(K28(X,(Fin Z)))
B is Relation-like Fin Z -defined Y -valued Function-like non empty V14( Fin Z) V18( Fin Z,Y) Element of K27(K28((Fin Z),Y))
B . (Z) is Element of Y
B * g is Relation-like X -defined Y -valued Function-like non empty V14(X) V18(X,Y) Element of K27(K28(X,Y))
K28(X,Y) is Relation-like non empty set
K27(K28(X,Y)) is non empty cup-closed diff-closed preBoolean set
y is finite Element of Fin X
(X,Z,y,g) is finite Element of Fin Z
(Z) is Relation-like K28((Fin Z),(Fin Z)) -defined Fin Z -valued Function-like non empty V14(K28((Fin Z),(Fin Z))) V18(K28((Fin Z),(Fin Z)), Fin Z) Element of K27(K28(K28((Fin Z),(Fin Z)),(Fin Z)))
K28((Fin Z),(Fin Z)) is Relation-like non empty set
K28(K28((Fin Z),(Fin Z)),(Fin Z)) is Relation-like non empty set
K27(K28(K28((Fin Z),(Fin Z)),(Fin Z))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Z),(Z),y,g) is finite Element of Fin Z
B . (X,Z,y,g) is Element of Y
(X,Y,f,y,(B * g)) is Element of Y
(X) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin X
((Fin Z)) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin (Fin Z)
Fin (Fin Z) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Z),g,y) is finite Element of Fin (Fin Z)
((Fin Z),Y,f,(X,(Fin Z),g,y),B) is Element of Y
X is set
Fin X is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin X)) is Relation-like set
K27(K28(X,(Fin X))) is non empty cup-closed diff-closed preBoolean set
Y is set
Z is non empty set
f is Element of Z
(Z,f) is non empty finite Element of Fin Z
Fin Z is non empty cup-closed diff-closed preBoolean set
{Y} is non empty finite set
Y is Relation-like X -defined Fin X -valued Function-like V14(X) V18(X, Fin X) Element of K27(K28(X,(Fin X)))
Z is Relation-like X -defined Fin X -valued Function-like V14(X) V18(X, Fin X) Element of K27(K28(X,(Fin X)))
f is set
Y . f is set
{f} is non empty finite set
Z . f is set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin X)) is Relation-like non empty set
K27(K28(X,(Fin X))) is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like X -defined Fin X -valued Function-like non empty V14(X) V18(X, Fin X) Element of K27(K28(X,(Fin X)))
Y is Relation-like X -defined Fin X -valued Function-like non empty V14(X) V18(X, Fin X) Element of K27(K28(X,(Fin X)))
Z is Element of X
Y . Z is finite Element of Fin X
{Z} is non empty finite set
Z is set
Y . Z is set
{Z} is non empty finite set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like X -defined Fin X -valued Function-like non empty V14(X) V18(X, Fin X) Element of K27(K28(X,(Fin X)))
K28(X,(Fin X)) is Relation-like non empty set
K27(K28(X,(Fin X))) is non empty cup-closed diff-closed preBoolean set
Y is set
Z is Element of X
(X) . Z is finite Element of Fin X
{Z} is non empty finite set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like X -defined Fin X -valued Function-like non empty V14(X) V18(X, Fin X) Element of K27(K28(X,(Fin X)))
K28(X,(Fin X)) is Relation-like non empty set
K27(K28(X,(Fin X))) is non empty cup-closed diff-closed preBoolean set
Y is Element of X
f is Element of X
(X) . f is finite Element of Fin X
Z is Element of X
Y is set
X is non empty set
K28(Y,X) is Relation-like set
K27(K28(Y,X)) is non empty cup-closed diff-closed preBoolean set
f is Relation-like Y -defined X -valued Function-like V14(Y) V18(Y,X) Element of K27(K28(Y,X))
Z is set
f .: Z is Element of K27(X)
K27(X) is non empty cup-closed diff-closed preBoolean set
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
f is finite Element of Fin X
(X,Y,f,Z) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),f,Z) is finite Element of Fin Y
g is set
(X,(Fin Y),Z,f) is finite Element of Fin (Fin Y)
Fin (Fin Y) is non empty cup-closed diff-closed preBoolean set
union (X,(Fin Y),Z,f) is set
B is set
K27((Fin Y)) is non empty cup-closed diff-closed preBoolean set
y is finite Element of Fin Y
i is Element of X
Z . i is finite Element of Fin Y
i9 is Element of X
Z . i9 is finite Element of Fin Y
B is Element of X
Z . B is finite Element of Fin Y
B is Element of X
Z . B is finite Element of Fin Y
y is Element of X
Z . y is finite Element of Fin Y
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
(X) is Relation-like X -defined Fin X -valued Function-like non empty V14(X) V18(X, Fin X) Element of K27(K28(X,(Fin X)))
K28(X,(Fin X)) is Relation-like non empty set
K27(K28(X,(Fin X))) is non empty cup-closed diff-closed preBoolean set
Y is finite Element of Fin X
(X,X,Y,(X)) is finite Element of Fin X
(X) is Relation-like K28((Fin X),(Fin X)) -defined Fin X -valued Function-like non empty V14(K28((Fin X),(Fin X))) V18(K28((Fin X),(Fin X)), Fin X) Element of K27(K28(K28((Fin X),(Fin X)),(Fin X)))
K28((Fin X),(Fin X)) is Relation-like non empty set
K28(K28((Fin X),(Fin X)),(Fin X)) is Relation-like non empty set
K27(K28(K28((Fin X),(Fin X)),(Fin X))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin X),(X),Y,(X)) is finite Element of Fin X
Z is set
f is Element of X
(X) . f is finite Element of Fin X
f is Element of X
(X) . f is finite Element of Fin X
X is non empty set
Fin X is non empty cup-closed diff-closed preBoolean set
Y is set
Fin Y is non empty cup-closed diff-closed preBoolean set
K28(X,(Fin Y)) is Relation-like non empty set
K27(K28(X,(Fin Y))) is non empty cup-closed diff-closed preBoolean set
Z is set
Fin Z is non empty cup-closed diff-closed preBoolean set
K28((Fin Y),(Fin Z)) is Relation-like non empty set
K27(K28((Fin Y),(Fin Z))) is non empty cup-closed diff-closed preBoolean set
(Y) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Y
(Z) is Relation-like non-empty empty-yielding empty finite finite-yielding V30() Element of Fin Z
f is Relation-like X -defined Fin Y -valued Function-like non empty V14(X) V18(X, Fin Y) Element of K27(K28(X,(Fin Y)))
g is Relation-like Fin Y -defined Fin Z -valued Function-like non empty V14( Fin Y) V18( Fin Y, Fin Z) Element of K27(K28((Fin Y),(Fin Z)))
g . (Y) is finite Element of Fin Z
g * f is Relation-like X -defined Fin Z -valued Function-like non empty V14(X) V18(X, Fin Z) Element of K27(K28(X,(Fin Z)))
K28(X,(Fin Z)) is Relation-like non empty set
K27(K28(X,(Fin Z))) is non empty cup-closed diff-closed preBoolean set
(Z) is Relation-like K28((Fin Z),(Fin Z)) -defined Fin Z -valued Function-like non empty V14(K28((Fin Z),(Fin Z))) V18(K28((Fin Z),(Fin Z)), Fin Z) Element of K27(K28(K28((Fin Z),(Fin Z)),(Fin Z)))
K28((Fin Z),(Fin Z)) is Relation-like non empty set
K28(K28((Fin Z),(Fin Z)),(Fin Z)) is Relation-like non empty set
K27(K28(K28((Fin Z),(Fin Z)),(Fin Z))) is non empty cup-closed diff-closed preBoolean set
the_unity_wrt (Z) is finite Element of Fin Z
B is finite Element of Fin Y
y is finite Element of Fin Y
(Y,B,y) is finite Element of Fin Y
g . (Y,B,y) is finite Element of Fin Z
g . B is finite Element of Fin Z
g . y is finite Element of Fin Z
(Z,(g . B),(g . y)) is finite Element of Fin Z
(Z) . ((g . B),(g . y)) is finite Element of Fin Z
[(g . B),(g . y)] is set
{(g . B),(g . y)} is non empty finite V30() set
{(g . B)} is non empty finite V30() set
{{(g . B),(g . y)},{(g . B)}} is non empty finite V30() set
(Z) . [(g . B),(g . y)] is set
B is finite Element of Fin X
(X,Y,B,f) is finite Element of Fin Y
(Y) is Relation-like K28((Fin Y),(Fin Y)) -defined Fin Y -valued Function-like non empty V14(K28((Fin Y),(Fin Y))) V18(K28((Fin Y),(Fin Y)), Fin Y) Element of K27(K28(K28((Fin Y),(Fin Y)),(Fin Y)))
K28((Fin Y),(Fin Y)) is Relation-like non empty set
K28(K28((Fin Y),(Fin Y)),(Fin Y)) is Relation-like non empty set
K27(K28(K28((Fin Y),(Fin Y)),(Fin Y))) is non empty cup-closed diff-closed preBoolean set
(X,(Fin Y),(Y),B,f) is finite Element of Fin Y
g . (X,Y,B,f) is finite Element of Fin Z
(X,Z,B,(g * f)) is finite Element of Fin Z
(X,(Fin Z),(Z),B,(g * f)) is finite Element of Fin Z