:: FUNCOP_1 semantic presentation

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

1 is non empty set

{{},1} is non empty set

z is set

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

[:z,z:] is Relation-like set

[:z,[:z,z:]:] is Relation-like set

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

id z is Relation-like z -defined z -valued Function-like one-to-one total V18(z,z) Element of bool [:z,z:]

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

<:(id z),(id z):> is Relation-like Function-like set

id [:z,z:] is Relation-like [:z,z:] -defined [:z,z:] -valued Function-like one-to-one total V18([:z,z:],[:z,z:]) Element of bool [:[:z,z:],[:z,z:]:]

[:[:z,z:],[:z,z:]:] is Relation-like set

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

(id [:z,z:]) * (delta z) is Relation-like z -defined [:z,z:] -valued Function-like V18(z,[:z,z:]) Element of bool [:z,[:z,z:]:]

[:(id z),(id z):] is Relation-like [:z,z:] -defined [:z,z:] -valued Function-like one-to-one total V18([:z,z:],[:z,z:]) Element of bool [:[:z,z:],[:z,z:]:]

[:(id z),(id z):] * (delta z) is Relation-like z -defined [:z,z:] -valued Function-like V18(z,[:z,z:]) Element of bool [:z,[:z,z:]:]

z is Relation-like Function-like set

proj1 z is set

A is set

z . A is set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

[y,x] is V15() set

{y,x} is non empty set

{y} is non empty set

{{y,x},{y}} is non empty set

e is V15() set

g is set

z is set

[g,z] is V15() set

{g,z} is non empty set

{g} is non empty set

{{g,z},{g}} is non empty set

[z,g] is V15() set

{z,g} is non empty set

{z} is non empty set

{{z,g},{z}} is non empty set

g is set

z is set

[g,z] is V15() set

{g,z} is non empty set

{g} is non empty set

{{g,z},{g}} is non empty set

z . A is set

x is set

y is set

e is set

[y,e] is V15() set

{y,e} is non empty set

{y} is non empty set

{{y,e},{y}} is non empty set

[e,y] is V15() set

{e,y} is non empty set

{e} is non empty set

{{e,y},{e}} is non empty set

z . A is set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

z . A is set

x is V15() set

y is set

e is set

[y,e] is V15() set

{y,e} is non empty set

{y} is non empty set

{{y,e},{y}} is non empty set

A is set

x is set

z . A is set

y is set

e is set

g is set

[e,g] is V15() set

{e,g} is non empty set

{e} is non empty set

{{e,g},{e}} is non empty set

e is set

g is set

[e,g] is V15() set

{e,g} is non empty set

{e} is non empty set

{{e,g},{e}} is non empty set

[g,e] is V15() set

{g,e} is non empty set

{g} is non empty set

{{g,e},{g}} is non empty set

z is set

x1 is set

[z,x1] is V15() set

{z,x1} is non empty set

{z} is non empty set

{{z,x1},{z}} is non empty set

z is set

x1 is set

[z,x1] is V15() set

{z,x1} is non empty set

{z} is non empty set

{{z,x1},{z}} is non empty set

e is set

g is set

[e,g] is V15() set

{e,g} is non empty set

{e} is non empty set

{{e,g},{e}} is non empty set

z is set

x1 is set

[z,x1] is V15() set

{z,x1} is non empty set

{z} is non empty set

{{z,x1},{z}} is non empty set

e is set

g is set

[e,g] is V15() set

{e,g} is non empty set

{e} is non empty set

{{e,g},{e}} is non empty set

A is Relation-like Function-like set

proj1 A is set

x is Relation-like Function-like set

proj1 x is set

y is set

z . y is set

e is set

g is set

[e,g] is V15() set

{e,g} is non empty set

{e} is non empty set

{{e,g},{e}} is non empty set

e is set

g is set

[e,g] is V15() set

{e,g} is non empty set

{e} is non empty set

{{e,g},{e}} is non empty set

A . y is set

[g,e] is V15() set

{g,e} is non empty set

{g} is non empty set

{{g,e},{g}} is non empty set

x . y is set

z . y is set

A . y is set

x . y is set

z . y is set

e is set

g is set

[e,g] is V15() set

{e,g} is non empty set

{e} is non empty set

{{e,g},{e}} is non empty set

A . y is set

x . y is set

A . y is set

x . y is set

A is Relation-like Function-like set

proj1 A is set

x is Relation-like Function-like set

proj1 x is set

y is set

A . y is set

x . y is set

e is set

g is set

[e,g] is V15() set

{e,g} is non empty set

{e} is non empty set

{{e,g},{e}} is non empty set

[g,e] is V15() set

{g,e} is non empty set

{g} is non empty set

{{g,e},{g}} is non empty set

z is set

x1 is set

[z,x1] is V15() set

{z,x1} is non empty set

{z} is non empty set

{{z,x1},{z}} is non empty set

z is set

x1 is set

[z,x1] is V15() set

{z,x1} is non empty set

{z} is non empty set

{{z,x1},{z}} is non empty set

[x1,z] is V15() set

{x1,z} is non empty set

{x1} is non empty set

{{x1,z},{x1}} is non empty set

z is set

x1 is set

[z,x1] is V15() set

{z,x1} is non empty set

{z} is non empty set

{{z,x1},{z}} is non empty set

e is set

g is set

[e,g] is V15() set

{e,g} is non empty set

{e} is non empty set

{{e,g},{e}} is non empty set

[g,e] is V15() set

{g,e} is non empty set

{g} is non empty set

{{g,e},{g}} is non empty set

z is Relation-like Function-like set

A is Relation-like Function-like set

<:z,A:> is Relation-like Function-like set

<:A,z:> is Relation-like Function-like set

(<:A,z:>) is Relation-like Function-like set

proj1 <:z,A:> is set

proj1 A is set

proj1 z is set

(proj1 A) /\ (proj1 z) is set

proj1 <:A,z:> is set

x is set

<:A,z:> . x is set

A . x is set

z . x is set

[(A . x),(z . x)] is V15() set

{(A . x),(z . x)} is non empty set

{(A . x)} is non empty set

{{(A . x),(z . x)},{(A . x)}} is non empty set

<:z,A:> . x is set

[(z . x),(A . x)] is V15() set

{(z . x),(A . x)} is non empty set

{(z . x)} is non empty set

{{(z . x),(A . x)},{(z . x)}} is non empty set

(<:A,z:>) . x is set

proj1 (<:A,z:>) is set

z is Relation-like Function-like set

(z) is Relation-like Function-like set

A is set

z | A is Relation-like Function-like set

((z | A)) is Relation-like Function-like set

(z) | A is Relation-like Function-like set

proj1 (z | A) is set

proj1 z is set

(proj1 z) /\ A is set

proj1 (z) is set

(proj1 (z)) /\ A is set

proj1 ((z) | A) is set

x is set

(z | A) . x is set

y is set

e is set

[y,e] is V15() set

{y,e} is non empty set

{y} is non empty set

{{y,e},{y}} is non empty set

y is set

e is set

[y,e] is V15() set

{y,e} is non empty set

{y} is non empty set

{{y,e},{y}} is non empty set

z . x is set

((z | A)) . x is set

[e,y] is V15() set

{e,y} is non empty set

{e} is non empty set

{{e,y},{e}} is non empty set

(z) . x is set

((z) | A) . x is set

(z | A) . x is set

z . x is set

((z | A)) . x is set

(z) . x is set

((z) | A) . x is set

(z | A) . x is set

y is set

e is set

[y,e] is V15() set

{y,e} is non empty set

{y} is non empty set

{{y,e},{y}} is non empty set

((z | A)) . x is set

((z) | A) . x is set

((z | A)) . x is set

((z) | A) . x is set

proj1 ((z | A)) is set

z is set

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

[:z,z:] is Relation-like set

[:z,[:z,z:]:] is Relation-like set

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

((delta z)) is Relation-like Function-like set

id z is Relation-like z -defined z -valued Function-like one-to-one total V18(z,z) Element of bool [:z,z:]

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

<:(id z),(id z):> is Relation-like Function-like set

(<:(id z),(id z):>) is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

<:z,A:> is Relation-like Function-like set

x is set

<:z,A:> | x is Relation-like Function-like set

z | x is Relation-like Function-like set

<:(z | x),A:> is Relation-like Function-like set

proj1 (<:z,A:> | x) is set

proj1 <:z,A:> is set

(proj1 <:z,A:>) /\ x is set

proj1 z is set

proj1 A is set

(proj1 z) /\ (proj1 A) is set

((proj1 z) /\ (proj1 A)) /\ x is set

(proj1 z) /\ x is set

((proj1 z) /\ x) /\ (proj1 A) is set

proj1 (z | x) is set

(proj1 (z | x)) /\ (proj1 A) is set

y is set

(<:z,A:> | x) . y is set

<:z,A:> . y is set

z . y is set

A . y is set

[(z . y),(A . y)] is V15() set

{(z . y),(A . y)} is non empty set

{(z . y)} is non empty set

{{(z . y),(A . y)},{(z . y)}} is non empty set

(z | x) . y is set

[((z | x) . y),(A . y)] is V15() set

{((z | x) . y),(A . y)} is non empty set

{((z | x) . y)} is non empty set

{{((z | x) . y),(A . y)},{((z | x) . y)}} is non empty set

z is Relation-like Function-like set

A is Relation-like Function-like set

<:z,A:> is Relation-like Function-like set

x is set

<:z,A:> | x is Relation-like Function-like set

A | x is Relation-like Function-like set

<:z,(A | x):> is Relation-like Function-like set

<:A,z:> is Relation-like Function-like set

(<:A,z:>) is Relation-like Function-like set

(<:A,z:>) | x is Relation-like Function-like set

<:A,z:> | x is Relation-like Function-like set

((<:A,z:> | x)) is Relation-like Function-like set

<:(A | x),z:> is Relation-like Function-like set

(<:(A | x),z:>) is Relation-like Function-like set

z is set

A is set

{A} is non empty set

[:z,{A}:] is Relation-like set

z is set

A is set

(z,A) is set

{A} is non empty set

[:z,{A}:] is Relation-like set

x is set

y is set

[x,y] is V15() set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

e is set

[x,e] is V15() set

{x,e} is non empty set

{{x,e},{x}} is non empty set

x is set

z is set

A is set

x is set

(z,x) is Relation-like Function-like set

{x} is non empty set

[:z,{x}:] is Relation-like set

(z,x) . A is set

[A,x] is V15() set

{A,x} is non empty set

{A} is non empty set

{{A,x},{A}} is non empty set

z is set

A is set

(z,A) is Relation-like Function-like set

{A} is non empty set

[:z,{A}:] is Relation-like set

proj2 (z,A) is set

z is Relation-like Function-like set

proj2 z is set

proj1 z is set

A is set

{A} is non empty set

((proj1 z),A) is Relation-like Function-like set

[:(proj1 z),{A}:] is Relation-like set

proj1 ((proj1 z),A) is set

proj2 ((proj1 z),A) is set

z is set

({},z) is Relation-like Function-like set

{z} is non empty set

[:{},{z}:] is Relation-like set

A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

z is set

(A,z) is Relation-like Function-like set

{z} is non empty set

[:A,{z}:] is Relation-like set

A is non empty set

z is set

(A,z) is Relation-like Function-like set

{z} is non empty set

[:A,{z}:] is Relation-like non empty set

z is set

({},z) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

{z} is non empty set

[:{},{z}:] is Relation-like set

proj1 ({},z) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

A is set

({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

{A} is non empty set

[:{},{A}:] is Relation-like set

proj2 ({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set

z is Relation-like Function-like set

proj1 z is set

A is set

((proj1 z),A) is Relation-like Function-like set

{A} is non empty set

[:(proj1 z),{A}:] is Relation-like set

({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

[:{},{A}:] is Relation-like set

proj1 ({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

the Element of proj1 z is Element of proj1 z

y is set

z . the Element of proj1 z is set

e is set

z . e is set

proj2 z is set

z is set

A is set

(z,A) is Relation-like Function-like set

{A} is non empty set

[:z,{A}:] is Relation-like set

x is set

(z,A) | x is Relation-like Function-like set

z /\ x is set

((z /\ x),A) is Relation-like Function-like set

[:(z /\ x),{A}:] is Relation-like set

proj1 ((z,A) | x) is set

proj1 (z,A) is set

(proj1 (z,A)) /\ x is set

proj1 ((z /\ x),A) is set

y is set

((z,A) | x) . y is set

(z,A) . y is set

((z /\ x),A) . y is set

z is set

A is set

(z,A) is Relation-like Function-like set

{A} is non empty set

[:z,{A}:] is Relation-like set

proj1 (z,A) is set

proj2 (z,A) is set

({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set

[:{},{A}:] is Relation-like set

proj2 ({},A) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set

z is set

A is set

(z,A) is Relation-like Function-like set

{A} is non empty set

[:z,{A}:] is Relation-like set

x is set

(z,A) " x is set

proj2 (z,A) is set

{A} /\ x is set

(z,A) " {A} is set

proj1 (z,A) is set

z is set

A is set

(z,A) is Relation-like Function-like set

{A} is non empty set

[:z,{A}:] is Relation-like set

(z,A) " {A} is set

z is set

A is set

(z,A) is Relation-like Function-like set

{A} is non empty set

[:z,{A}:] is Relation-like set

x is set

(z,A) " x is set

proj2 (z,A) is set

z is Relation-like Function-like set

proj1 z is set

A is set

x is set

(A,x) is Relation-like Function-like set

{x} is non empty set

[:A,{x}:] is Relation-like set

(A,x) * z is Relation-like Function-like set

z . x is set

(A,(z . x)) is Relation-like Function-like set

{(z . x)} is non empty set

[:A,{(z . x)}:] is Relation-like set

y is set

proj1 ((A,x) * z) is set

proj1 (A,x) is set

((A,x) * z) . y is set

(A,x) . y is set

z . ((A,x) . y) is set

(A,(z . x)) . y is set

(A,x) " (proj1 z) is set

proj1 (A,(z . x)) is set

z is Relation-like Function-like set

proj1 z is set

A is set

x is set

(A,x) is Relation-like Function-like set

{x} is non empty set

[:A,{x}:] is Relation-like set

(A,x) * z is Relation-like Function-like set

proj1 ((A,x) * z) is set

the Element of A is Element of A

proj1 (A,x) is set

(A,x) . the Element of A is set

z is Relation-like Function-like set

A is set

z " A is set

x is set

(A,x) is Relation-like Function-like set

{x} is non empty set

[:A,{x}:] is Relation-like set

z * (A,x) is Relation-like Function-like set

((z " A),x) is Relation-like Function-like set

[:(z " A),{x}:] is Relation-like set

proj1 (z * (A,x)) is set

proj1 (A,x) is set

z " (proj1 (A,x)) is set

y is set

z . y is set

(z * (A,x)) . y is set

(A,x) . (z . y) is set

((z " A),x) . y is set

proj1 ((z " A),x) is set

z is set

A is set

x is set

[A,x] is V15() set

{A,x} is non empty set

{A} is non empty set

{{A,x},{A}} is non empty set

(z,[A,x]) is Relation-like Function-like set

{[A,x]} is Relation-like Function-like non empty set

[:z,{[A,x]}:] is Relation-like set

((z,[A,x])) is Relation-like Function-like set

[x,A] is V15() set

{x,A} is non empty set

{x} is non empty set

{{x,A},{x}} is non empty set

(z,[x,A]) is Relation-like Function-like set

{[x,A]} is Relation-like Function-like non empty set

[:z,{[x,A]}:] is Relation-like set

proj1 ((z,[A,x])) is set

proj1 (z,[A,x]) is set

y is set

(z,[A,x]) . y is set

((z,[A,x])) . y is set

(z,[x,A]) . y is set

proj1 (z,[x,A]) is set

A is Relation-like Function-like set

x is Relation-like Function-like set

<:A,x:> is Relation-like Function-like set

z is Relation-like Function-like set

<:A,x:> * z is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is Relation-like Function-like set

(z,A,x) is set

<:A,x:> is Relation-like Function-like set

<:A,x:> * z is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

<:z,A:> is Relation-like Function-like set

x is Relation-like Function-like set

<:z,A:> * x is Relation-like Function-like set

proj1 (<:z,A:> * x) is set

y is set

(<:z,A:> * x) . y is set

z . y is set

A . y is set

x . ((z . y),(A . y)) is set

[(z . y),(A . y)] is V15() set

{(z . y),(A . y)} is non empty set

{(z . y)} is non empty set

{{(z . y),(A . y)},{(z . y)}} is non empty set

x . [(z . y),(A . y)] is set

proj1 <:z,A:> is set

<:z,A:> . y is set

x . (<:z,A:> . y) is set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is Relation-like Function-like set

(x,z,A) is Relation-like Function-like set

<:z,A:> is Relation-like Function-like set

<:z,A:> * x is Relation-like Function-like set

proj1 (x,z,A) is set

y is Relation-like Function-like set

proj1 y is set

e is set

y . e is set

z . e is set

A . e is set

x . ((z . e),(A . e)) is set

[(z . e),(A . e)] is V15() set

{(z . e),(A . e)} is non empty set

{(z . e)} is non empty set

{{(z . e),(A . e)},{(z . e)}} is non empty set

x . [(z . e),(A . e)] is set

(x,z,A) . e is set

y is set

x is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

(x,z,A) is Relation-like Function-like set

<:z,A:> is Relation-like Function-like set

<:z,A:> * x is Relation-like Function-like set

proj1 (x,z,A) is set

(x,z,A) . y is set

z . y is set

A . y is set

x . ((z . y),(A . y)) is set

[(z . y),(A . y)] is V15() set

{(z . y),(A . y)} is non empty set

{(z . y)} is non empty set

{{(z . y),(A . y)},{(z . y)}} is non empty set

x . [(z . y),(A . y)] is set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is Relation-like Function-like set

y is set

z | y is Relation-like Function-like set

A | y is Relation-like Function-like set

e is Relation-like Function-like set

(e,z,x) is Relation-like Function-like set

<:z,x:> is Relation-like Function-like set

<:z,x:> * e is Relation-like Function-like set

(e,z,x) | y is Relation-like Function-like set

(e,A,x) is Relation-like Function-like set

<:A,x:> is Relation-like Function-like set

<:A,x:> * e is Relation-like Function-like set

(e,A,x) | y is Relation-like Function-like set

<:z,x:> | y is Relation-like Function-like set

(<:z,x:> | y) * e is Relation-like Function-like set

<:(z | y),x:> is Relation-like Function-like set

<:(z | y),x:> * e is Relation-like Function-like set

<:A,x:> | y is Relation-like Function-like set

(<:A,x:> | y) * e is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is Relation-like Function-like set

y is set

z | y is Relation-like Function-like set

A | y is Relation-like Function-like set

e is Relation-like Function-like set

(e,x,z) is Relation-like Function-like set

<:x,z:> is Relation-like Function-like set

<:x,z:> * e is Relation-like Function-like set

(e,x,z) | y is Relation-like Function-like set

(e,x,A) is Relation-like Function-like set

<:x,A:> is Relation-like Function-like set

<:x,A:> * e is Relation-like Function-like set

(e,x,A) | y is Relation-like Function-like set

<:x,z:> | y is Relation-like Function-like set

(<:x,z:> | y) * e is Relation-like Function-like set

<:x,(z | y):> is Relation-like Function-like set

<:x,(z | y):> * e is Relation-like Function-like set

<:x,A:> | y is Relation-like Function-like set

(<:x,A:> | y) * e is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is Relation-like Function-like set

x * z is Relation-like Function-like set

x * A is Relation-like Function-like set

y is Relation-like Function-like set

(y,z,A) is Relation-like Function-like set

<:z,A:> is Relation-like Function-like set

<:z,A:> * y is Relation-like Function-like set

x * (y,z,A) is Relation-like Function-like set

(y,(x * z),(x * A)) is Relation-like Function-like set

<:(x * z),(x * A):> is Relation-like Function-like set

<:(x * z),(x * A):> * y is Relation-like Function-like set

x * <:z,A:> is Relation-like Function-like set

(x * <:z,A:>) * y is Relation-like Function-like set

A is Relation-like Function-like set

proj1 A is set

x is set

((proj1 A),x) is Relation-like Function-like set

{x} is non empty set

[:(proj1 A),{x}:] is Relation-like set

<:A,((proj1 A),x):> is Relation-like Function-like set

z is Relation-like Function-like set

<:A,((proj1 A),x):> * z is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is set

(z,A,x) is set

proj1 A is set

((proj1 A),x) is Relation-like Function-like set

{x} is non empty set

[:(proj1 A),{x}:] is Relation-like set

<:A,((proj1 A),x):> is Relation-like Function-like set

<:A,((proj1 A),x):> * z is Relation-like Function-like set

A is Relation-like Function-like set

z is Relation-like Function-like set

x is set

(A,z,x) is Relation-like Function-like set

proj1 z is set

((proj1 z),x) is Relation-like Function-like set

{x} is non empty set

[:(proj1 z),{x}:] is Relation-like set

<:z,((proj1 z),x):> is Relation-like Function-like set

<:z,((proj1 z),x):> * A is Relation-like Function-like set

(A,z,((proj1 z),x)) is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is set

z . x is set

y is set

(A,z,y) is Relation-like Function-like set

proj1 z is set

((proj1 z),y) is Relation-like Function-like set

{y} is non empty set

[:(proj1 z),{y}:] is Relation-like set

<:z,((proj1 z),y):> is Relation-like Function-like set

<:z,((proj1 z),y):> * A is Relation-like Function-like set

proj1 (A,z,y) is set

(A,z,y) . x is set

A . ((z . x),y) is set

[(z . x),y] is V15() set

{(z . x),y} is non empty set

{(z . x)} is non empty set

{{(z . x),y},{(z . x)}} is non empty set

A . [(z . x),y] is set

proj1 <:z,((proj1 z),y):> is set

proj1 ((proj1 z),y) is set

(proj1 z) /\ (proj1 ((proj1 z),y)) is set

((proj1 z),y) . x is set

A . ((z . x),(((proj1 z),y) . x)) is set

[(z . x),(((proj1 z),y) . x)] is V15() set

{(z . x),(((proj1 z),y) . x)} is non empty set

{{(z . x),(((proj1 z),y) . x)},{(z . x)}} is non empty set

A . [(z . x),(((proj1 z),y) . x)] is set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is set

z | x is Relation-like Function-like set

A | x is Relation-like Function-like set

y is Relation-like Function-like set

e is set

(y,z,e) is Relation-like Function-like set

proj1 z is set

((proj1 z),e) is Relation-like Function-like set

{e} is non empty set

[:(proj1 z),{e}:] is Relation-like set

<:z,((proj1 z),e):> is Relation-like Function-like set

<:z,((proj1 z),e):> * y is Relation-like Function-like set

(y,z,e) | x is Relation-like Function-like set

(y,A,e) is Relation-like Function-like set

proj1 A is set

((proj1 A),e) is Relation-like Function-like set

[:(proj1 A),{e}:] is Relation-like set

<:A,((proj1 A),e):> is Relation-like Function-like set

<:A,((proj1 A),e):> * y is Relation-like Function-like set

(y,A,e) | x is Relation-like Function-like set

(proj1 z) /\ x is set

proj1 (z | x) is set

(proj1 A) /\ x is set

((proj1 z),e) | x is Relation-like Function-like set

(((proj1 A) /\ x),e) is Relation-like Function-like set

[:((proj1 A) /\ x),{e}:] is Relation-like set

((proj1 A),e) | x is Relation-like Function-like set

(y,z,((proj1 z),e)) is Relation-like Function-like set

(y,z,((proj1 z),e)) | x is Relation-like Function-like set

(y,A,((proj1 z),e)) is Relation-like Function-like set

<:A,((proj1 z),e):> is Relation-like Function-like set

<:A,((proj1 z),e):> * y is Relation-like Function-like set

(y,A,((proj1 z),e)) | x is Relation-like Function-like set

(y,A,((proj1 A),e)) is Relation-like Function-like set

(y,A,((proj1 A),e)) | x is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

A * z is Relation-like Function-like set

x is Relation-like Function-like set

y is set

(x,z,y) is Relation-like Function-like set

proj1 z is set

((proj1 z),y) is Relation-like Function-like set

{y} is non empty set

[:(proj1 z),{y}:] is Relation-like set

<:z,((proj1 z),y):> is Relation-like Function-like set

<:z,((proj1 z),y):> * x is Relation-like Function-like set

A * (x,z,y) is Relation-like Function-like set

(x,(A * z),y) is Relation-like Function-like set

proj1 (A * z) is set

((proj1 (A * z)),y) is Relation-like Function-like set

[:(proj1 (A * z)),{y}:] is Relation-like set

<:(A * z),((proj1 (A * z)),y):> is Relation-like Function-like set

<:(A * z),((proj1 (A * z)),y):> * x is Relation-like Function-like set

proj1 ((proj1 z),y) is set

A * ((proj1 z),y) is Relation-like Function-like set

proj1 (A * ((proj1 z),y)) is set

e is set

A . e is set

(A * ((proj1 z),y)) . e is set

((proj1 z),y) . (A . e) is set

(x,z,((proj1 z),y)) is Relation-like Function-like set

A * (x,z,((proj1 z),y)) is Relation-like Function-like set

(x,(A * z),(A * ((proj1 z),y))) is Relation-like Function-like set

<:(A * z),(A * ((proj1 z),y)):> is Relation-like Function-like set

<:(A * z),(A * ((proj1 z),y)):> * x is Relation-like Function-like set

z is Relation-like Function-like set

A is set

id A is Relation-like A -defined A -valued Function-like one-to-one total V18(A,A) Element of bool [:A,A:]

[:A,A:] is Relation-like set

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

z | A is Relation-like Function-like set

x is Relation-like Function-like set

y is set

(x,z,y) is Relation-like Function-like set

proj1 z is set

((proj1 z),y) is Relation-like Function-like set

{y} is non empty set

[:(proj1 z),{y}:] is Relation-like set

<:z,((proj1 z),y):> is Relation-like Function-like set

<:z,((proj1 z),y):> * x is Relation-like Function-like set

(id A) * (x,z,y) is Relation-like A -defined Function-like set

(x,(z | A),y) is Relation-like Function-like set

proj1 (z | A) is set

((proj1 (z | A)),y) is Relation-like Function-like set

[:(proj1 (z | A)),{y}:] is Relation-like set

<:(z | A),((proj1 (z | A)),y):> is Relation-like Function-like set

<:(z | A),((proj1 (z | A)),y):> * x is Relation-like Function-like set

(id A) * z is Relation-like A -defined Function-like set

(x,((id A) * z),y) is Relation-like Function-like set

proj1 ((id A) * z) is set

((proj1 ((id A) * z)),y) is Relation-like Function-like set

[:(proj1 ((id A) * z)),{y}:] is Relation-like set

<:((id A) * z),((proj1 ((id A) * z)),y):> is Relation-like Function-like set

<:((id A) * z),((proj1 ((id A) * z)),y):> * x is Relation-like Function-like set

x is Relation-like Function-like set

proj1 x is set

A is set

((proj1 x),A) is Relation-like Function-like set

{A} is non empty set

[:(proj1 x),{A}:] is Relation-like set

<:((proj1 x),A),x:> is Relation-like Function-like set

z is Relation-like Function-like set

<:((proj1 x),A),x:> * z is Relation-like Function-like set

z is Relation-like Function-like set

A is set

x is Relation-like Function-like set

(z,A,x) is set

proj1 x is set

((proj1 x),A) is Relation-like Function-like set

{A} is non empty set

[:(proj1 x),{A}:] is Relation-like set

<:((proj1 x),A),x:> is Relation-like Function-like set

<:((proj1 x),A),x:> * z is Relation-like Function-like set

A is Relation-like Function-like set

x is set

z is Relation-like Function-like set

(A,x,z) is Relation-like Function-like set

proj1 z is set

((proj1 z),x) is Relation-like Function-like set

{x} is non empty set

[:(proj1 z),{x}:] is Relation-like set

<:((proj1 z),x),z:> is Relation-like Function-like set

<:((proj1 z),x),z:> * A is Relation-like Function-like set

(A,((proj1 z),x),z) is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is set

z . x is set

y is set

(A,y,z) is Relation-like Function-like set

proj1 z is set

((proj1 z),y) is Relation-like Function-like set

{y} is non empty set

[:(proj1 z),{y}:] is Relation-like set

<:((proj1 z),y),z:> is Relation-like Function-like set

<:((proj1 z),y),z:> * A is Relation-like Function-like set

proj1 (A,y,z) is set

(A,y,z) . x is set

A . (y,(z . x)) is set

[y,(z . x)] is V15() set

{y,(z . x)} is non empty set

{{y,(z . x)},{y}} is non empty set

A . [y,(z . x)] is set

proj1 <:((proj1 z),y),z:> is set

proj1 ((proj1 z),y) is set

(proj1 ((proj1 z),y)) /\ (proj1 z) is set

((proj1 z),y) . x is set

A . ((((proj1 z),y) . x),(z . x)) is set

[(((proj1 z),y) . x),(z . x)] is V15() set

{(((proj1 z),y) . x),(z . x)} is non empty set

{(((proj1 z),y) . x)} is non empty set

{{(((proj1 z),y) . x),(z . x)},{(((proj1 z),y) . x)}} is non empty set

A . [(((proj1 z),y) . x),(z . x)] is set

z is Relation-like Function-like set

A is Relation-like Function-like set

x is set

z | x is Relation-like Function-like set

A | x is Relation-like Function-like set

y is Relation-like Function-like set

e is set

(y,e,z) is Relation-like Function-like set

proj1 z is set

((proj1 z),e) is Relation-like Function-like set

{e} is non empty set

[:(proj1 z),{e}:] is Relation-like set

<:((proj1 z),e),z:> is Relation-like Function-like set

<:((proj1 z),e),z:> * y is Relation-like Function-like set

(y,e,z) | x is Relation-like Function-like set

(y,e,A) is Relation-like Function-like set

proj1 A is set

((proj1 A),e) is Relation-like Function-like set

[:(proj1 A),{e}:] is Relation-like set

<:((proj1 A),e),A:> is Relation-like Function-like set

<:((proj1 A),e),A:> * y is Relation-like Function-like set

(y,e,A) | x is Relation-like Function-like set

(proj1 z) /\ x is set

proj1 (z | x) is set

(proj1 A) /\ x is set

((proj1 z),e) | x is Relation-like Function-like set

(((proj1 A) /\ x),e) is Relation-like Function-like set

[:((proj1 A) /\ x),{e}:] is Relation-like set

((proj1 A),e) | x is Relation-like Function-like set

(y,((proj1 z),e),z) is Relation-like Function-like set

(y,((proj1 z),e),z) | x is Relation-like Function-like set

(y,((proj1 z),e),A) is Relation-like Function-like set

<:((proj1 z),e),A:> is Relation-like Function-like set

<:((proj1 z),e),A:> * y is Relation-like Function-like set

(y,((proj1 z),e),A) | x is Relation-like Function-like set

(y,((proj1 A),e),A) is Relation-like Function-like set

(y,((proj1 A),e),A) | x is Relation-like Function-like set

z is Relation-like Function-like set

A is Relation-like Function-like set

A * z is Relation-like Function-like set

x is Relation-like Function-like set

y is set

(x,y,z) is Relation-like Function-like set

proj1 z is set

((proj1 z),y) is Relation-like Function-like set

{y} is non empty set

[:(proj1 z),{y}:] is Relation-like set

<:((proj1 z),y),z:> is Relation-like Function-like set

<:((proj1 z),y),z:> * x is Relation-like Function-like set

A * (x,y,z) is Relation-like Function-like set

(x,y,(A * z)) is Relation-like Function-like set

proj1 (A * z) is set

((proj1 (A * z)),y) is Relation-like Function-like set

[:(proj1 (A * z)),{y}:] is Relation-like set

<:((proj1 (A * z)),y),(A * z):> is Relation-like Function-like set

<:((proj1 (A * z)),y),(A * z):> * x is Relation-like Function-like set

proj1 ((proj1 z),y) is set

A * ((proj1 z),y) is Relation-like Function-like set

proj1 (A * ((proj1 z),y)) is set

e is set

A . e is set

(A * ((proj1 z),y)) . e is set

((proj1 z),y) . (A . e) is set

(x,((proj1 z),y),z) is Relation-like Function-like set

A * (x,((proj1 z),y),z) is Relation-like Function-like set

(x,(A * ((proj1 z),y)),(A * z)) is Relation-like Function-like set

<:(A * ((proj1 z),y)),(A * z):> is Relation-like Function-like set

<:(A * ((proj1 z),y)),(A * z):> * x is Relation-like Function-like set

z is Relation-like Function-like set

A is set

id A is Relation-like A -defined A -valued Function-like one-to-one total V18(A,A) Element of bool [:A,A:]

[:A,A:] is Relation-like set

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

z | A is Relation-like Function-like set

x is Relation-like Function-like set

y is set

(x,y,z) is Relation-like Function-like set

proj1 z is set

((proj1 z),y) is Relation-like Function-like set

{y} is non empty set

[:(proj1 z),{y}:] is Relation-like set

<:((proj1 z),y),z:> is Relation-like Function-like set

<:((proj1 z),y),z:> * x is Relation-like Function-like set

(id A) * (x,y,z) is Relation-like A -defined Function-like set

(x,y,(z | A)) is Relation-like Function-like set

proj1 (z | A) is set

((proj1 (z | A)),y) is Relation-like Function-like set

[:(proj1 (z | A)),{y}:] is Relation-like set

<:((proj1 (z | A)),y),(z | A):> is Relation-like Function-like set

<:((proj1 (z | A)),y),(z | A):> * x is Relation-like Function-like set

(id A) * z is Relation-like A -defined Function-like set

(x,y,((id A) * z)) is Relation-like Function-like set

proj1 ((id A) * z) is set

((proj1 ((id A) * z)),y) is Relation-like Function-like set

[:(proj1 ((id A) * z)),{y}:] is Relation-like set

<:((proj1 ((id A) * z)),y),((id A) * z):> is Relation-like Function-like set

<:((proj1 ((id A) * z)),y),((id A) * z):> * x is Relation-like Function-like set

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

A is set

[:A,z:] is Relation-like set

bool [:A,z:] is non empty set

x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]

e is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]

(x,y,e) is Relation-like Function-like set

<:y,e:> is Relation-like Function-like set

<:y,e:> * x is Relation-like z -valued Function-like set

<:y,e:> is Relation-like A -defined [:z,z:] -valued Function-like total V18(A,[:z,z:]) Element of bool [:A,[:z,z:]:]

[:A,[:z,z:]:] is Relation-like set

bool [:A,[:z,z:]:] is non empty set

x * <:y,e:> is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

A is set

[:A,z:] is Relation-like set

bool [:A,z:] is non empty set

x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]

e is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]

(x,y,e) is Relation-like Function-like set

<:y,e:> is Relation-like Function-like set

<:y,e:> * x is Relation-like z -valued Function-like set

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

A is non empty set

[:A,z:] is Relation-like non empty set

bool [:A,z:] is non empty set

x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

e is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(z,A,x,y,e) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

<:y,e:> is Relation-like Function-like set

<:y,e:> * x is Relation-like z -valued Function-like set

g is Element of A

(z,A,x,y,e) . g is Element of z

y . g is Element of z

e . g is Element of z

x . ((y . g),(e . g)) is Element of z

[(y . g),(e . g)] is V15() set

{(y . g),(e . g)} is non empty set

{(y . g)} is non empty set

{{(y . g),(e . g)},{(y . g)}} is non empty set

x . [(y . g),(e . g)] is set

dom (z,A,x,y,e) is non empty Element of bool A

bool A is non empty set

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

A is non empty set

[:A,z:] is Relation-like non empty set

bool [:A,z:] is non empty set

x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

e is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(z,A,x,y,e) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

<:y,e:> is Relation-like Function-like set

<:y,e:> * x is Relation-like z -valued Function-like set

g is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

z is Element of A

g . z is Element of z

y . z is Element of z

e . z is Element of z

x . ((y . z),(e . z)) is Element of z

[(y . z),(e . z)] is V15() set

{(y . z),(e . z)} is non empty set

{(y . z)} is non empty set

{{(y . z),(e . z)},{(y . z)}} is non empty set

x . [(y . z),(e . z)] is set

(z,A,x,y,e) . z is Element of z

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

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

id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]

A is non empty set

[:A,z:] is Relation-like non empty set

bool [:A,z:] is non empty set

x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

e is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

(z,z,x,(id z),e) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

<:(id z),e:> is Relation-like Function-like set

<:(id z),e:> * x is Relation-like z -valued Function-like set

(z,z,x,(id z),e) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

e * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(z,A,x,y,(e * y)) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

<:y,(e * y):> is Relation-like Function-like set

<:y,(e * y):> * x is Relation-like z -valued Function-like set

(id z) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(z,A,x,((id z) * y),(e * y)) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

<:((id z) * y),(e * y):> is Relation-like Function-like set

<:((id z) * y),(e * y):> * x is Relation-like z -valued Function-like set

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

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

id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]

A is non empty set

[:A,z:] is Relation-like non empty set

bool [:A,z:] is non empty set

x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

e is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

(z,z,x,e,(id z)) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

<:e,(id z):> is Relation-like Function-like set

<:e,(id z):> * x is Relation-like z -valued Function-like set

(z,z,x,e,(id z)) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

e * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(z,A,x,(e * y),y) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

<:(e * y),y:> is Relation-like Function-like set

<:(e * y),y:> * x is Relation-like z -valued Function-like set

(id z) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(z,A,x,(e * y),((id z) * y)) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

<:(e * y),((id z) * y):> is Relation-like Function-like set

<:(e * y),((id z) * y):> * x is Relation-like z -valued Function-like set

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]

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

A is non empty set

[:A,z:] is Relation-like non empty set

bool [:A,z:] is non empty set

x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

(z,z,x,(id z),(id z)) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

<:(id z),(id z):> is Relation-like Function-like set

<:(id z),(id z):> * x is Relation-like z -valued Function-like set

y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(z,z,x,(id z),(id z)) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(z,A,x,y,y) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

<:y,y:> is Relation-like Function-like set

<:y,y:> * x is Relation-like z -valued Function-like set

(id z) * y is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

(z,A,x,((id z) * y),((id z) * y)) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

<:((id z) * y),((id z) * y):> is Relation-like Function-like set

<:((id z) * y),((id z) * y):> * x is Relation-like z -valued Function-like set

(z,A,x,((id z) * y),y) is Relation-like A -defined z -valued Function-like non empty total V18(A,z) Element of bool [:A,z:]

<:((id z) * y),y:> is Relation-like Function-like set

<:((id z) * y),y:> * x is Relation-like z -valued Function-like set

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

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

id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]

A is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

x is Element of z

y is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

(z,z,A,(id z),y) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

<:(id z),y:> is Relation-like Function-like set

<:(id z),y:> * A is Relation-like z -valued Function-like set

(z,z,A,(id z),y) . x is Element of z

y . x is Element of z

A . (x,(y . x)) is Element of z

[x,(y . x)] is V15() set

{x,(y . x)} is non empty set

{x} is non empty set

{{x,(y . x)},{x}} is non empty set

A . [x,(y . x)] is set

(id z) . x is Element of z

A . (((id z) . x),(y . x)) is Element of z

[((id z) . x),(y . x)] is V15() set

{((id z) . x),(y . x)} is non empty set

{((id z) . x)} is non empty set

{{((id z) . x),(y . x)},{((id z) . x)}} is non empty set

A . [((id z) . x),(y . x)] is set

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

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

id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]

A is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

x is Element of z

y is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

(z,z,A,y,(id z)) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

<:y,(id z):> is Relation-like Function-like set

<:y,(id z):> * A is Relation-like z -valued Function-like set

(z,z,A,y,(id z)) . x is Element of z

y . x is Element of z

A . ((y . x),x) is Element of z

[(y . x),x] is V15() set

{(y . x),x} is non empty set

{(y . x)} is non empty set

{{(y . x),x},{(y . x)}} is non empty set

A . [(y . x),x] is set

(id z) . x is Element of z

A . ((y . x),((id z) . x)) is Element of z

[(y . x),((id z) . x)] is V15() set

{(y . x),((id z) . x)} is non empty set

{{(y . x),((id z) . x)},{(y . x)}} is non empty set

A . [(y . x),((id z) . x)] is set

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

id z is Relation-like z -defined z -valued Function-like one-to-one non empty total V18(z,z) Element of bool [:z,z:]

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

A is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

(z,z,A,(id z),(id z)) is Relation-like z -defined z -valued Function-like non empty total V18(z,z) Element of bool [:z,z:]

<:(id z),(id z):> is Relation-like Function-like set

<:(id z),(id z):> * A is Relation-like z -valued Function-like set

x is Element of z

(z,z,A,(id z),(id z)) . x is Element of z

A . (x,x) is Element of z

[x,x] is V15() set

{x,x} is non empty set

{x} is non empty set

{{x,x},{x}} is non empty set

A . [x,x] is set

(id z) . x is Element of z

A . (((id z) . x),((id z) . x)) is Element of z

[((id z) . x),((id z) . x)] is V15() set

{((id z) . x),((id z) . x)} is non empty set

{((id z) . x)} is non empty set

{{((id z) . x),((id z) . x)},{((id z) . x)}} is non empty set

A . [((id z) . x),((id z) . x)] is set

A . (((id z) . x),x) is Element of z

[((id z) . x),x] is V15() set

{((id z) . x),x} is non empty set

{{((id z) . x),x},{((id z) . x)}} is non empty set

A . [((id z) . x),x] is set

z is set

A is set

[:z,A:] is Relation-like set

bool [:z,A:] is non empty set

x is set

(z,x) is Relation-like Function-like set

{x} is non empty set

[:z,{x}:] is Relation-like set

proj2 (z,x) is set

proj1 (z,x) is set

z is set

A is set

(z,A) is Relation-like Function-like set

{A} is non empty set

[:z,{A}:] is Relation-like set

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

proj1 (z,A) is set

proj2 (z,A) is set

z is non empty set

A is set

x is Element of z

(A,x) is Relation-like Function-like set

{x} is non empty set

[:A,{x}:] is Relation-like set

[:A,z:] is Relation-like set

bool [:A,z:] is non empty set

A is non empty set

z is set

x is Element of A

(A,z,x) is Relation-like z -defined A -valued Function-like total V18(z,A) Element of bool [:z,A:]

[:z,A:] is Relation-like set

bool [:z,A:] is non empty set

{x} is non empty set

[:z,{x}:] is Relation-like set

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

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

A is set

[:A,z:] is Relation-like set

bool [:A,z:] is non empty set

x is Relation-like [:z,z:] -defined z -valued Function-like non empty total V18([:z,z:],z) Element of bool [:[:z,z:],z:]

y is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]

e is Element of z

(x,y,e) is Relation-like Function-like set

proj1 y is set

((proj1 y),e) is Relation-like Function-like set

{e} is non empty set

[:(proj1 y),{e}:] is Relation-like set

<:y,((proj1 y),e):> is Relation-like Function-like set

<:y,((proj1 y),e):> * x is Relation-like z -valued Function-like set

dom y is Element of bool A

bool A is non empty set

(z,(dom y),e) is Relation-like dom y -defined z -valued Function-like total V18( dom y,z) Element of bool [:(dom y),z:]

[:(dom y),z:] is Relation-like set

bool [:(dom y),z:] is non empty set

[:(dom y),{e}:] is Relation-like set

g is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]

<:y,g:> is Relation-like A -defined [:z,z:] -valued Function-like total V18(A,[:z,z:]) Element of bool [:A,[:z,z:]:]

[:A,[:z,z:]:] is Relation-like set

bool [:A,[:z,z:]:] is non empty set

x * <:y,g:> is Relation-like A -defined z -valued Function-like total V18(A,z) Element of bool [:A,z:]

z is non empty set

[:z,z:] is Relation-like non empty set

[:[:z,z:],z:] is Relation-like non empty set

bool [:[: