:: FUNCT_3 semantic presentation

A is set

b is set

b /\ A is set

A is 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

dom b is set
b .: A is set

dom a is set

dom (b * a) is set
z2 is set
b . z2 is set
A is 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

rng a is set
a " A is set

rng b is 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

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

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

dom a is 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

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

dom b is set
a is set
b . a is set
A .: a is set

dom b is set

dom a is set
z2 is set
b . z2 is set
a . z2 is set
A .: z2 is set
A is 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 set
dom A is 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) .: A is set
rng b is set
bool (rng b) is non empty set
rng (b) is set
A is 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) " b is set
dom z2 is Element of bool A
A is set
union A is set

(b) .: A is set
union ((b) .: A) is set
b .: () 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

dom b is set
bool (dom b) is non empty set
b .: () is 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 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) " A is set
union ((b) " A) is set
b " () 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

rng b is set
bool (rng b) is non empty set
b " () is 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 * 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

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

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

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

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

dom b is set
a is set
b . a is set
A " a is set

dom b is set

dom a is set
z2 is set
b . z2 is set
a . z2 is set
A " z2 is set
A is set

dom (b) is set
(b) . A is set
b " A is set
rng b is set
bool (rng b) is non empty 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) .: A is set
dom b is set
bool (dom b) is non empty set
rng (b) is set
A is 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) .: A is set
union ((b) .: A) is set
b " () 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

rng b is set
bool (rng b) is non empty set

(b) .: A is set
union ((b) .: A) is set
b " () 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) " A is set
union ((b) " A) is set
b .: () 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

dom b is set
bool (dom b) is non empty set

(b) " A is set
union ((b) " A) is set
b .: () 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) .: A is 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) .: A is 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

dom A is set
bool (dom A) is non empty 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

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

dom A is set
bool (dom A) is non empty set

b is set
(A) " b is set
(A) .: b is set

((A * b)) 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

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

dom a is set

dom a is 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 " {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

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

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

A is set
b is set
bool b is non empty set
a is Element of bool 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

dom a is set

dom a is 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

dom a is set

dom a is 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

dom b is set

dom b is 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

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

dom A is set

dom b is set
(dom A) /\ (dom b) is set

dom a is set

dom a is 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,b) is Relation-like Function-like 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 (b,A) is set
dom b is set
{} /\ (dom b) is Relation-like set
A is set

dom b is 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

dom a is 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

dom b is 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,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

dom a is 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

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

dom A is set

dom b is set

dom z2 is 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 * 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,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,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,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,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

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

(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

(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,y1) is Relation-like Function-like set

(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

(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

(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

dom A is set

dom b is set
[:(dom A),(dom b):] is Relation-like set

dom a is set

dom a is 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

dom A is 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,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,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,A:] is Relation-like set
[:A,[:A,A:]:] is Relation-like set
bool [:A,[:A,A:]:] is non empty set

dom b is 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

b is set

((id A),(id b)) is Relation-like Function-like set
[:A,b:] is Relation-like 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,z2) 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),(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,z2) 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),(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