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