:: BINOP_1 semantic presentation

{} is Function-like functional empty set

X is Relation-like Function-like set

Y is set

Z is set

[Y,Z] is set

X . [Y,Z] is set

X is non empty set

Y is non empty set

[:X,Y:] is non empty set

Z is set

[:[:X,Y:],Z:] is set

bool [:[:X,Y:],Z:] is non empty set

f1 is Relation-like [:X,Y:] -defined Z -valued Function-like V18([:X,Y:],Z) Element of bool [:[:X,Y:],Z:]

f2 is Element of X

f is Element of Y

(f1,f2,f) is set

[f2,f] is set

f1 . [f2,f] is set

x is Element of [:X,Y:]

f1 . x is Element of Z

X is set

Y is set

[:X,Y:] is set

Z is set

[:[:X,Y:],Z:] is set

bool [:[:X,Y:],Z:] is non empty set

f1 is Relation-like [:X,Y:] -defined Z -valued Function-like V18([:X,Y:],Z) Element of bool [:[:X,Y:],Z:]

f2 is Relation-like [:X,Y:] -defined Z -valued Function-like V18([:X,Y:],Z) Element of bool [:[:X,Y:],Z:]

f is set

f1 . f is set

f2 . f is set

x is set

y is set

[x,y] is set

(f1,x,y) is set

f1 . [x,y] is set

(f2,x,y) is set

f2 . [x,y] is set

X is set

Y is set

[:X,Y:] is set

Z is set

[:[:X,Y:],Z:] is set

bool [:[:X,Y:],Z:] is non empty set

f1 is Relation-like [:X,Y:] -defined Z -valued Function-like V18([:X,Y:],Z) Element of bool [:[:X,Y:],Z:]

f2 is Relation-like [:X,Y:] -defined Z -valued Function-like V18([:X,Y:],Z) Element of bool [:[:X,Y:],Z:]

f is set

x is set

(f1,f,x) is set

[f,x] is set

f1 . [f,x] is set

(f2,f,x) is set

f2 . [f,x] is set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

f1 is Element of X

(Y,Z,f1) is set

[Z,f1] is set

Y . [Z,f1] is set

f2 is non empty set

[:f2,f2:] is non empty set

[:[:f2,f2:],f2:] is non empty set

bool [:[:f2,f2:],f2:] is non empty set

f is Relation-like [:f2,f2:] -defined f2 -valued Function-like V18([:f2,f2:],f2) Element of bool [:[:f2,f2:],f2:]

x is Element of [:f2,f2:]

f . x is Element of f2

dom Y is Relation-like X -defined X -valued Element of bool [:X,X:]

bool [:X,X:] is non empty set

F

F

F

[:F

[:[:F

bool [:[:F

X is set

Y is set

Z is set

[Y,Z] is set

f1 is set

f2 is set

f is set

[f2,f] is set

X is Relation-like [:F

Y is set

Z is set

(X,Y,Z) is set

[Y,Z] is set

X . [Y,Z] is set

F

F

F

[:F

[:[:F

bool [:[:F

X is set

Y is set

F

F

F

F

[:F

[:[:F

bool [:[:F

X is Element of [:F

Y is set

Z is set

[Y,Z] is set

f2 is Element of F

f1 is Element of F

f is Element of F

x is Element of F

y is Element of F

[x,y] is set

X is Relation-like [:F

Y is Element of F

Z is Element of F

(F

[Y,Z] is set

X . [Y,Z] is set

f1 is Element of [:F

X . f1 is Element of F

F

F

F

[:F

[:[:F

bool [:[:F

X is Element of F

Y is Element of F

F

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

[:{},{}:] is set

[:[:{},{}:],{}:] is set

bool [:[:{},{}:],{}:] is non empty set

X is Relation-like [:{},{}:] -defined {} -valued Function-like one-to-one constant functional empty V18([:{},{}:], {} ) Element of bool [:[:{},{}:],{}:]

dom X is Relation-like {} -defined {} -valued Function-like one-to-one constant functional empty Element of bool [:{},{}:]

bool [:{},{}:] is non empty set

rng X is Function-like functional empty trivial non proper Element of bool {}

bool {} is non empty set

[:(dom X),(rng X):] is set

Y is Relation-like Function-like Element of {}

Z is Relation-like Function-like Element of {}

f1 is Relation-like Function-like Element of {}

({},X,Z,f1) is Relation-like Function-like Element of {}

[Z,f1] is set

X . [Z,f1] is Relation-like Function-like set

({},X,Y,({},X,Z,f1)) is Relation-like Function-like Element of {}

[Y,({},X,Z,f1)] is set

X . [Y,({},X,Z,f1)] is Relation-like Function-like set

({},X,Y,Z) is Relation-like Function-like Element of {}

[Y,Z] is set

X . [Y,Z] is Relation-like Function-like set

({},X,({},X,Y,Z),f1) is Relation-like Function-like Element of {}

[({},X,Y,Z),f1] is set

X . [({},X,Y,Z),f1] is Relation-like Function-like set

Y is Relation-like Function-like Element of {}

Z is Relation-like Function-like Element of {}

({},X,Y,Z) is Relation-like Function-like Element of {}

[Y,Z] is set

X . [Y,Z] is Relation-like Function-like set

({},X,Z,Y) is Relation-like Function-like Element of {}

[Z,Y] is set

X . [Z,Y] is Relation-like Function-like set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

f1 is Element of X

(X,Y,Z,f1) is Element of X

[Z,f1] is set

Y . [Z,f1] is set

f2 is Element of X

(X,Y,f2,Z) is Element of X

[f2,Z] is set

Y . [f2,Z] is set

f1 is Element of X

(X,Y,Z,f1) is Element of X

[Z,f1] is set

Y . [Z,f1] is set

f2 is Element of X

(X,Y,f2,Z) is Element of X

[f2,Z] is set

Y . [f2,Z] is set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

f1 is Element of X

(X,Y,Z,f1) is Element of X

[Z,f1] is set

Y . [Z,f1] is set

f1 is Element of X

(X,Y,Z,f1) is Element of X

[Z,f1] is set

Y . [Z,f1] is set

(X,Y,f1,Z) is Element of X

[f1,Z] is set

Y . [f1,Z] is set

f1 is Element of X

(X,Y,Z,f1) is Element of X

[Z,f1] is set

Y . [Z,f1] is set

f2 is Element of X

(X,Y,Z,f2) is Element of X

[Z,f2] is set

Y . [Z,f2] is set

f is Element of X

(X,Y,f,Z) is Element of X

[f,Z] is set

Y . [f,Z] is set

x is Element of X

(X,Y,Z,x) is Element of X

[Z,x] is set

Y . [Z,x] is set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

f1 is Element of X

(X,Y,f1,Z) is Element of X

[f1,Z] is set

Y . [f1,Z] is set

f1 is Element of X

(X,Y,Z,f1) is Element of X

[Z,f1] is set

Y . [Z,f1] is set

(X,Y,f1,Z) is Element of X

[f1,Z] is set

Y . [f1,Z] is set

f1 is Element of X

(X,Y,f1,Z) is Element of X

[f1,Z] is set

Y . [f1,Z] is set

f2 is Element of X

(X,Y,Z,f2) is Element of X

[Z,f2] is set

Y . [Z,f2] is set

f is Element of X

(X,Y,f,Z) is Element of X

[f,Z] is set

Y . [f,Z] is set

x is Element of X

(X,Y,x,Z) is Element of X

[x,Z] is set

Y . [x,Z] is set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

f1 is Element of X

(X,Y,Z,f1) is Element of X

[Z,f1] is set

Y . [Z,f1] is set

f1 is Element of X

(X,Y,Z,f1) is Element of X

[Z,f1] is set

Y . [Z,f1] is set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

f1 is Element of X

(X,Y,f1,Z) is Element of X

[f1,Z] is set

Y . [f1,Z] is set

f1 is Element of X

(X,Y,f1,Z) is Element of X

[f1,Z] is set

Y . [f1,Z] is set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

f1 is Element of X

(X,Y,Z,f1) is Element of X

[Z,f1] is set

Y . [Z,f1] is set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

f1 is Element of X

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

Z is Element of X

f1 is Element of X

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

f1 is Element of X

f2 is Element of X

f is Element of X

(X,Z,f2,f) is Element of X

[f2,f] is set

Z . [f2,f] is set

(X,Y,f1,(X,Z,f2,f)) is Element of X

[f1,(X,Z,f2,f)] is set

Y . [f1,(X,Z,f2,f)] is set

(X,Y,f1,f2) is Element of X

[f1,f2] is set

Y . [f1,f2] is set

(X,Y,f1,f) is Element of X

[f1,f] is set

Y . [f1,f] is set

(X,Z,(X,Y,f1,f2),(X,Y,f1,f)) is Element of X

[(X,Y,f1,f2),(X,Y,f1,f)] is set

Z . [(X,Y,f1,f2),(X,Y,f1,f)] is set

x is Element of X

y is Element of X

(X,Z,x,y) is Element of X

[x,y] is set

Z . [x,y] is set

y2 is Element of X

(X,Y,(X,Z,x,y),y2) is Element of X

[(X,Z,x,y),y2] is set

Y . [(X,Z,x,y),y2] is set

(X,Y,x,y2) is Element of X

[x,y2] is set

Y . [x,y2] is set

(X,Y,y,y2) is Element of X

[y,y2] is set

Y . [y,y2] is set

(X,Z,(X,Y,x,y2),(X,Y,y,y2)) is Element of X

[(X,Y,x,y2),(X,Y,y,y2)] is set

Z . [(X,Y,x,y2),(X,Y,y,y2)] is set

f1 is Element of X

f2 is Element of X

f is Element of X

(X,Z,f2,f) is Element of X

[f2,f] is set

Z . [f2,f] is set

(X,Y,f1,(X,Z,f2,f)) is Element of X

[f1,(X,Z,f2,f)] is set

Y . [f1,(X,Z,f2,f)] is set

(X,Y,f1,f2) is Element of X

[f1,f2] is set

Y . [f1,f2] is set

(X,Y,f1,f) is Element of X

[f1,f] is set

Y . [f1,f] is set

(X,Z,(X,Y,f1,f2),(X,Y,f1,f)) is Element of X

[(X,Y,f1,f2),(X,Y,f1,f)] is set

Z . [(X,Y,f1,f2),(X,Y,f1,f)] is set

x is Element of X

y is Element of X

(X,Z,x,y) is Element of X

[x,y] is set

Z . [x,y] is set

y2 is Element of X

(X,Y,(X,Z,x,y),y2) is Element of X

[(X,Z,x,y),y2] is set

Y . [(X,Z,x,y),y2] is set

(X,Y,x,y2) is Element of X

[x,y2] is set

Y . [x,y2] is set

(X,Y,y,y2) is Element of X

[y,y2] is set

Y . [y,y2] is set

(X,Z,(X,Y,x,y2),(X,Y,y,y2)) is Element of X

[(X,Y,x,y2),(X,Y,y,y2)] is set

Z . [(X,Y,x,y2),(X,Y,y,y2)] is set

X is non empty set

[:X,X:] is non empty set

[:[:X,X:],X:] is non empty set

bool [:[:X,X:],X:] is non empty set

Z is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

f1 is Element of X

f2 is Element of X

f is Element of X

(X,Y,f2,f) is Element of X

[f2,f] is set

Y . [f2,f] is set

(X,Z,f1,(X,Y,f2,f)) is Element of X

[f1,(X,Y,f2,f)] is set

Z . [f1,(X,Y,f2,f)] is set

(X,Z,f1,f2) is Element of X

[f1,f2] is set

Z . [f1,f2] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Y,(X,Z,f1,f2),(X,Z,f1,f)) is Element of X

[(X,Z,f1,f2),(X,Z,f1,f)] is set

Y . [(X,Z,f1,f2),(X,Z,f1,f)] is set

f1 is Element of X

f2 is Element of X

f is Element of X

(X,Y,f2,f) is Element of X

[f2,f] is set

Y . [f2,f] is set

(X,Z,f1,(X,Y,f2,f)) is Element of X

[f1,(X,Y,f2,f)] is set

Z . [f1,(X,Y,f2,f)] is set

(X,Z,f1,f2) is Element of X

[f1,f2] is set

Z . [f1,f2] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Y,(X,Z,f1,f2),(X,Z,f1,f)) is Element of X

[(X,Z,f1,f2),(X,Z,f1,f)] is set

Y . [(X,Z,f1,f2),(X,Z,f1,f)] is set

(X,Y,f1,f2) is Element of X

Y . [f1,f2] is set

(X,Z,(X,Y,f1,f2),f) is Element of X

[(X,Y,f1,f2),f] is set

Z . [(X,Y,f1,f2),f] is set

(X,Z,f2,f) is Element of X

Z . [f2,f] is set

(X,Y,(X,Z,f1,f),(X,Z,f2,f)) is Element of X

[(X,Z,f1,f),(X,Z,f2,f)] is set

Y . [(X,Z,f1,f),(X,Z,f2,f)] is set

(X,Z,f,(X,Y,f1,f2)) is Element of X

[f,(X,Y,f1,f2)] is set

Z . [f,(X,Y,f1,f2)] is set

(X,Z,f,f1) is Element of X

[f,f1] is set

Z . [f,f1] is set

(X,Z,f,f2) is Element of X

[f,f2] is set

Z . [f,f2] is set

(X,Y,(X,Z,f,f1),(X,Z,f,f2)) is Element of X

[(X,Z,f,f1),(X,Z,f,f2)] is set

Y . [(X,Z,f,f1),(X,Z,f,f2)] is set

(X,Y,(X,Z,f1,f),(X,Z,f,f2)) is Element of X

[(X,Z,f1,f),(X,Z,f,f2)] is set

Y . [(X,Z,f1,f),(X,Z,f,f2)] is set

f1 is Element of X

f2 is Element of X

f is Element of X

(X,Y,f2,f) is Element of X

[f2,f] is set

Y . [f2,f] is set

(X,Z,f1,(X,Y,f2,f)) is Element of X

[f1,(X,Y,f2,f)] is set

Z . [f1,(X,Y,f2,f)] is set

(X,Z,f1,f2) is Element of X

[f1,f2] is set

Z . [f1,f2] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Y,(X,Z,f1,f2),(X,Z,f1,f)) is Element of X

[(X,Z,f1,f2),(X,Z,f1,f)] is set

Y . [(X,Z,f1,f2),(X,Z,f1,f)] is set

x is Element of X

y is Element of X

y2 is Element of X

(X,Y,y,y2) is Element of X

[y,y2] is set

Y . [y,y2] is set

(X,Z,x,(X,Y,y,y2)) is Element of X

[x,(X,Y,y,y2)] is set

Z . [x,(X,Y,y,y2)] is set

(X,Z,x,y) is Element of X

[x,y] is set

Z . [x,y] is set

(X,Z,x,y2) is Element of X

[x,y2] is set

Z . [x,y2] is set

(X,Y,(X,Z,x,y),(X,Z,x,y2)) is Element of X

[(X,Z,x,y),(X,Z,x,y2)] is set

Y . [(X,Z,x,y),(X,Z,x,y2)] is set

c

c

(X,Y,c

[c

Y . [c

c

(X,Z,(X,Y,c

[(X,Y,c

Z . [(X,Y,c

(X,Z,c

[c

Z . [c

(X,Z,c

[c

Z . [c

(X,Y,(X,Z,c

[(X,Z,c

Y . [(X,Z,c

c

c

c

(X,Y,c

[c

Y . [c

(X,Z,c

[c

Z . [c

(X,Z,c

[c

Z . [c

(X,Z,c

[c

Z . [c

(X,Y,(X,Z,c

[(X,Z,c

Y . [(X,Z,c

X is non empty set

[:X,X:] is non empty set

[:[:X,X:],X:] is non empty set

bool [:[:X,X:],X:] is non empty set

Z is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

f1 is Element of X

f2 is Element of X

(X,Y,f1,f2) is Element of X

[f1,f2] is set

Y . [f1,f2] is set

f is Element of X

(X,Z,(X,Y,f1,f2),f) is Element of X

[(X,Y,f1,f2),f] is set

Z . [(X,Y,f1,f2),f] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Z,f2,f) is Element of X

[f2,f] is set

Z . [f2,f] is set

(X,Y,(X,Z,f1,f),(X,Z,f2,f)) is Element of X

[(X,Z,f1,f),(X,Z,f2,f)] is set

Y . [(X,Z,f1,f),(X,Z,f2,f)] is set

f1 is Element of X

f2 is Element of X

f is Element of X

(X,Y,f2,f) is Element of X

[f2,f] is set

Y . [f2,f] is set

(X,Z,f1,(X,Y,f2,f)) is Element of X

[f1,(X,Y,f2,f)] is set

Z . [f1,(X,Y,f2,f)] is set

(X,Z,f1,f2) is Element of X

[f1,f2] is set

Z . [f1,f2] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Y,(X,Z,f1,f2),(X,Z,f1,f)) is Element of X

[(X,Z,f1,f2),(X,Z,f1,f)] is set

Y . [(X,Z,f1,f2),(X,Z,f1,f)] is set

(X,Y,f1,f2) is Element of X

Y . [f1,f2] is set

(X,Z,(X,Y,f1,f2),f) is Element of X

[(X,Y,f1,f2),f] is set

Z . [(X,Y,f1,f2),f] is set

(X,Z,f2,f) is Element of X

Z . [f2,f] is set

(X,Y,(X,Z,f1,f),(X,Z,f2,f)) is Element of X

[(X,Z,f1,f),(X,Z,f2,f)] is set

Y . [(X,Z,f1,f),(X,Z,f2,f)] is set

(X,Z,(X,Y,f2,f),f1) is Element of X

[(X,Y,f2,f),f1] is set

Z . [(X,Y,f2,f),f1] is set

(X,Z,f2,f1) is Element of X

[f2,f1] is set

Z . [f2,f1] is set

(X,Z,f,f1) is Element of X

[f,f1] is set

Z . [f,f1] is set

(X,Y,(X,Z,f2,f1),(X,Z,f,f1)) is Element of X

[(X,Z,f2,f1),(X,Z,f,f1)] is set

Y . [(X,Z,f2,f1),(X,Z,f,f1)] is set

(X,Y,(X,Z,f1,f2),(X,Z,f,f1)) is Element of X

[(X,Z,f1,f2),(X,Z,f,f1)] is set

Y . [(X,Z,f1,f2),(X,Z,f,f1)] is set

f1 is Element of X

f2 is Element of X

(X,Y,f1,f2) is Element of X

[f1,f2] is set

Y . [f1,f2] is set

f is Element of X

(X,Z,(X,Y,f1,f2),f) is Element of X

[(X,Y,f1,f2),f] is set

Z . [(X,Y,f1,f2),f] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Z,f2,f) is Element of X

[f2,f] is set

Z . [f2,f] is set

(X,Y,(X,Z,f1,f),(X,Z,f2,f)) is Element of X

[(X,Z,f1,f),(X,Z,f2,f)] is set

Y . [(X,Z,f1,f),(X,Z,f2,f)] is set

x is Element of X

y is Element of X

y2 is Element of X

(X,Y,y,y2) is Element of X

[y,y2] is set

Y . [y,y2] is set

(X,Z,x,(X,Y,y,y2)) is Element of X

[x,(X,Y,y,y2)] is set

Z . [x,(X,Y,y,y2)] is set

(X,Z,x,y) is Element of X

[x,y] is set

Z . [x,y] is set

(X,Z,x,y2) is Element of X

[x,y2] is set

Z . [x,y2] is set

(X,Y,(X,Z,x,y),(X,Z,x,y2)) is Element of X

[(X,Z,x,y),(X,Z,x,y2)] is set

Y . [(X,Z,x,y),(X,Z,x,y2)] is set

c

c

(X,Y,c

[c

Y . [c

c

(X,Z,(X,Y,c

[(X,Y,c

Z . [(X,Y,c

(X,Z,c

[c

Z . [c

(X,Z,c

[c

Z . [c

(X,Y,(X,Z,c

[(X,Z,c

Y . [(X,Z,c

c

c

(X,Y,c

[c

Y . [c

c

(X,Z,(X,Y,c

[(X,Y,c

Z . [(X,Y,c

(X,Z,c

[c

Z . [c

(X,Z,c

[c

Z . [c

(X,Y,(X,Z,c

[(X,Z,c

Y . [(X,Z,c

X is non empty set

[:X,X:] is non empty set

[:[:X,X:],X:] is non empty set

bool [:[:X,X:],X:] is non empty set

Z is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

f1 is Element of X

f2 is Element of X

f is Element of X

(X,Y,f2,f) is Element of X

[f2,f] is set

Y . [f2,f] is set

(X,Z,f1,(X,Y,f2,f)) is Element of X

[f1,(X,Y,f2,f)] is set

Z . [f1,(X,Y,f2,f)] is set

(X,Z,f1,f2) is Element of X

[f1,f2] is set

Z . [f1,f2] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Y,(X,Z,f1,f2),(X,Z,f1,f)) is Element of X

[(X,Z,f1,f2),(X,Z,f1,f)] is set

Y . [(X,Z,f1,f2),(X,Z,f1,f)] is set

f1 is Element of X

f2 is Element of X

f is Element of X

(X,Y,f2,f) is Element of X

[f2,f] is set

Y . [f2,f] is set

(X,Z,f1,(X,Y,f2,f)) is Element of X

[f1,(X,Y,f2,f)] is set

Z . [f1,(X,Y,f2,f)] is set

(X,Z,f1,f2) is Element of X

[f1,f2] is set

Z . [f1,f2] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Y,(X,Z,f1,f2),(X,Z,f1,f)) is Element of X

[(X,Z,f1,f2),(X,Z,f1,f)] is set

Y . [(X,Z,f1,f2),(X,Z,f1,f)] is set

X is non empty set

[:X,X:] is non empty set

[:[:X,X:],X:] is non empty set

bool [:[:X,X:],X:] is non empty set

Z is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

f1 is Element of X

f2 is Element of X

(X,Y,f1,f2) is Element of X

[f1,f2] is set

Y . [f1,f2] is set

f is Element of X

(X,Z,(X,Y,f1,f2),f) is Element of X

[(X,Y,f1,f2),f] is set

Z . [(X,Y,f1,f2),f] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Z,f2,f) is Element of X

[f2,f] is set

Z . [f2,f] is set

(X,Y,(X,Z,f1,f),(X,Z,f2,f)) is Element of X

[(X,Z,f1,f),(X,Z,f2,f)] is set

Y . [(X,Z,f1,f),(X,Z,f2,f)] is set

f1 is Element of X

f2 is Element of X

(X,Y,f1,f2) is Element of X

[f1,f2] is set

Y . [f1,f2] is set

f is Element of X

(X,Z,(X,Y,f1,f2),f) is Element of X

[(X,Y,f1,f2),f] is set

Z . [(X,Y,f1,f2),f] is set

(X,Z,f1,f) is Element of X

[f1,f] is set

Z . [f1,f] is set

(X,Z,f2,f) is Element of X

[f2,f] is set

Z . [f2,f] is set

(X,Y,(X,Z,f1,f),(X,Z,f2,f)) is Element of X

[(X,Z,f1,f),(X,Z,f2,f)] is set

Y . [(X,Z,f1,f),(X,Z,f2,f)] is set

X is non empty set

[:X,X:] is non empty set

[:[:X,X:],X:] is non empty set

bool [:[:X,X:],X:] is non empty set

Z is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

X is set

[:X,X:] is set

bool [:X,X:] is non empty set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

X is non empty set

[:X,X:] is non empty set

[:[:X,X:],X:] is non empty set

bool [:[:X,X:],X:] is non empty set

Y is Element of X

Z is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

f1 is Element of X

(X,Z,Y,f1) is Element of X

[Y,f1] is set

Z . [Y,f1] is set

f1 is Element of X

(X,Z,f1,Y) is Element of X

[f1,Y] is set

Z . [f1,Y] is set

X is non empty set

[:X,X:] is non empty set

[:[:X,X:],X:] is non empty set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

f1 is Element of X

f2 is Element of X

f is Element of X

(X,Z,f2,f) is Element of X

[f2,f] is set

Z . [f2,f] is set

(X,Y,f1,(X,Z,f2,f)) is Element of X

[f1,(X,Z,f2,f)] is set

Y . [f1,(X,Z,f2,f)] is set

(X,Y,f1,f2) is Element of X

[f1,f2] is set

Y . [f1,f2] is set

(X,Y,f1,f) is Element of X

[f1,f] is set

Y . [f1,f] is set

(X,Z,(X,Y,f1,f2),(X,Y,f1,f)) is Element of X

[(X,Y,f1,f2),(X,Y,f1,f)] is set

Z . [(X,Y,f1,f2),(X,Y,f1,f)] is set

f1 is Element of X

f2 is Element of X

(X,Z,f1,f2) is Element of X

[f1,f2] is set

Z . [f1,f2] is set

f is Element of X

(X,Y,(X,Z,f1,f2),f) is Element of X

[(X,Z,f1,f2),f] is set

Y . [(X,Z,f1,f2),f] is set

(X,Y,f1,f) is Element of X

[f1,f] is set

Y . [f1,f] is set

(X,Y,f2,f) is Element of X

[f2,f] is set

Y . [f2,f] is set

(X,Z,(X,Y,f1,f),(X,Y,f2,f)) is Element of X

[(X,Y,f1,f),(X,Y,f2,f)] is set

Z . [(X,Y,f1,f),(X,Y,f2,f)] is set

X is non empty set

[:X,X:] is non empty set

bool [:X,X:] is non empty set

[:[:X,X:],X:] is non empty set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like X -defined X -valued Function-like V18(X,X) Element of bool [:X,X:]

Z is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

f1 is Element of X

f2 is Element of X

(X,Z,f1,f2) is Element of X

[f1,f2] is set

Z . [f1,f2] is set

Y . (X,Z,f1,f2) is Element of X

Y . f1 is Element of X

Y . f2 is Element of X

(X,Z,(Y . f1),(Y . f2)) is Element of X

[(Y . f1),(Y . f2)] is set

Z . [(Y . f1),(Y . f2)] is set

X is set

Y is set

[:X,Y:] is set

Z is set

[:[:X,Y:],Z:] is set

bool [:[:X,Y:],Z:] is non empty set

f1 is set

f2 is set

f is Relation-like [:X,Y:] -defined Z -valued Function-like V18([:X,Y:],Z) Element of bool [:[:X,Y:],Z:]

(f,f1,f2) is set

[f1,f2] is set

f . [f1,f2] is set

Z is set

f1 is set

[:Z,f1:] is set

f2 is set

[:[:Z,f1:],f2:] is set

bool [:[:Z,f1:],f2:] is non empty set

X is set

Y is set

f is Relation-like [:Z,f1:] -defined f2 -valued Function-like V18([:Z,f1:],f2) Element of bool [:[:Z,f1:],f2:]

(f,X,Y) is set

[X,Y] is set

f . [X,Y] is set

x is Relation-like Function-like set

f * x is Relation-like Function-like set

((f * x),X,Y) is set

(f * x) . [X,Y] is set

x . (f,X,Y) is set

X is set

Y is set

[:X,Y:] is set

Z is Relation-like Function-like set

dom Z is set

f1 is set

f2 is set

f is set

x is set

[f1,f] is set

[f2,x] is set

(Z,f1,f) is set

Z . [f1,f] is set

(Z,f2,x) is set

Z . [f2,x] is set

f1 is set

Z . f1 is set

f2 is set

Z . f2 is set

f is set

x is set

[f,x] is set

y is set

y2 is set

[y,y2] is set

(Z,f,x) is set

Z . [f,x] is set

(Z,y,y2) is set

Z . [y,y2] is set

X is set

Y is set

[:X,Y:] is set

Z is set

[:[:X,Y:],Z:] is set

bool [:[:X,Y:],Z:] is non empty set

f1 is Relation-like [:X,Y:] -defined Z -valued Function-like Element of bool [:[:X,Y:],Z:]

dom f1 is Relation-like X -defined Y -valued Element of bool [:X,Y:]

bool [:X,Y:] is non empty set

f2 is Relation-like [:X,Y:] -defined Z -valued Function-like Element of bool [:[:X,Y:],Z:]

dom f2 is Relation-like X -defined Y -valued Element of bool [:X,Y:]

f is set

f1 . f is set

f2 . f is set

x is set

y is set

[x,y] is set

(f1,x,y) is set

f1 . [x,y] is set

(f2,x,y) is set

f2 . [x,y] is set

F

F

F

[:F

[:[:F

bool [:[:F

X is set

Y is set

Z is set

f1 is set

[Z,f1] is set

X is set

Y is set

Z is set

f1 is set

f2 is set

[f1,f2] is set

X is Relation-like [:F

dom X is Relation-like F

bool [:F

Y is set

Z is set

[Y,Z] is set

f1 is set

f1 is set

f is set

x is set

[f,x] is set

f2 is set

f2 is set

Y is set

Z is set

[Y,Z] is set

(X,Y,Z) is set

X . [Y,Z] is set

F

F

F

[:F

[:[:F

bool [:[:F

X is set

Y is set

Z is set

F

f1 is set

X is set

Y is set

Z is set

F

X is Relation-like [:F

dom X is Relation-like F

bool [:F

Y is set

Z is set

[Y,Z] is set

F

f1 is set

F

f1 is set

Y is set

Z is set

[Y,Z] is set

(X,Y,Z) is set

X . [Y,Z] is set

F

F

F

F

[:F

[:[:F

bool [:[:F

X is set

Y is set

F

X is Relation-like [:F

dom X is Relation-like F

bool [:F

Y is set

Z is set

[Y,Z] is set

f1 is set

f2 is set

[f1,f2] is set

f is set

x is set

[f,x] is set

(X,f,x) is set

X . [f,x] is set

F

F

F

F

[:F

[:[:F

bool [:[:F

X is set

Y is set

F

X is Relation-like [:F

dom X is Relation-like F

bool [:F

Y is Element of F

Z is Element of F

[Y,Z] is set

f1 is Element of F

f2 is Element of F

[f1,f2] is set

f is Element of F

x is Element of F

[f,x] is set

(X,f,x) is set

X . [f,x] is set

F

X is set

[:X,X:] is set

[:[:X,X:],X:] is set

bool [:[:X,X:],X:] is non empty set

Y is Relation-like [:X,X:] -defined X -valued Function-like V18([:X,X:],X) Element of bool [:[:X,X:],X:]

Z is Element of X

f1 is Element of X

(Y,Z,f1) is set

[Z,f1] is set

Y . [Z,f1] is set

dom Y is Relation-like X -defined X -valued Element of bool [:X,X:]

bool [:X,X:] is non empty set

(X,Y,Z,f1) is Element of X

f2 is non empty set

[:f2,f2:] is non empty set

[:[:f2,f2:],f2:] is non empty set

bool [:[:f2,f2:],f2:] is non empty set

f is Relation-like [:f2,f2:] -defined f2 -valued Function-like V18([:f2,f2:],f2) Element of bool [:[:f2,f2:],f2:]

x is Element of f2

y is Element of f2

(f2,f,x,y) is Element of f2

[x,y] is set

f . [x,y] is set

X is set

Y is set

[:X,Y:] is set

Z is set

[:[:X,Y:],Z:] is set

bool [:[:X,Y:],Z:] is non empty set

f1 is Relation-like [:X,Y:] -defined Z -valued Function-like V18([:X,Y:],Z) Element of bool [:[:X,Y:],Z:]

f2 is Relation-like [:X,Y:] -defined Z -valued Function-like V18([:X,Y:],Z) Element of bool [:[:X,Y:],Z:]

f is set

x is set

(f1,f,x) is set

[f,x] is set

f1 . [f,x] is set

(f2,f,x) is set

f2 . [f,x] is set