:: FUNCT_3 semantic presentation

{} 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

F

F

[:F

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

F

F

[:F

A is set

b is set

F

A is set

b is set

a is set

F

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