{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
dom {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
rng {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set
A is set
id A is Relation-like A -defined A -valued Function-like one-to-one set
b is set
id b is Relation-like b -defined b -valued Function-like one-to-one set
(id b) | A is Relation-like A -defined b -defined b -valued Function-like set
b /\ A is set
id (b /\ A) is Relation-like b /\ A -defined b /\ A -valued Function-like one-to-one set
(id A) * (id b) is Relation-like A -defined b -valued Function-like one-to-one set
A is set
b is Relation-like Function-like set
a is Relation-like Function-like set
b * a is Relation-like Function-like set
dom (b * a) is set
b .: A is set
dom a is set
z2 is set
dom b is set
x1 is set
b . x1 is set
A is set
b is Relation-like Function-like set
dom b is set
b .: A is set
a is Relation-like Function-like set
dom a is set
b * a is Relation-like Function-like set
dom (b * a) is set
z2 is set
b . z2 is set
A is set
b is Relation-like Function-like set
a is Relation-like Function-like set
b * a is Relation-like Function-like set
rng (b * a) is set
a " A is set
rng b is set
z2 is set
dom a is set
a . z2 is set
dom (b * a) is set
x1 is set
(b * a) . x1 is set
dom b is set
b . x1 is set
a . (b . x1) is set
A is set
a is Relation-like Function-like set
rng a is set
a " A is set
b is Relation-like Function-like set
rng b is set
b * a is Relation-like Function-like set
rng (b * a) is set
z2 is set
dom a is set
x1 is set
a . x1 is set
dom b is set
y1 is set
b . y1 is set
dom (b * a) is set
(b * a) . y1 is set
F1() is set
F2() is set
[:F1(),F2():] is Relation-like set
b is set
a is set
z2 is set
[a,z2] is set
{a,z2} is non empty set
{a} is non empty set
{{a,z2},{a}} is non empty set
x1 is set
y1 is set
x2 is set
[y1,x2] is set
{y1,x2} is non empty set
{y1} is non empty set
{{y1,x2},{y1}} is non empty set
b is set
a is set
z2 is set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
b is Relation-like Function-like set
dom b is set
a is set
z2 is set
b . (a,z2) is set
[a,z2] is set
{a,z2} is non empty set
{a} is non empty set
{{a,z2},{a}} is non empty set
b . [a,z2] is set
F1() is set
F2() is set
[:F1(),F2():] is Relation-like set
A is set
b is set
F3(A,b) is set
A is set
b is set
a is set
F3(A,b) is set
z2 is set
A is Relation-like Function-like set
dom A is set
A is set
b is set
[:A,b:] is Relation-like set
a is Relation-like Function-like set
dom a is set
z2 is Relation-like Function-like set
dom z2 is set
x1 is set
a . x1 is set
z2 . x1 is set
y1 is set
x2 is set
[y1,x2] is set
{y1,x2} is non empty set
{y1} is non empty set
{{y1,x2},{y1}} is non empty set
a . (y1,x2) is set
a . [y1,x2] is set
z2 . (y1,x2) is set
z2 . [y1,x2] is set
A is Relation-like Function-like set
dom A is set
bool (dom A) is non empty set
b is set
A .: b is set
a is set
A .: a is set
b is set
a is set
z2 is set
A .: b is set
b is Relation-like Function-like set
dom b is set
a is set
b . a is set
A .: a is set
b is Relation-like Function-like set
dom b is set
a is Relation-like Function-like set
dom a is set
z2 is set
b . z2 is set
a . z2 is set
A .: z2 is set
A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
dom (b) is set
(b) . A is set
b .: A is set
dom b is set
bool (dom b) is non empty set
A is Relation-like Function-like set
(A) is Relation-like Function-like set
(A) . {} is set
dom A is set
A .: {} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
A is Relation-like Function-like set
(A) is Relation-like Function-like set
rng (A) is set
rng A is set
bool (rng A) is non empty set
b is set
dom (A) is set
a is set
(A) . a is set
A .: a is set
A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) .: A is set
rng b is set
bool (rng b) is non empty set
rng (b) is set
A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) " A is set
dom b is set
bool (dom b) is non empty set
dom (b) is set
A is set
bool A is non empty set
b is set
a is non empty set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
z2 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(z2) is Relation-like Function-like set
(z2) " b is set
dom z2 is Element of bool A
A is set
union A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) .: A is set
union ((b) .: A) is set
b .: (union A) is set
a is set
z2 is set
dom (b) is set
x1 is set
(b) . x1 is set
b .: x1 is set
dom b is set
y1 is set
b . y1 is set
A is set
union A is set
b is Relation-like Function-like set
dom b is set
bool (dom b) is non empty set
b .: (union A) is set
(b) is Relation-like Function-like set
(b) .: A is set
union ((b) .: A) is set
a is set
z2 is set
b . z2 is set
x1 is set
dom (b) is set
(b) . x1 is set
b .: x1 is set
A is set
bool A is non empty set
b is set
union b is set
a is non empty set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
z2 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
z2 .: (union b) is set
(z2) is Relation-like Function-like set
(z2) .: b is set
union ((z2) .: b) is set
dom z2 is Element of bool A
A is set
union A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) " A is set
union ((b) " A) is set
b " (union A) is set
a is set
z2 is set
dom (b) is set
dom b is set
bool (dom b) is non empty set
b . a is set
b .: z2 is set
(b) . z2 is set
A is set
union A is set
b is Relation-like Function-like set
rng b is set
bool (rng b) is non empty set
b " (union A) is set
(b) is Relation-like Function-like set
(b) " A is set
union ((b) " A) is set
a is set
b . a is set
z2 is set
b " z2 is set
dom b is set
bool (dom b) is non empty set
dom (b) is set
b .: (b " z2) is set
(b) . (b " z2) is set
A is Relation-like Function-like set
b is Relation-like Function-like set
A * b is Relation-like Function-like set
((A * b)) is Relation-like Function-like set
(A) is Relation-like Function-like set
(b) is Relation-like Function-like set
(A) * (b) is Relation-like Function-like set
dom ((A * b)) is set
dom ((A) * (b)) is set
a is set
dom (A * b) is set
bool (dom (A * b)) is non empty set
dom A is set
bool (dom A) is non empty set
dom (A) is set
A .: a is set
dom b is set
bool (dom b) is non empty set
dom (b) is set
(A) . a is set
dom (A) is set
(A) . a is set
dom (b) is set
A .: a is set
dom b is set
bool (dom b) is non empty set
dom A is set
bool (dom A) is non empty set
dom (A * b) is set
bool (dom (A * b)) is non empty set
a is set
((A * b)) . a is set
((A) * (b)) . a is set
dom (A * b) is set
bool (dom (A * b)) is non empty set
A .: a is set
dom b is set
dom A is set
bool (dom A) is non empty set
dom (A) is set
(A * b) .: a is set
b .: (A .: a) is set
(b) . (A .: a) is set
(A) . a is set
(b) . ((A) . a) is set
A is Relation-like Function-like set
(A) is Relation-like Function-like set
dom A is set
bool (dom A) is non empty set
rng A is set
bool (rng A) is non empty set
[:(bool (dom A)),(bool (rng A)):] is Relation-like non empty set
bool [:(bool (dom A)),(bool (rng A)):] is non empty set
dom (A) is set
rng (A) is set
A is set
bool A is non empty set
b is set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
bool b is non empty set
[:(bool A),(bool b):] is Relation-like non empty set
bool [:(bool A),(bool b):] is non empty set
a is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
(a) is Relation-like Function-like set
dom a is Element of bool A
rng a is set
bool (rng a) is non empty set
bool (dom a) is non empty set
[:(bool (dom a)),(bool (rng a)):] is Relation-like non empty set
bool [:(bool (dom a)),(bool (rng a)):] is non empty set
rng (a) is set
dom (a) is set
A is set
b is non empty set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
(a) is Relation-like Function-like set
bool A is non empty set
bool b is non empty set
[:(bool A),(bool b):] is Relation-like non empty set
bool [:(bool A),(bool b):] is non empty set
A is Relation-like Function-like set
rng A is set
bool (rng A) is non empty set
b is set
A " b is set
a is set
A " a is set
b is set
a is set
z2 is set
A " b is set
b is Relation-like Function-like set
dom b is set
a is set
b . a is set
A " a is set
b is Relation-like Function-like set
dom b is set
a is Relation-like Function-like set
dom a is set
z2 is set
b . z2 is set
a . z2 is set
A " z2 is set
A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
dom (b) is set
(b) . A is set
b " A is set
rng b is set
bool (rng b) is non empty set
A is Relation-like Function-like set
(A) is Relation-like Function-like set
rng (A) is set
dom A is set
bool (dom A) is non empty set
b is set
dom (A) is set
a is set
(A) . a is set
A " a is set
A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) .: A is set
dom b is set
bool (dom b) is non empty set
rng (b) is set
A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) " A is set
rng b is set
bool (rng b) is non empty set
dom (b) is set
A is set
union A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) .: A is set
union ((b) .: A) is set
b " (union A) is set
a is set
z2 is set
dom (b) is set
x1 is set
(b) . x1 is set
b " x1 is set
rng b is set
bool (rng b) is non empty set
b .: z2 is set
dom b is set
b . a is set
A is set
union A is set
b is Relation-like Function-like set
rng b is set
bool (rng b) is non empty set
(b) is Relation-like Function-like set
(b) .: A is set
union ((b) .: A) is set
b " (union A) is set
a is set
b . a is set
z2 is set
dom b is set
b " z2 is set
dom (b) is set
(b) . z2 is set
A is set
union A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) " A is set
union ((b) " A) is set
b .: (union A) is set
a is set
z2 is set
dom (b) is set
rng b is set
bool (rng b) is non empty set
dom b is set
x1 is set
b . x1 is set
(b) . z2 is set
b " z2 is set
A is set
union A is set
b is Relation-like Function-like set
dom b is set
bool (dom b) is non empty set
(b) is Relation-like Function-like set
(b) " A is set
union ((b) " A) is set
b .: (union A) is set
a is set
z2 is set
b . z2 is set
x1 is set
b .: x1 is set
b " (b .: x1) is set
rng b is set
bool (rng b) is non empty set
dom (b) is set
(b) . (b .: x1) is set
A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) .: A is set
(b) is Relation-like Function-like set
(b) " A is set
a is set
dom (b) is set
z2 is set
(b) . z2 is set
b " z2 is set
dom b is set
bool (dom b) is non empty set
dom (b) is set
rng b is set
bool (rng b) is non empty set
b .: a is set
(b) . a is set
A is set
b is Relation-like Function-like set
(b) is Relation-like Function-like set
(b) .: A is set
(b) is Relation-like Function-like set
(b) " A is set
a is set
b .: a is set
rng b is set
bool (rng b) is non empty set
dom (b) is set
dom (b) is set
dom b is set
bool (dom b) is non empty set
b " (b .: a) is set
(b) . (b .: a) is set
(b) . a is set
A is Relation-like Function-like set
dom A is set
bool (dom A) is non empty set
(A) is Relation-like Function-like set
(A) is Relation-like Function-like set
b is set
(A) " b is set
(A) .: b is set
a is set
(A) . a is set
dom (A) is set
rng A is set
bool (rng A) is non empty set
A " a is set
dom (A) is set
A .: (A " a) is set
(A) . (A " a) is set
A is Relation-like Function-like set
(A) is Relation-like Function-like set
(A) is Relation-like Function-like set
b is set
(A) .: b is set
(A) " b is set
a is set
dom (A) is set
z2 is set
(A) . z2 is set
dom A is set
bool (dom A) is non empty set
A .: z2 is set
A " a is set
rng A is set
bool (rng A) is non empty set
dom (A) is set
(A) . a is set
A is Relation-like Function-like set
dom A is set
bool (dom A) is non empty set
(A) is Relation-like Function-like set
(A) is Relation-like Function-like set
b is set
(A) " b is set
(A) .: b is set
b is Relation-like Function-like set
A is Relation-like Function-like set
A * b is Relation-like Function-like set
((A * b)) is Relation-like Function-like set
(b) is Relation-like Function-like set
(A) is Relation-like Function-like set
(b) * (A) is Relation-like Function-like set
dom ((A * b)) is set
dom ((b) * (A)) is set
a is set
rng (A * b) is set
bool (rng (A * b)) is non empty set
rng b is set
bool (rng b) is non empty set
dom (b) is set
b " a is set
rng A is set
bool (rng A) is non empty set
dom (A) is set
(b) . a is set
dom (b) is set
(b) . a is set
dom (A) is set
b " a is set
rng A is set
bool (rng A) is non empty set
rng b is set
bool (rng b) is non empty set
rng (A * b) is set
bool (rng (A * b)) is non empty set
a is set
((A * b)) . a is set
((b) * (A)) . a is set
rng (A * b) is set
bool (rng (A * b)) is non empty set
b " a is set
rng A is set
rng b is set
bool (rng b) is non empty set
dom (b) is set
(A * b) " a is set
A " (b " a) is set
(A) . (b " a) is set
(b) . a is set
(A) . ((b) . a) is set
A is Relation-like Function-like set
(A) is Relation-like Function-like set
rng A is set
bool (rng A) is non empty set
dom A is set
bool (dom A) is non empty set
[:(bool (rng A)),(bool (dom A)):] is Relation-like non empty set
bool [:(bool (rng A)),(bool (dom A)):] is non empty set
dom (A) is set
rng (A) is set
b is set
A is set
1 is non empty set
a is set
z2 is set
a is set
z2 is set
x1 is set
a is Relation-like Function-like set
dom a is set
a is Relation-like Function-like set
dom a is set
z2 is Relation-like Function-like set
dom z2 is set
x1 is set
a . x1 is set
z2 . x1 is set
A is set
b is set
a is set
(b,a) is Relation-like Function-like set
(b,a) . A is set
dom (b,a) is set
A is set
b is set
a is set
b \ a is Element of bool b
bool b is non empty set
(a,b) is Relation-like Function-like set
(a,b) . A is set
A is set
b is set
(A,b) is Relation-like Function-like set
a is set
(a,b) is Relation-like Function-like set
z2 is set
(A,b) . z2 is set
(a,b) . z2 is set
{{},1} is non empty set
A is set
b is set
(A,b) is Relation-like Function-like set
rng (A,b) is set
a is set
dom (A,b) is set
z2 is set
(A,b) . z2 is set
{1} is non empty set
A is set
[:A,{{},1}:] is Relation-like set
bool [:A,{{},1}:] is non empty set
b is Relation-like A -defined {{},1} -valued Function-like quasi_total Element of bool [:A,{{},1}:]
b " {1} is set
((b " {1}),A) is Relation-like Function-like set
dom b is Element of bool A
bool A is non empty set
a is set
b . a is set
rng b is set
A is set
b is set
(A,b) is Relation-like Function-like set
[:b,{{},1}:] is Relation-like set
bool [:b,{{},1}:] is non empty set
dom (A,b) is set
rng (A,b) is set
A is set
bool A is non empty set
A is set
bool A is non empty set
b is Element of bool A
id b is Relation-like b -defined b -valued Function-like one-to-one set
[:b,A:] is Relation-like set
bool [:b,A:] is non empty set
rng (id b) is set
dom (id b) is Element of bool b
bool b is non empty set
A is set
bool A is non empty set
b is Element of bool A
(A,b) is Relation-like b -defined A -valued b -valued Function-like one-to-one quasi_total Element of bool [:b,A:]
[:b,A:] is Relation-like set
bool [:b,A:] is non empty set
id A is Relation-like A -defined A -valued Function-like one-to-one set
(id A) | b is Relation-like b -defined A -defined A -valued Function-like set
A is set
b is set
bool b is non empty set
a is Element of bool b
(b,a) is Relation-like a -defined b -valued a -valued Function-like one-to-one quasi_total Element of bool [:a,b:]
[:a,b:] is Relation-like set
bool [:a,b:] is non empty set
(b,a) . A is set
dom (b,a) is Element of bool a
bool a is non empty set
rng (b,a) is set
A is set
b is set
[:A,b:] is Relation-like set
a is Relation-like Function-like set
dom a is set
a is Relation-like Function-like set
dom a is set
z2 is Relation-like Function-like set
dom z2 is set
x1 is set
y1 is set
a . (x1,y1) is set
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
a . [x1,y1] is set
z2 . (x1,y1) is set
z2 . [x1,y1] is set
a is Relation-like Function-like set
dom a is set
a is Relation-like Function-like set
dom a is set
z2 is Relation-like Function-like set
dom z2 is set
x1 is set
y1 is set
a . (x1,y1) is set
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
a . [x1,y1] is set
z2 . (x1,y1) is set
z2 . [x1,y1] is set
A is set
b is set
(A,b) is Relation-like Function-like set
rng (A,b) is set
a is set
dom (A,b) is set
z2 is set
(A,b) . z2 is set
[:A,b:] is Relation-like set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
(A,b) . (x1,y1) is set
(A,b) . [x1,y1] is set
A is set
b is set
(b,A) is Relation-like Function-like set
rng (b,A) is set
the Element of A is Element of A
z2 is set
[z2, the Element of A] is set
{z2, the Element of A} is non empty set
{z2} is non empty set
{{z2, the Element of A},{z2}} is non empty set
[:b,A:] is Relation-like set
dom (b,A) is set
(b,A) . (z2, the Element of A) is set
(b,A) . [z2, the Element of A] is set
A is set
b is set
(A,b) is Relation-like Function-like set
rng (A,b) is set
a is set
dom (A,b) is set
z2 is set
(A,b) . z2 is set
[:A,b:] is Relation-like set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
(A,b) . (x1,y1) is set
(A,b) . [x1,y1] is set
A is set
b is set
(A,b) is Relation-like Function-like set
rng (A,b) is set
the Element of A is Element of A
z2 is set
[ the Element of A,z2] is set
{ the Element of A,z2} is non empty set
{ the Element of A} is non empty set
{{ the Element of A,z2},{ the Element of A}} is non empty set
[:A,b:] is Relation-like set
dom (A,b) is set
(A,b) . ( the Element of A,z2) is set
(A,b) . [ the Element of A,z2] is set
A is set
b is set
(A,b) is Relation-like Function-like set
[:A,b:] is Relation-like set
[:[:A,b:],A:] is Relation-like set
bool [:[:A,b:],A:] is non empty set
dom (A,b) is set
rng (A,b) is set
(A,b) is Relation-like Function-like set
[:[:A,b:],b:] is Relation-like set
bool [:[:A,b:],b:] is non empty set
dom (A,b) is set
rng (A,b) is set
A is set
b is Relation-like Function-like set
dom b is set
b is Relation-like Function-like set
dom b is set
a is Relation-like Function-like set
dom a is set
z2 is set
b . z2 is set
a . z2 is set
[z2,z2] is set
{z2,z2} is non empty set
{z2} is non empty set
{{z2,z2},{z2}} is non empty set
A is set
(A) is Relation-like Function-like set
rng (A) is set
[:A,A:] is Relation-like set
b is set
dom (A) is set
a is set
(A) . a is set
[a,a] is set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
A is set
(A) is Relation-like Function-like set
[:A,A:] is Relation-like set
[:A,[:A,A:]:] is Relation-like set
bool [:A,[:A,A:]:] is non empty set
dom (A) is set
rng (A) is set
A is Relation-like Function-like set
dom A is set
b is Relation-like Function-like set
dom b is set
(dom A) /\ (dom b) is set
a is Relation-like Function-like set
dom a is set
a is Relation-like Function-like set
dom a is set
z2 is Relation-like Function-like set
dom z2 is set
x1 is set
a . x1 is set
z2 . x1 is set
A . x1 is set
b . x1 is set
[(A . x1),(b . x1)] is set
{(A . x1),(b . x1)} is non empty set
{(A . x1)} is non empty set
{{(A . x1),(b . x1)},{(A . x1)}} is non empty set
A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
b is Relation-like Function-like set
(A,b) is Relation-like Function-like set
dom A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
dom (A,b) is set
dom b is set
{} /\ (dom b) is Relation-like set
(b,A) is Relation-like Function-like set
dom A is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
dom (b,A) is set
dom b is set
{} /\ (dom b) is Relation-like set
A is set
b is Relation-like Function-like set
dom b is set
a is Relation-like Function-like set
dom a is set
(dom b) /\ (dom a) is set
(b,a) is Relation-like Function-like set
(b,a) . A is set
b . A is set
a . A is set
[(b . A),(a . A)] is set
{(b . A),(a . A)} is non empty set
{(b . A)} is non empty set
{{(b . A),(a . A)},{(b . A)}} is non empty set
dom (b,a) is set
A is set
b is set
a is Relation-like Function-like set
dom a is set
z2 is Relation-like Function-like set
dom z2 is set
(a,z2) is Relation-like Function-like set
(a,z2) . A is set
a . A is set
z2 . A is set
[(a . A),(z2 . A)] is set
{(a . A),(z2 . A)} is non empty set
{(a . A)} is non empty set
{{(a . A),(z2 . A)},{(a . A)}} is non empty set
(dom a) /\ (dom z2) is set
dom (a,z2) is set
A is set
b is Relation-like Function-like set
dom b is set
a is Relation-like Function-like set
dom a is set
(b,a) is Relation-like Function-like set
dom (b,a) is set
(dom b) /\ (dom a) is set
A is Relation-like Function-like set
b is Relation-like Function-like set
(A,b) is Relation-like Function-like set
rng (A,b) is set
rng A is set
rng b is set
[:(rng A),(rng b):] is Relation-like set
a is set
dom (A,b) is set
z2 is set
(A,b) . z2 is set
dom A is set
dom b is set
(dom A) /\ (dom b) is set
A . z2 is set
b . z2 is set
[(A . z2),(b . z2)] is set
{(A . z2),(b . z2)} is non empty set
{(A . z2)} is non empty set
{{(A . z2),(b . z2)},{(A . z2)}} is non empty set
A is set
b is set
(A,b) is Relation-like [:A,b:] -defined A -valued Function-like quasi_total Element of bool [:[:A,b:],A:]
[:A,b:] is Relation-like set
[:[:A,b:],A:] is Relation-like set
bool [:[:A,b:],A:] is non empty set
(A,b) is Relation-like [:A,b:] -defined b -valued Function-like quasi_total Element of bool [:[:A,b:],b:]
[:[:A,b:],b:] is Relation-like set
bool [:[:A,b:],b:] is non empty set
a is Relation-like Function-like set
dom a is set
z2 is Relation-like Function-like set
dom z2 is set
rng a is set
rng z2 is set
(a,z2) is Relation-like Function-like set
(a,z2) * (A,b) is Relation-like A -valued Function-like set
(a,z2) * (A,b) is Relation-like b -valued Function-like set
[:(rng a),(rng z2):] is Relation-like set
rng (a,z2) is set
dom (A,b) is Relation-like A -defined b -valued Element of bool [:A,b:]
bool [:A,b:] is non empty set
dom ((a,z2) * (A,b)) is set
dom (a,z2) is set
x1 is set
((a,z2) * (A,b)) . x1 is set
a . x1 is set
z2 . x1 is set
(a,z2) . x1 is set
(A,b) . ((a,z2) . x1) is set
(A,b) . ((a . x1),(z2 . x1)) is set
[(a . x1),(z2 . x1)] is set
{(a . x1),(z2 . x1)} is non empty set
{(a . x1)} is non empty set
{{(a . x1),(z2 . x1)},{(a . x1)}} is non empty set
(A,b) . [(a . x1),(z2 . x1)] is set
dom (A,b) is Relation-like A -defined b -valued Element of bool [:A,b:]
dom ((a,z2) * (A,b)) is set
x1 is set
((a,z2) * (A,b)) . x1 is set
z2 . x1 is set
a . x1 is set
(a,z2) . x1 is set
(A,b) . ((a,z2) . x1) is set
(A,b) . ((a . x1),(z2 . x1)) is set
[(a . x1),(z2 . x1)] is set
{(a . x1),(z2 . x1)} is non empty set
{(a . x1)} is non empty set
{{(a . x1),(z2 . x1)},{(a . x1)}} is non empty set
(A,b) . [(a . x1),(z2 . x1)] is set
A is set
b is set
(A,b) is Relation-like [:A,b:] -defined A -valued Function-like quasi_total Element of bool [:[:A,b:],A:]
[:A,b:] is Relation-like set
[:[:A,b:],A:] is Relation-like set
bool [:[:A,b:],A:] is non empty set
(A,b) is Relation-like [:A,b:] -defined b -valued Function-like quasi_total Element of bool [:[:A,b:],b:]
[:[:A,b:],b:] is Relation-like set
bool [:[:A,b:],b:] is non empty set
((A,b),(A,b)) is Relation-like Function-like set
id [:A,b:] is Relation-like [:A,b:] -defined [:A,b:] -valued Function-like one-to-one set
dom (A,b) is Relation-like A -defined b -valued Element of bool [:A,b:]
bool [:A,b:] is non empty set
dom (A,b) is Relation-like A -defined b -valued Element of bool [:A,b:]
dom ((A,b),(A,b)) is set
a is set
z2 is set
((A,b),(A,b)) . (a,z2) is set
[a,z2] is set
{a,z2} is non empty set
{a} is non empty set
{{a,z2},{a}} is non empty set
((A,b),(A,b)) . [a,z2] is set
(id [:A,b:]) . (a,z2) is set
(id [:A,b:]) . [a,z2] is set
(A,b) . (a,z2) is set
(A,b) . [a,z2] is set
(A,b) . (a,z2) is set
(A,b) . [a,z2] is set
[((A,b) . (a,z2)),((A,b) . (a,z2))] is set
{((A,b) . (a,z2)),((A,b) . (a,z2))} is non empty set
{((A,b) . (a,z2))} is non empty set
{{((A,b) . (a,z2)),((A,b) . (a,z2))},{((A,b) . (a,z2))}} is non empty set
[a,((A,b) . (a,z2))] is set
{a,((A,b) . (a,z2))} is non empty set
{{a,((A,b) . (a,z2))},{a}} is non empty set
dom (id [:A,b:]) is Relation-like A -defined b -valued Element of bool [:A,b:]
A is Relation-like Function-like set
dom A is set
b is Relation-like Function-like set
dom b is set
z2 is Relation-like Function-like set
dom z2 is set
a is Relation-like Function-like set
dom a is set
(A,b) is Relation-like Function-like set
(z2,a) is Relation-like Function-like set
dom (A,b) is set
x1 is set
A . x1 is set
z2 . x1 is set
(A,b) . x1 is set
b . x1 is set
[(A . x1),(b . x1)] is set
{(A . x1),(b . x1)} is non empty set
{(A . x1)} is non empty set
{{(A . x1),(b . x1)},{(A . x1)}} is non empty set
(z2,a) . x1 is set
a . x1 is set
[(z2 . x1),(a . x1)] is set
{(z2 . x1),(a . x1)} is non empty set
{(z2 . x1)} is non empty set
{{(z2 . x1),(a . x1)},{(z2 . x1)}} is non empty set
x1 is set
b . x1 is set
a . x1 is set
(A,b) . x1 is set
A . x1 is set
[(A . x1),(b . x1)] is set
{(A . x1),(b . x1)} is non empty set
{(A . x1)} is non empty set
{{(A . x1),(b . x1)},{(A . x1)}} is non empty set
(z2,a) . x1 is set
z2 . x1 is set
[(z2 . x1),(a . x1)] is set
{(z2 . x1),(a . x1)} is non empty set
{(z2 . x1)} is non empty set
{{(z2 . x1),(a . x1)},{(z2 . x1)}} is non empty set
a is Relation-like Function-like set
A is Relation-like Function-like set
a * A is Relation-like Function-like set
b is Relation-like Function-like set
a * b is Relation-like Function-like set
((a * A),(a * b)) is Relation-like Function-like set
(A,b) is Relation-like Function-like set
a * (A,b) is Relation-like Function-like set
dom ((a * A),(a * b)) is set
dom (a * (A,b)) is set
z2 is set
dom (a * A) is set
dom (a * b) is set
(dom (a * A)) /\ (dom (a * b)) is set
a . z2 is set
dom b is set
dom A is set
(dom A) /\ (dom b) is set
dom (A,b) is set
dom a is set
dom a is set
a . z2 is set
dom (A,b) is set
dom A is set
dom b is set
(dom A) /\ (dom b) is set
dom (a * b) is set
dom (a * A) is set
(dom (a * A)) /\ (dom (a * b)) is set
z2 is set
((a * A),(a * b)) . z2 is set
(a * (A,b)) . z2 is set
dom (a * A) is set
dom (a * b) is set
(dom (a * A)) /\ (dom (a * b)) is set
dom a is set
a . z2 is set
dom b is set
dom A is set
(dom A) /\ (dom b) is set
(a * A) . z2 is set
(a * b) . z2 is set
[((a * A) . z2),((a * b) . z2)] is set
{((a * A) . z2),((a * b) . z2)} is non empty set
{((a * A) . z2)} is non empty set
{{((a * A) . z2),((a * b) . z2)},{((a * A) . z2)}} is non empty set
A . (a . z2) is set
[(A . (a . z2)),((a * b) . z2)] is set
{(A . (a . z2)),((a * b) . z2)} is non empty set
{(A . (a . z2))} is non empty set
{{(A . (a . z2)),((a * b) . z2)},{(A . (a . z2))}} is non empty set
b . (a . z2) is set
[(A . (a . z2)),(b . (a . z2))] is set
{(A . (a . z2)),(b . (a . z2))} is non empty set
{{(A . (a . z2)),(b . (a . z2))},{(A . (a . z2))}} is non empty set
(A,b) . (a . z2) is set
A is set
b is Relation-like Function-like set
a is Relation-like Function-like set
(b,a) is Relation-like Function-like set
(b,a) .: A is set
b .: A is set
a .: A is set
[:(b .: A),(a .: A):] is Relation-like set
z2 is set
dom (b,a) is set
x1 is set
(b,a) . x1 is set
dom b is set
dom a is set
(dom b) /\ (dom a) is set
b . x1 is set
a . x1 is set
[(b . x1),(a . x1)] is set
{(b . x1),(a . x1)} is non empty set
{(b . x1)} is non empty set
{{(b . x1),(a . x1)},{(b . x1)}} is non empty set
A is set
b is non empty set
[:A,b:] is Relation-like set
a is Relation-like Function-like set
z2 is Relation-like Function-like set
(a,z2) is Relation-like Function-like set
(a,z2) " [:A,b:] is set
a " A is set
z2 " b is set
(a " A) /\ (z2 " b) is set
x1 is set
(a,z2) . x1 is set
y1 is set
x2 is set
[y1,x2] is set
{y1,x2} is non empty set
{y1} is non empty set
{{y1,x2},{y1}} is non empty set
dom (a,z2) is set
dom a is set
dom z2 is set
(dom a) /\ (dom z2) is set
a . x1 is set
z2 . x1 is set
[(a . x1),(z2 . x1)] is set
{(a . x1),(z2 . x1)} is non empty set
{(a . x1)} is non empty set
{{(a . x1),(z2 . x1)},{(a . x1)}} is non empty set
dom z2 is set
dom a is set
(dom a) /\ (dom z2) is set
dom (a,z2) is set
z2 . x1 is set
a . x1 is set
[(a . x1),(z2 . x1)] is set
{(a . x1),(z2 . x1)} is non empty set
{(a . x1)} is non empty set
{{(a . x1),(z2 . x1)},{(a . x1)}} is non empty set
(a,z2) . x1 is set
A is set
b is set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
[:b,a:] is Relation-like set
[:A,[:b,a:]:] is Relation-like set
bool [:A,[:b,a:]:] is non empty set
z2 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
x1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(z2,x1) is Relation-like Function-like set
rng z2 is set
rng x1 is set
[:(rng z2),(rng x1):] is Relation-like set
dom z2 is Element of bool A
bool A is non empty set
dom x1 is Element of bool A
dom (z2,x1) is set
rng (z2,x1) is set
A is set
b is non empty set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is non empty set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
z2 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
x1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(z2,x1) is Relation-like Function-like set
[:b,a:] is Relation-like non empty set
[:A,[:b,a:]:] is Relation-like set
bool [:A,[:b,a:]:] is non empty set
A is non empty set
b is non empty set
[:A,b:] is Relation-like non empty set
bool [:A,b:] is non empty set
a is non empty set
[:A,a:] is Relation-like non empty set
bool [:A,a:] is non empty set
[:b,a:] is Relation-like non empty set
z2 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
x1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(A,b,a,z2,x1) is Relation-like A -defined [:b,a:] -valued Function-like quasi_total Element of bool [:A,[:b,a:]:]
[:A,[:b,a:]:] is Relation-like non empty set
bool [:A,[:b,a:]:] is non empty set
y1 is Element of A
(A,b,a,z2,x1) . y1 is Element of [:b,a:]
z2 . y1 is Element of b
x1 . y1 is Element of a
[(z2 . y1),(x1 . y1)] is set
{(z2 . y1),(x1 . y1)} is non empty set
{(z2 . y1)} is non empty set
{{(z2 . y1),(x1 . y1)},{(z2 . y1)}} is non empty set
dom z2 is Element of bool A
bool A is non empty set
dom x1 is Element of bool A
A is set
b is set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
[:b,a:] is Relation-like set
z2 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
x1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(z2,x1) is Relation-like Function-like set
rng (z2,x1) is set
rng z2 is set
rng x1 is set
[:(rng z2),(rng x1):] is Relation-like set
A is set
b is set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
(b,a) is Relation-like [:b,a:] -defined b -valued Function-like quasi_total Element of bool [:[:b,a:],b:]
[:b,a:] is Relation-like set
[:[:b,a:],b:] is Relation-like set
bool [:[:b,a:],b:] is non empty set
(b,a) is Relation-like [:b,a:] -defined a -valued Function-like quasi_total Element of bool [:[:b,a:],a:]
[:[:b,a:],a:] is Relation-like set
bool [:[:b,a:],a:] is non empty set
z2 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
x1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(z2,x1) is Relation-like Function-like set
(z2,x1) * (b,a) is Relation-like b -valued Function-like set
(z2,x1) * (b,a) is Relation-like a -valued Function-like set
dom z2 is Element of bool A
bool A is non empty set
dom x1 is Element of bool A
rng z2 is set
rng x1 is set
A is set
b is non empty set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is non empty set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
y1 is set
x2 is non empty set
[:y1,x2:] is Relation-like set
bool [:y1,x2:] is non empty set
y2 is non empty set
[:y1,y2:] is Relation-like set
bool [:y1,y2:] is non empty set
z2 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
x1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(A,b,a,z2,x1) is Relation-like A -defined [:b,a:] -valued Function-like quasi_total Element of bool [:A,[:b,a:]:]
[:b,a:] is Relation-like non empty set
[:A,[:b,a:]:] is Relation-like set
bool [:A,[:b,a:]:] is non empty set
(b,a) is Relation-like [:b,a:] -defined b -valued Function-like quasi_total Element of bool [:[:b,a:],b:]
[:[:b,a:],b:] is Relation-like non empty set
bool [:[:b,a:],b:] is non empty set
(A,b,a,z2,x1) * (b,a) is Relation-like A -defined b -valued Function-like set
b2 is Relation-like y1 -defined x2 -valued Function-like quasi_total Element of bool [:y1,x2:]
c2 is Relation-like y1 -defined y2 -valued Function-like quasi_total Element of bool [:y1,y2:]
(y1,x2,y2,b2,c2) is Relation-like y1 -defined [:x2,y2:] -valued Function-like quasi_total Element of bool [:y1,[:x2,y2:]:]
[:x2,y2:] is Relation-like non empty set
[:y1,[:x2,y2:]:] is Relation-like set
bool [:y1,[:x2,y2:]:] is non empty set
(x2,y2) is Relation-like [:x2,y2:] -defined y2 -valued Function-like quasi_total Element of bool [:[:x2,y2:],y2:]
[:[:x2,y2:],y2:] is Relation-like non empty set
bool [:[:x2,y2:],y2:] is non empty set
(y1,x2,y2,b2,c2) * (x2,y2) is Relation-like y1 -defined y2 -valued Function-like set
A is set
b is set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
z2 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
x1 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
y1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(z2,y1) is Relation-like Function-like set
x2 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(x1,x2) is Relation-like Function-like set
dom y1 is Element of bool A
bool A is non empty set
dom x2 is Element of bool A
dom z2 is Element of bool A
dom x1 is Element of bool A
A is set
b is non empty set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is non empty set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
[:b,a:] is Relation-like non empty set
z2 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
x1 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
y1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(A,b,a,z2,y1) is Relation-like A -defined [:b,a:] -valued Function-like quasi_total Element of bool [:A,[:b,a:]:]
[:A,[:b,a:]:] is Relation-like set
bool [:A,[:b,a:]:] is non empty set
x2 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(A,b,a,x1,x2) is Relation-like A -defined [:b,a:] -valued Function-like quasi_total Element of bool [:A,[:b,a:]:]
dom y1 is Element of bool A
bool A is non empty set
dom x2 is Element of bool A
dom z2 is Element of bool A
dom x1 is Element of bool A
A is Relation-like Function-like set
dom A is set
b is Relation-like Function-like set
dom b is set
[:(dom A),(dom b):] is Relation-like set
a is Relation-like Function-like set
dom a is set
a is Relation-like Function-like set
dom a is set
z2 is Relation-like Function-like set
dom z2 is set
x1 is set
a . x1 is set
z2 . x1 is set
y1 is set
x2 is set
[y1,x2] is set
{y1,x2} is non empty set
{y1} is non empty set
{{y1,x2},{y1}} is non empty set
a . (y1,x2) is set
a . [y1,x2] is set
A . y1 is set
b . x2 is set
[(A . y1),(b . x2)] is set
{(A . y1),(b . x2)} is non empty set
{(A . y1)} is non empty set
{{(A . y1),(b . x2)},{(A . y1)}} is non empty set
z2 . (y1,x2) is set
z2 . [y1,x2] is set
A is Relation-like Function-like set
dom A is set
b is Relation-like Function-like set
dom b is set
[:(dom A),(dom b):] is Relation-like set
(A,b) is Relation-like Function-like set
a is set
A . a is set
z2 is set
[a,z2] is set
{a,z2} is non empty set
{a} is non empty set
{{a,z2},{a}} is non empty set
(A,b) . (a,z2) is set
(A,b) . [a,z2] is set
b . z2 is set
[(A . a),(b . z2)] is set
{(A . a),(b . z2)} is non empty set
{(A . a)} is non empty set
{{(A . a),(b . z2)},{(A . a)}} is non empty set
A is Relation-like Function-like set
b is Relation-like Function-like set
(A,b) is Relation-like Function-like set
dom A is set
dom b is set
((dom A),(dom b)) is Relation-like [:(dom A),(dom b):] -defined dom A -valued Function-like quasi_total Element of bool [:[:(dom A),(dom b):],(dom A):]
[:(dom A),(dom b):] is Relation-like set
[:[:(dom A),(dom b):],(dom A):] is Relation-like set
bool [:[:(dom A),(dom b):],(dom A):] is non empty set
((dom A),(dom b)) * A is Relation-like [:(dom A),(dom b):] -defined Function-like set
((dom A),(dom b)) is Relation-like [:(dom A),(dom b):] -defined dom b -valued Function-like quasi_total Element of bool [:[:(dom A),(dom b):],(dom b):]
[:[:(dom A),(dom b):],(dom b):] is Relation-like set
bool [:[:(dom A),(dom b):],(dom b):] is non empty set
((dom A),(dom b)) * b is Relation-like [:(dom A),(dom b):] -defined Function-like set
((((dom A),(dom b)) * A),(((dom A),(dom b)) * b)) is Relation-like Function-like set
dom ((dom A),(dom b)) is Relation-like dom A -defined dom b -valued Element of bool [:(dom A),(dom b):]
bool [:(dom A),(dom b):] is non empty set
dom ((dom A),(dom b)) is Relation-like dom A -defined dom b -valued Element of bool [:(dom A),(dom b):]
rng ((dom A),(dom b)) is set
dom (((dom A),(dom b)) * b) is Relation-like dom A -defined dom b -valued Element of bool [:(dom A),(dom b):]
rng ((dom A),(dom b)) is set
dom (((dom A),(dom b)) * A) is Relation-like dom A -defined dom b -valued Element of bool [:(dom A),(dom b):]
dom ((((dom A),(dom b)) * A),(((dom A),(dom b)) * b)) is set
a is set
z2 is set
(A,b) . (a,z2) is set
[a,z2] is set
{a,z2} is non empty set
{a} is non empty set
{{a,z2},{a}} is non empty set
(A,b) . [a,z2] is set
((((dom A),(dom b)) * A),(((dom A),(dom b)) * b)) . (a,z2) is set
((((dom A),(dom b)) * A),(((dom A),(dom b)) * b)) . [a,z2] is set
A . a is set
b . z2 is set
[(A . a),(b . z2)] is set
{(A . a),(b . z2)} is non empty set
{(A . a)} is non empty set
{{(A . a),(b . z2)},{(A . a)}} is non empty set
((dom A),(dom b)) . (a,z2) is set
((dom A),(dom b)) . [a,z2] is set
A . (((dom A),(dom b)) . (a,z2)) is set
[(A . (((dom A),(dom b)) . (a,z2))),(b . z2)] is set
{(A . (((dom A),(dom b)) . (a,z2))),(b . z2)} is non empty set
{(A . (((dom A),(dom b)) . (a,z2)))} is non empty set
{{(A . (((dom A),(dom b)) . (a,z2))),(b . z2)},{(A . (((dom A),(dom b)) . (a,z2)))}} is non empty set
((dom A),(dom b)) . (a,z2) is set
((dom A),(dom b)) . [a,z2] is set
b . (((dom A),(dom b)) . (a,z2)) is set
[(A . (((dom A),(dom b)) . (a,z2))),(b . (((dom A),(dom b)) . (a,z2)))] is set
{(A . (((dom A),(dom b)) . (a,z2))),(b . (((dom A),(dom b)) . (a,z2)))} is non empty set
{{(A . (((dom A),(dom b)) . (a,z2))),(b . (((dom A),(dom b)) . (a,z2)))},{(A . (((dom A),(dom b)) . (a,z2)))}} is non empty set
(((dom A),(dom b)) * A) . (a,z2) is set
(((dom A),(dom b)) * A) . [a,z2] is set
[((((dom A),(dom b)) * A) . (a,z2)),(b . (((dom A),(dom b)) . (a,z2)))] is set
{((((dom A),(dom b)) * A) . (a,z2)),(b . (((dom A),(dom b)) . (a,z2)))} is non empty set
{((((dom A),(dom b)) * A) . (a,z2))} is non empty set
{{((((dom A),(dom b)) * A) . (a,z2)),(b . (((dom A),(dom b)) . (a,z2)))},{((((dom A),(dom b)) * A) . (a,z2))}} is non empty set
(((dom A),(dom b)) * b) . (a,z2) is set
(((dom A),(dom b)) * b) . [a,z2] is set
[((((dom A),(dom b)) * A) . (a,z2)),((((dom A),(dom b)) * b) . (a,z2))] is set
{((((dom A),(dom b)) * A) . (a,z2)),((((dom A),(dom b)) * b) . (a,z2))} is non empty set
{{((((dom A),(dom b)) * A) . (a,z2)),((((dom A),(dom b)) * b) . (a,z2))},{((((dom A),(dom b)) * A) . (a,z2))}} is non empty set
dom (A,b) is set
A is Relation-like Function-like set
b is Relation-like Function-like set
(A,b) is Relation-like Function-like set
rng (A,b) is set
rng A is set
rng b is set
[:(rng A),(rng b):] is Relation-like set
a is set
dom (A,b) is set
dom A is set
dom b is set
[:(dom A),(dom b):] is Relation-like set
z2 is set
(A,b) . z2 is set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
A . x1 is set
b . y1 is set
(A,b) . (x1,y1) is set
(A,b) . [x1,y1] is set
[(A . x1),(b . y1)] is set
{(A . x1),(b . y1)} is non empty set
{(A . x1)} is non empty set
{{(A . x1),(b . y1)},{(A . x1)}} is non empty set
z2 is set
x1 is set
[z2,x1] is set
{z2,x1} is non empty set
{z2} is non empty set
{{z2,x1},{z2}} is non empty set
y1 is set
b . y1 is set
x2 is set
A . x2 is set
[x2,y1] is set
{x2,y1} is non empty set
{x2} is non empty set
{{x2,y1},{x2}} is non empty set
(A,b) . (x2,y1) is set
(A,b) . [x2,y1] is set
A is set
(A) is Relation-like A -defined [:A,A:] -valued Function-like quasi_total Element of bool [:A,[:A,A:]:]
[:A,A:] is Relation-like set
[:A,[:A,A:]:] is Relation-like set
bool [:A,[:A,A:]:] is non empty set
b is Relation-like Function-like set
dom b is set
a is Relation-like Function-like set
dom a is set
(b,a) is Relation-like Function-like set
(b,a) is Relation-like Function-like set
(A) * (b,a) is Relation-like A -defined Function-like set
dom (A) is Element of bool A
bool A is non empty set
rng (A) is Relation-like set
dom (b,a) is set
dom ((A) * (b,a)) is Element of bool A
(dom b) /\ (dom a) is set
dom (b,a) is set
z2 is set
(b,a) . z2 is set
((A) * (b,a)) . z2 is set
b . z2 is set
a . z2 is set
[(b . z2),(a . z2)] is set
{(b . z2),(a . z2)} is non empty set
{(b . z2)} is non empty set
{{(b . z2),(a . z2)},{(b . z2)}} is non empty set
(b,a) . (z2,z2) is set
[z2,z2] is set
{z2,z2} is non empty set
{z2} is non empty set
{{z2,z2},{z2}} is non empty set
(b,a) . [z2,z2] is set
(A) . z2 is set
(b,a) . ((A) . z2) is set
A is set
id A is Relation-like A -defined A -valued Function-like one-to-one set
b is set
id b is Relation-like b -defined b -valued Function-like one-to-one set
((id A),(id b)) is Relation-like Function-like set
[:A,b:] is Relation-like set
id [:A,b:] is Relation-like [:A,b:] -defined [:A,b:] -valued Function-like one-to-one set
(A,b) is Relation-like [:A,b:] -defined A -valued Function-like quasi_total Element of bool [:[:A,b:],A:]
[:[:A,b:],A:] is Relation-like set
bool [:[:A,b:],A:] is non empty set
rng (A,b) is set
(A,b) * (id A) is Relation-like [:A,b:] -defined A -valued Function-like set
(A,b) is Relation-like [:A,b:] -defined b -valued Function-like quasi_total Element of bool [:[:A,b:],b:]
[:[:A,b:],b:] is Relation-like set
bool [:[:A,b:],b:] is non empty set
rng (A,b) is set
(A,b) * (id b) is Relation-like [:A,b:] -defined b -valued Function-like set
dom (id A) is Element of bool A
bool A is non empty set
dom (id b) is Element of bool b
bool b is non empty set
((A,b),(A,b)) is Relation-like Function-like set
b is Relation-like Function-like set
z2 is Relation-like Function-like set
(b,z2) is Relation-like Function-like set
A is Relation-like Function-like set
a is Relation-like Function-like set
(A,a) is Relation-like Function-like set
(b,z2) * (A,a) is Relation-like Function-like set
b * A is Relation-like Function-like set
z2 * a is Relation-like Function-like set
((b * A),(z2 * a)) is Relation-like Function-like set
dom ((b,z2) * (A,a)) is set
dom ((b * A),(z2 * a)) is set
x1 is set
dom (b,z2) is set
dom b is set
dom z2 is set
(dom b) /\ (dom z2) is set
(b,z2) . x1 is set
dom (A,a) is set
b . x1 is set
z2 . x1 is set
[(b . x1),(z2 . x1)] is set
{(b . x1),(z2 . x1)} is non empty set
{(b . x1)} is non empty set
{{(b . x1),(z2 . x1)},{(b . x1)}} is non empty set
dom A is set
dom a is set
[:(dom A),(dom a):] is Relation-like set
dom (z2 * a) is set
dom (b * A) is set
(dom (b * A)) /\ (dom (z2 * a)) is set
dom (b * A) is set
dom (z2 * a) is set
(dom (b * A)) /\ (dom (z2 * a)) is set
dom z2 is set
dom b is set
(dom b) /\ (dom z2) is set
dom (b,z2) is set
z2 . x1 is set
dom a is set
b . x1 is set
dom A is set
[(b . x1),(z2 . x1)] is set
{(b . x1),(z2 . x1)} is non empty set
{(b . x1)} is non empty set
{{(b . x1),(z2 . x1)},{(b . x1)}} is non empty set
[:(dom A),(dom a):] is Relation-like set
dom (A,a) is set
(b,z2) . x1 is set
x1 is set
((b,z2) * (A,a)) . x1 is set
((b * A),(z2 * a)) . x1 is set
dom (b,z2) is set
dom b is set
dom z2 is set
(dom b) /\ (dom z2) is set
(b,z2) . x1 is set
dom (A,a) is set
b . x1 is set
z2 . x1 is set
[(b . x1),(z2 . x1)] is set
{(b . x1),(z2 . x1)} is non empty set
{(b . x1)} is non empty set
{{(b . x1),(z2 . x1)},{(b . x1)}} is non empty set
dom A is set
dom a is set
[:(dom A),(dom a):] is Relation-like set
dom (z2 * a) is set
dom (b * A) is set
(dom (b * A)) /\ (dom (z2 * a)) is set
(A,a) . ((b,z2) . x1) is set
(A,a) . ((b . x1),(z2 . x1)) is set
(A,a) . [(b . x1),(z2 . x1)] is set
A . (b . x1) is set
a . (z2 . x1) is set
[(A . (b . x1)),(a . (z2 . x1))] is set
{(A . (b . x1)),(a . (z2 . x1))} is non empty set
{(A . (b . x1))} is non empty set
{{(A . (b . x1)),(a . (z2 . x1))},{(A . (b . x1))}} is non empty set
(b * A) . x1 is set
[((b * A) . x1),(a . (z2 . x1))] is set
{((b * A) . x1),(a . (z2 . x1))} is non empty set
{((b * A) . x1)} is non empty set
{{((b * A) . x1),(a . (z2 . x1))},{((b * A) . x1)}} is non empty set
(z2 * a) . x1 is set
[((b * A) . x1),((z2 * a) . x1)] is set
{((b * A) . x1),((z2 * a) . x1)} is non empty set
{{((b * A) . x1),((z2 * a) . x1)},{((b * A) . x1)}} is non empty set
b is Relation-like Function-like set
z2 is Relation-like Function-like set
(b,z2) is Relation-like Function-like set
A is Relation-like Function-like set
a is Relation-like Function-like set
(A,a) is Relation-like Function-like set
(b,z2) * (A,a) is Relation-like Function-like set
b * A is Relation-like Function-like set
z2 * a is Relation-like Function-like set
((b * A),(z2 * a)) is Relation-like Function-like set
dom (b * A) is set
dom (z2 * a) is set
x1 is set
y1 is set
((b,z2) * (A,a)) . (x1,y1) is set
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
((b,z2) * (A,a)) . [x1,y1] is set
((b * A),(z2 * a)) . (x1,y1) is set
((b * A),(z2 * a)) . [x1,y1] is set
b . x1 is set
dom A is set
z2 . y1 is set
dom a is set
dom b is set
dom z2 is set
[:(dom b),(dom z2):] is Relation-like set
dom (b,z2) is set
(b,z2) . (x1,y1) is set
(b,z2) . [x1,y1] is set
(A,a) . ((b,z2) . (x1,y1)) is set
(A,a) . ((b . x1),(z2 . y1)) is set
[(b . x1),(z2 . y1)] is set
{(b . x1),(z2 . y1)} is non empty set
{(b . x1)} is non empty set
{{(b . x1),(z2 . y1)},{(b . x1)}} is non empty set
(A,a) . [(b . x1),(z2 . y1)] is set
A . (b . x1) is set
a . (z2 . y1) is set
[(A . (b . x1)),(a . (z2 . y1))] is set
{(A . (b . x1)),(a . (z2 . y1))} is non empty set
{(A . (b . x1))} is non empty set
{{(A . (b . x1)),(a . (z2 . y1))},{(A . (b . x1))}} is non empty set
(b * A) . x1 is set
[((b * A) . x1),(a . (z2 . y1))] is set
{((b * A) . x1),(a . (z2 . y1))} is non empty set
{((b * A) . x1)} is non empty set
{{((b * A) . x1),(a . (z2 . y1))},{((b * A) . x1)}} is non empty set
(z2 * a) . y1 is set
[((b * A) . x1),((z2 * a) . y1)] is set
{((b * A) . x1),((z2 * a) . y1)} is non empty set
{{((b * A) . x1),((z2 * a) . y1)},{((b * A) . x1)}} is non empty set
dom ((b,z2) * (A,a)) is set
[:(dom (b * A)),(dom (z2 * a)):] is Relation-like set
x1 is set
dom (b,z2) is set
dom b is set
dom z2 is set
[:(dom b),(dom z2):] is Relation-like set
dom (A,a) is set
dom A is set
dom a is set
[:(dom A),(dom a):] is Relation-like set
(b,z2) . x1 is set
y1 is set
x2 is set
[y1,x2] is set
{y1,x2} is non empty set
{y1} is non empty set
{{y1,x2},{y1}} is non empty set
(b,z2) . (y1,x2) is set
(b,z2) . [y1,x2] is set
b . y1 is set
z2 . x2 is set
[(b . y1),(z2 . x2)] is set
{(b . y1),(z2 . x2)} is non empty set
{(b . y1)} is non empty set
{{(b . y1),(z2 . x2)},{(b . y1)}} is non empty set
y1 is set
x2 is set
[y1,x2] is set
{y1,x2} is non empty set
{y1} is non empty set
{{y1,x2},{y1}} is non empty set
b . y1 is set
z2 . x2 is set
[(b . y1),(z2 . x2)] is set
{(b . y1),(z2 . x2)} is non empty set
{(b . y1)} is non empty set
{{(b . y1),(z2 . x2)},{(b . y1)}} is non empty set
(b,z2) . (y1,x2) is set
(b,z2) . [y1,x2] is set
dom ((b * A),(z2 * a)) is set
A is set
b is set
[:A,b:] is Relation-like set
a is Relation-like Function-like set
z2 is Relation-like Function-like set
(a,z2) is Relation-like Function-like set
(a,z2) .: [:A,b:] is set
a .: A is set
z2 .: b is set
[:(a .: A),(z2 .: b):] is Relation-like set
x1 is set
dom a is set
dom z2 is set
[:(dom a),(dom z2):] is Relation-like set
dom (a,z2) is set
y1 is set
(a,z2) . y1 is set
x2 is set
y2 is set
[x2,y2] is set
{x2,y2} is non empty set
{x2} is non empty set
{{x2,y2},{x2}} is non empty set
a . x2 is set
z2 . y2 is set
(a,z2) . (x2,y2) is set
(a,z2) . [x2,y2] is set
[(a . x2),(z2 . y2)] is set
{(a . x2),(z2 . y2)} is non empty set
{(a . x2)} is non empty set
{{(a . x2),(z2 . y2)},{(a . x2)}} is non empty set
y1 is set
x2 is set
[y1,x2] is set
{y1,x2} is non empty set
{y1} is non empty set
{{y1,x2},{y1}} is non empty set
y2 is set
a . y2 is set
b2 is set
z2 . b2 is set
(a,z2) . (y2,b2) is set
[y2,b2] is set
{y2,b2} is non empty set
{y2} is non empty set
{{y2,b2},{y2}} is non empty set
(a,z2) . [y2,b2] is set
[(a . y2),(z2 . b2)] is set
{(a . y2),(z2 . b2)} is non empty set
{(a . y2)} is non empty set
{{(a . y2),(z2 . b2)},{(a . y2)}} is non empty set
A is set
b is set
[:A,b:] is Relation-like set
a is Relation-like Function-like set
z2 is Relation-like Function-like set
(a,z2) is Relation-like Function-like set
(a,z2) " [:A,b:] is set
a " A is set
z2 " b is set
[:(a " A),(z2 " b):] is Relation-like set
x1 is set
(a,z2) . x1 is set
dom (a,z2) is set
dom a is set
dom z2 is set
[:(dom a),(dom z2):] is Relation-like set
y1 is set
x2 is set
[y1,x2] is set
{y1,x2} is non empty set
{y1} is non empty set
{{y1,x2},{y1}} is non empty set
(a,z2) . (y1,x2) is set
(a,z2) . [y1,x2] is set
a . y1 is set
z2 . x2 is set
[(a . y1),(z2 . x2)] is set
{(a . y1),(z2 . x2)} is non empty set
{(a . y1)} is non empty set
{{(a . y1),(z2 . x2)},{(a . y1)}} is non empty set
y1 is set
x2 is set
[y1,x2] is set
{y1,x2} is non empty set
{y1} is non empty set
{{y1,x2},{y1}} is non empty set
a . y1 is set
z2 . x2 is set
[(a . y1),(z2 . x2)] is set
{(a . y1),(z2 . x2)} is non empty set
{(a . y1)} is non empty set
{{(a . y1),(z2 . x2)},{(a . y1)}} is non empty set
dom a is set
dom z2 is set
[:(dom a),(dom z2):] is Relation-like set
(a,z2) . (y1,x2) is set
(a,z2) . [y1,x2] is set
dom (a,z2) is set
A is set
b is set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is set
[:A,a:] is Relation-like set
z2 is set
[:a,z2:] is Relation-like set
bool [:a,z2:] is non empty set
[:b,z2:] is Relation-like set
[:[:A,a:],[:b,z2:]:] is Relation-like set
bool [:[:A,a:],[:b,z2:]:] is non empty set
x1 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
y1 is Relation-like a -defined z2 -valued Function-like quasi_total Element of bool [:a,z2:]
(x1,y1) is Relation-like Function-like set
rng x1 is set
rng y1 is set
[:(rng x1),(rng y1):] is Relation-like set
rng (x1,y1) is set
dom y1 is Element of bool a
bool a is non empty set
dom x1 is Element of bool A
bool A is non empty set
dom (x1,y1) is set
dom x1 is Element of bool A
bool A is non empty set
dom y1 is Element of bool a
bool a is non empty set
[:(dom x1),(dom y1):] is Relation-like set
dom (x1,y1) is set
rng x1 is set
rng y1 is set
[:(rng x1),(rng y1):] is Relation-like set
rng (x1,y1) is set
dom x1 is Element of bool A
bool A is non empty set
dom y1 is Element of bool a
bool a is non empty set
[:(dom x1),(dom y1):] is Relation-like set
dom (x1,y1) is set
rng (x1,y1) is set
x2 is Relation-like [:A,a:] -defined [:b,z2:] -valued Element of bool [:[:A,a:],[:b,z2:]:]
A is set
a is set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
b is set
z2 is set
[:b,z2:] is Relation-like set
bool [:b,z2:] is non empty set
x1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
y1 is Relation-like b -defined z2 -valued Function-like quasi_total Element of bool [:b,z2:]
(x1,y1) is Relation-like Function-like set
[:A,b:] is Relation-like set
[:a,z2:] is Relation-like set
[:[:A,b:],[:a,z2:]:] is Relation-like set
bool [:[:A,b:],[:a,z2:]:] is non empty set
A is non empty set
b is non empty set
[:A,b:] is Relation-like non empty set
bool [:A,b:] is non empty set
a is non empty set
z2 is non empty set
[:a,z2:] is Relation-like non empty set
bool [:a,z2:] is non empty set
[:b,z2:] is Relation-like non empty set
x1 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
y1 is Relation-like a -defined z2 -valued Function-like quasi_total Element of bool [:a,z2:]
(A,a,b,z2,x1,y1) is Relation-like [:A,a:] -defined [:b,z2:] -valued Function-like quasi_total Element of bool [:[:A,a:],[:b,z2:]:]
[:A,a:] is Relation-like non empty set
[:[:A,a:],[:b,z2:]:] is Relation-like non empty set
bool [:[:A,a:],[:b,z2:]:] is non empty set
x2 is Element of A
x1 . x2 is Element of b
y2 is Element of a
(A,a,b,z2,x1,y1) . (x2,y2) is Element of [:b,z2:]
[x2,y2] is set
{x2,y2} is non empty set
{x2} is non empty set
{{x2,y2},{x2}} is non empty set
(A,a,b,z2,x1,y1) . [x2,y2] is set
y1 . y2 is Element of z2
[(x1 . x2),(y1 . y2)] is set
{(x1 . x2),(y1 . y2)} is non empty set
{(x1 . x2)} is non empty set
{{(x1 . x2),(y1 . y2)},{(x1 . x2)}} is non empty set
dom x1 is Element of bool A
bool A is non empty set
dom y1 is Element of bool a
bool a is non empty set
A is set
b is set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is set
(A,a) is Relation-like [:A,a:] -defined A -valued Function-like quasi_total Element of bool [:[:A,a:],A:]
[:A,a:] is Relation-like set
[:[:A,a:],A:] is Relation-like set
bool [:[:A,a:],A:] is non empty set
(A,a) is Relation-like [:A,a:] -defined a -valued Function-like quasi_total Element of bool [:[:A,a:],a:]
[:[:A,a:],a:] is Relation-like set
bool [:[:A,a:],a:] is non empty set
z2 is set
[:a,z2:] is Relation-like set
bool [:a,z2:] is non empty set
x1 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
(A,a) * x1 is Relation-like [:A,a:] -defined b -valued Function-like set
y1 is Relation-like a -defined z2 -valued Function-like quasi_total Element of bool [:a,z2:]
(A,a,b,z2,x1,y1) is Relation-like [:A,a:] -defined [:b,z2:] -valued Function-like quasi_total Element of bool [:[:A,a:],[:b,z2:]:]
[:b,z2:] is Relation-like set
[:[:A,a:],[:b,z2:]:] is Relation-like set
bool [:[:A,a:],[:b,z2:]:] is non empty set
(A,a) * y1 is Relation-like [:A,a:] -defined z2 -valued Function-like set
(((A,a) * x1),((A,a) * y1)) is Relation-like Function-like set
dom x1 is Element of bool A
bool A is non empty set
dom y1 is Element of bool a
bool a is non empty set
A is set
b is set
(A,b) is Relation-like [:A,b:] -defined A -valued Function-like quasi_total Element of bool [:[:A,b:],A:]
[:A,b:] is Relation-like set
[:[:A,b:],A:] is Relation-like set
bool [:[:A,b:],A:] is non empty set
(A,b) is Relation-like [:A,b:] -defined b -valued Function-like quasi_total Element of bool [:[:A,b:],b:]
[:[:A,b:],b:] is Relation-like set
bool [:[:A,b:],b:] is non empty set
a is non empty set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
z2 is non empty set
[:b,z2:] is Relation-like set
bool [:b,z2:] is non empty set
x1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(A,b) * x1 is Relation-like [:A,b:] -defined a -valued Function-like set
y1 is Relation-like b -defined z2 -valued Function-like quasi_total Element of bool [:b,z2:]
(A,b,a,z2,x1,y1) is Relation-like [:A,b:] -defined [:a,z2:] -valued Function-like quasi_total Element of bool [:[:A,b:],[:a,z2:]:]
[:a,z2:] is Relation-like non empty set
[:[:A,b:],[:a,z2:]:] is Relation-like set
bool [:[:A,b:],[:a,z2:]:] is non empty set
(A,b) * y1 is Relation-like [:A,b:] -defined z2 -valued Function-like set
(((A,b) * x1),((A,b) * y1)) is Relation-like Function-like set
dom x1 is Element of bool A
bool A is non empty set
dom y1 is Element of bool b
bool b is non empty set
A is set
(A) is Relation-like A -defined [:A,A:] -valued Function-like quasi_total Element of bool [:A,[:A,A:]:]
[:A,A:] is Relation-like set
[:A,[:A,A:]:] is Relation-like set
bool [:A,[:A,A:]:] is non empty set
b is set
[:A,b:] is Relation-like set
bool [:A,b:] is non empty set
a is set
[:A,a:] is Relation-like set
bool [:A,a:] is non empty set
z2 is Relation-like A -defined b -valued Function-like quasi_total Element of bool [:A,b:]
x1 is Relation-like A -defined a -valued Function-like quasi_total Element of bool [:A,a:]
(z2,x1) is Relation-like Function-like set
(A,A,b,a,z2,x1) is Relation-like [:A,A:] -defined [:b,a:] -valued Function-like quasi_total Element of bool [:[:A,A:],[:b,a:]:]
[:b,a:] is Relation-like set
[:[:A,A:],[:b,a:]:] is Relation-like set
bool [:[:A,A:],[:b,a:]:] is non empty set
(A) * (A,A,b,a,z2,x1) is Relation-like A -defined [:b,a:] -valued Function-like set
dom z2 is Element of bool A
bool A is non empty set
dom x1 is Element of bool A
dom (A,A,b,a,z2,x1) is Relation-like A -defined A -valued Element of bool [:A,A:]
bool [:A,A:] is non empty set
[:(dom z2),(dom x1):] is Relation-like set
dom (z2,x1) is set
(dom z2) /\ (dom x1) is Element of bool A
(A) * {} is Relation-like non-empty empty-yielding A -defined Function-like one-to-one constant functional empty set
dom z2 is Element of bool A
bool A is non empty set
dom x1 is Element of bool A
A is Relation-like Function-like set
dom A is set
rng A is set
((dom A),(rng A)) is Relation-like [:(dom A),(rng A):] -defined dom A -valued Function-like quasi_total Element of bool [:[:(dom A),(rng A):],(dom A):]
[:(dom A),(rng A):] is Relation-like set
[:[:(dom A),(rng A):],(dom A):] is Relation-like set
bool [:[:(dom A),(rng A):],(dom A):] is non empty set
((dom A),(rng A)) .: A is set
b is set
dom ((dom A),(rng A)) is Relation-like dom A -defined rng A -valued Element of bool [:(dom A),(rng A):]
bool [:(dom A),(rng A):] is non empty set
A . b is set
[b,(A . b)] is set
{b,(A . b)} is non empty set
{b} is non empty set
{{b,(A . b)},{b}} is non empty set
((dom A),(rng A)) . [b,(A . b)] is set
((dom A),(rng A)) . (b,(A . b)) is set
a is set
((dom A),(rng A)) . a is set
z2 is set
x1 is set
[z2,x1] is set
{z2,x1} is non empty set
{z2} is non empty set
{{z2,x1},{z2}} is non empty set
((dom A),(rng A)) . (z2,x1) is set
((dom A),(rng A)) . [z2,x1] is set
A is non empty set
b is non empty set
a is non empty set
[:b,a:] is Relation-like non empty set
[:A,[:b,a:]:] is Relation-like non empty set
bool [:A,[:b,a:]:] is non empty set
(b,a) is Relation-like [:b,a:] -defined b -valued Function-like quasi_total Element of bool [:[:b,a:],b:]
[:[:b,a:],b:] is Relation-like non empty set
bool [:[:b,a:],b:] is non empty set
(b,a) is Relation-like [:b,a:] -defined a -valued Function-like quasi_total Element of bool [:[:b,a:],a:]
[:[:b,a:],a:] is Relation-like non empty set
bool [:[:b,a:],a:] is non empty set
z2 is Relation-like A -defined [:b,a:] -valued Function-like quasi_total Element of bool [:A,[:b,a:]:]
z2 * (b,a) is Relation-like A -defined b -valued Function-like set
x1 is Relation-like A -defined [:b,a:] -valued Function-like quasi_total Element of bool [:A,[:b,a:]:]
x1 * (b,a) is Relation-like A -defined b -valued Function-like set
z2 * (b,a) is Relation-like A -defined a -valued Function-like set
x1 * (b,a) is Relation-like A -defined a -valued Function-like set
y1 is Element of A
z2 . y1 is Element of [:b,a:]
x2 is Element of b
y2 is Element of a
[x2,y2] is set
{x2,y2} is non empty set
{x2} is non empty set
{{x2,y2},{x2}} is non empty set
x1 . y1 is Element of [:b,a:]
b2 is Element of b
c2 is Element of a
[b2,c2] is set
{b2,c2} is non empty set
{b2} is non empty set
{{b2,c2},{b2}} is non empty set
(b,a) . (x1 . y1) is Element of b
(x1 * (b,a)) . y1 is set
(b,a) . (z2 . y1) is Element of b
(z2 * (b,a)) . y1 is set
(b,a) . (z2 . y1) is Element of a
(z2 * (b,a)) . y1 is set
(b,a) . (x2,y2) is Element of a
(b,a) . [x2,y2] is set
(b,a) . (b2,c2) is Element of a
(b,a) . [b2,c2] is set
(b,a) . (x2,y2) is Element of b
(b,a) . [x2,y2] is set
(b,a) . (b2,c2) is Element of b
(b,a) . [b2,c2] is set
A is Relation-like Function-like one-to-one set
b is Relation-like Function-like one-to-one set
(A,b) is Relation-like Function-like set
a is set
dom (A,b) is set
z2 is set
(A,b) . a is set
(A,b) . z2 is set
dom A is set
dom b is set
[:(dom A),(dom b):] is Relation-like set
x1 is set
y1 is set
[x1,y1] is set
{x1,y1} is non empty set
{x1} is non empty set
{{x1,y1},{x1}} is non empty set
(A,b) . (x1,y1) is set
(A,b) . [x1,y1] is set
A . x1 is set
b . y1 is set
[(A . x1),(b . y1)] is set
{(A . x1),(b . y1)} is non empty set
{(A . x1)} is non empty set
{{(A . x1),(b . y1)},{(A . x1)}} is non empty set
x2 is set
y2 is set
[x2,y2] is set
{x2,y2} is non empty set
{x2} is non empty set
{{x2,y2},{x2}} is non empty set
(A,b) . (x2,y2) is set
(A,b) . [x2,y2] is set
A . x2 is set
b . y2 is set
[(A . x2),(b . y2)] is set
{(A . x2),(b . y2)} is non empty set
{(A . x2)} is non empty set
{{(A . x2),(b . y2)},{(A . x2)}} is non empty set
A is set
[:A,A:] is Relation-like set
[:[:A,A:],A:] is Relation-like set
bool [:[:A,A:],A:] is non empty set
(A,A) is Relation-like [:A,A:] -defined A -valued Function-like quasi_total Element of bool [:[:A,A:],A:]
b is Element of A
(A,A) . (b,b) is Element of A
[b,b] is set
{b,b} is non empty set
{b} is non empty set
{{b,b},{b}} is non empty set
(A,A) . [b,b] is set
(A,A) . (b,b) is Element of A
b is Element of A
(A,A) . (b,b) is Element of A
[b,b] is set
{b,b} is non empty set
{b} is non empty set
{{b,b},{b}} is non empty set
(A,A) . [b,b] is set
dom (A,A) is Relation-like A -defined A -valued Element of bool [:A,A:]
bool [:A,A:] is non empty set
(A,A) . (b,b) is Element of A
A is set
[:A,A:] is Relation-like set
[:[:A,A:],A:] is Relation-like set
bool [:[:A,A:],A:] is non empty set
b is Relation-like [:A,A:] -defined A -valued Function-like quasi_total idempotent Element of bool [:[:A,A:],A:]
a is Element of A
b . (a,a) is Element of A
[a,a] is set
{a,a} is non empty set
{a} is non empty set
{{a,a},{a}} is non empty set
b . [a,a] is set