:: BINOP_1 semantic presentation

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

bool [:X,X:] is non empty set
F1() is set
F2() is set
F3() is set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is non empty set
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 [:F1(),F2():] -defined F3() -valued Function-like V18([:F1(),F2():],F3()) Element of bool [:[:F1(),F2():],F3():]
Y is set
Z is set
(X,Y,Z) is set
[Y,Z] is set
X . [Y,Z] is set
F1() is set
F2() is set
F3() is set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is non empty set
X is set
Y is set
F4(X,Y) is set
F1() is non empty set
F2() is non empty set
F3() is non empty set
[:F1(),F2():] is non empty set
[:[:F1(),F2():],F3():] is non empty set
bool [:[:F1(),F2():],F3():] is non empty set
X is Element of [:F1(),F2():]
Y is set
Z is set
[Y,Z] is set
f2 is Element of F1()
f1 is Element of F2()
f is Element of F3()
x is Element of F1()
y is Element of F2()
[x,y] is set
X is Relation-like [:F1(),F2():] -defined F3() -valued Function-like V18([:F1(),F2():],F3()) Element of bool [:[:F1(),F2():],F3():]
Y is Element of F1()
Z is Element of F2()
(F1(),F2(),F3(),X,Y,Z) is Element of F3()
[Y,Z] is set
X . [Y,Z] is set
f1 is Element of [:F1(),F2():]
X . f1 is Element of F3()
F1() is non empty set
F2() is non empty set
F3() is non empty set
[:F1(),F2():] is non empty set
[:[:F1(),F2():],F3():] is non empty set
bool [:[:F1(),F2():],F3():] is non empty set
X is Element of F1()
Y is Element of F2()
F4(X,Y) is Element of F3()
X is set
[:X,X:] is set
[:[:X,X:],X:] is set
bool [:[:X,X:],X:] is non empty set
is set

bool is non empty set

bool is non empty set

bool {} is non empty set
[:(dom X),(rng X):] is set

({},X,Z,f1) is Relation-like Function-like Element of {}
[Z,f1] is 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,({},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

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

({},X,Z,Y) is Relation-like Function-like Element of {}
[Z,Y] is 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
c10 is Element of X
c11 is Element of X
(X,Y,c10,c11) is Element of X
[c10,c11] is set
Y . [c10,c11] is set
c12 is Element of X
(X,Z,(X,Y,c10,c11),c12) is Element of X
[(X,Y,c10,c11),c12] is set
Z . [(X,Y,c10,c11),c12] is set
(X,Z,c10,c12) is Element of X
[c10,c12] is set
Z . [c10,c12] is set
(X,Z,c11,c12) is Element of X
[c11,c12] is set
Z . [c11,c12] is set
(X,Y,(X,Z,c10,c12),(X,Z,c11,c12)) is Element of X
[(X,Z,c10,c12),(X,Z,c11,c12)] is set
Y . [(X,Z,c10,c12),(X,Z,c11,c12)] is set
c13 is Element of X
c14 is Element of X
c15 is Element of X
(X,Y,c14,c15) is Element of X
[c14,c15] is set
Y . [c14,c15] is set
(X,Z,c13,(X,Y,c14,c15)) is Element of X
[c13,(X,Y,c14,c15)] is set
Z . [c13,(X,Y,c14,c15)] is set
(X,Z,c13,c14) is Element of X
[c13,c14] is set
Z . [c13,c14] is set
(X,Z,c13,c15) is Element of X
[c13,c15] is set
Z . [c13,c15] is set
(X,Y,(X,Z,c13,c14),(X,Z,c13,c15)) is Element of X
[(X,Z,c13,c14),(X,Z,c13,c15)] is set
Y . [(X,Z,c13,c14),(X,Z,c13,c15)] 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
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
c10 is Element of X
c11 is Element of X
(X,Y,c10,c11) is Element of X
[c10,c11] is set
Y . [c10,c11] is set
c12 is Element of X
(X,Z,(X,Y,c10,c11),c12) is Element of X
[(X,Y,c10,c11),c12] is set
Z . [(X,Y,c10,c11),c12] is set
(X,Z,c10,c12) is Element of X
[c10,c12] is set
Z . [c10,c12] is set
(X,Z,c11,c12) is Element of X
[c11,c12] is set
Z . [c11,c12] is set
(X,Y,(X,Z,c10,c12),(X,Z,c11,c12)) is Element of X
[(X,Z,c10,c12),(X,Z,c11,c12)] is set
Y . [(X,Z,c10,c12),(X,Z,c11,c12)] is set
c13 is Element of X
c14 is Element of X
(X,Y,c13,c14) is Element of X
[c13,c14] is set
Y . [c13,c14] is set
c15 is Element of X
(X,Z,(X,Y,c13,c14),c15) is Element of X
[(X,Y,c13,c14),c15] is set
Z . [(X,Y,c13,c14),c15] is set
(X,Z,c13,c15) is Element of X
[c13,c15] is set
Z . [c13,c15] is set
(X,Z,c14,c15) is Element of X
[c14,c15] is set
Z . [c14,c15] is set
(X,Y,(X,Z,c13,c15),(X,Z,c14,c15)) is Element of X
[(X,Z,c13,c15),(X,Z,c14,c15)] is set
Y . [(X,Z,c13,c15),(X,Z,c14,c15)] 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 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

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

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

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

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
F1() is set
F2() is set
F3() is set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is non empty set
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 [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom X is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is non empty set
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
F3() is set
F1() is set
F2() is set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is non empty set
X is set
Y is set
Z is set
F4(X,Y) is set
f1 is set
X is set
Y is set
Z is set
F4(X,Y) is set
X is Relation-like [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom X is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is non empty set
Y is set
Z is set
[Y,Z] is set
F4(Y,Z) is set
f1 is set
F4(Y,Z) is set
f1 is set
Y is set
Z is set
[Y,Z] is set
(X,Y,Z) is set
X . [Y,Z] is set
F4(Y,Z) is set
F1() is set
F2() is set
F3() is set
[:F1(),F2():] is set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is non empty set
X is set
Y is set
F4(X,Y) is set
X is Relation-like [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom X is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is non empty set
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
F4(f,x) is set
F1() is non empty set
F2() is non empty set
F3() is set
[:F1(),F2():] is non empty set
[:[:F1(),F2():],F3():] is set
bool [:[:F1(),F2():],F3():] is non empty set
X is set
Y is set
F4(X,Y) is set
X is Relation-like [:F1(),F2():] -defined F3() -valued Function-like Element of bool [:[:F1(),F2():],F3():]
dom X is Relation-like F1() -defined F2() -valued Element of bool [:F1(),F2():]
bool [:F1(),F2():] is non empty set
Y is Element of F1()
Z is Element of F2()
[Y,Z] is set
f1 is Element of F1()
f2 is Element of F2()
[f1,f2] is set
f is Element of F1()
x is Element of F2()
[f,x] is set
(X,f,x) is set
X . [f,x] is set
F4(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

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