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

Fin F

K28(F

K27(K28(F

F

K27(F

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

(F

Fin F

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

{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

Fin F

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

B is finite Element of Fin F

Y is finite Element of Fin F

F

(F

Fin F

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

c

(X,c

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