:: FUNCT_6 semantic presentation

K64() is non empty V18() V19() V20() set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() set

1 is non empty V18() V19() V20() V24() Element of K64()

{{},1} is non empty V36() set

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

bool [:1,1:] is set

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

bool [:[:1,1:],1:] is set

bool K64() is set

union {} is V18() V19() V20() V36() set

product {} is set

{{}} is non empty functional V36() V40() set

curry {} is Relation-like Function-like set

curry' {} is Relation-like Function-like set

uncurry {} is Relation-like Function-like set

uncurry' {} is Relation-like Function-like set

dom {} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() set

rng {} is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() set

f is Relation-like Function-like set

product f is set

dom f is set

Union f is set

Funcs ((dom f),(Union f)) is functional set

i is set

C is Relation-like Function-like set

dom C is set

rng C is set

f is set

rng f is set

union (rng f) is set

cf is set

C . cf is set

f . cf is set

f is set

i is Relation-like Function-like set

~ i is Relation-like Function-like set

dom (~ i) is set

C is set

f is set

[:C,f:] is Relation-like set

f is set

i is set

[:f,i:] is Relation-like set

[:i,f:] is Relation-like set

C is set

[:f,i:] --> C is Relation-like [:f,i:] -defined {C} -valued Function-like constant total quasi_total Element of bool [:[:f,i:],{C}:]

{C} is non empty V36() set

[:[:f,i:],{C}:] is Relation-like set

bool [:[:f,i:],{C}:] is set

~ ([:f,i:] --> C) is Relation-like Function-like set

[:i,f:] --> C is Relation-like [:i,f:] -defined {C} -valued Function-like constant total quasi_total Element of bool [:[:i,f:],{C}:]

[:[:i,f:],{C}:] is Relation-like set

bool [:[:i,f:],{C}:] is set

dom ([:f,i:] --> C) is Relation-like set

dom (~ ([:f,i:] --> C)) is set

f is set

ccf is set

cf is set

[ccf,cf] is V25() set

{ccf,cf} is non empty V36() set

{ccf} is non empty V36() set

{{ccf,cf},{ccf}} is non empty V36() V40() set

[cf,ccf] is V25() set

{cf,ccf} is non empty V36() set

{cf} is non empty V36() set

{{cf,ccf},{cf}} is non empty V36() V40() set

([:f,i:] --> C) . (cf,ccf) is set

([:f,i:] --> C) . [cf,ccf] is set

([:i,f:] --> C) . (ccf,cf) is set

([:i,f:] --> C) . [ccf,cf] is set

(~ ([:f,i:] --> C)) . (ccf,cf) is set

(~ ([:f,i:] --> C)) . [ccf,cf] is set

(~ ([:f,i:] --> C)) . f is set

([:i,f:] --> C) . f is set

dom ([:i,f:] --> C) is Relation-like set

f is Relation-like Function-like set

curry f is Relation-like Function-like set

~ f is Relation-like Function-like set

curry' (~ f) is Relation-like Function-like set

uncurry f is Relation-like Function-like set

uncurry' f is Relation-like Function-like set

~ (uncurry' f) is Relation-like Function-like set

~ (~ f) is Relation-like Function-like set

curry (~ (~ f)) is Relation-like Function-like set

dom (curry (~ (~ f))) is set

dom (~ (~ f)) is set

dom (dom (~ (~ f))) is set

dom (curry f) is set

dom f is set

dom (dom f) is set

i is set

C is set

[i,C] is V25() set

{i,C} is non empty V36() set

{i} is non empty V36() set

{{i,C},{i}} is non empty V36() V40() set

[C,i] is V25() set

{C,i} is non empty V36() set

{C} is non empty V36() set

{{C,i},{C}} is non empty V36() V40() set

dom (~ f) is set

i is set

C is set

[i,C] is V25() set

{i,C} is non empty V36() set

{i} is non empty V36() set

{{i,C},{i}} is non empty V36() V40() set

[C,i] is V25() set

{C,i} is non empty V36() set

{C} is non empty V36() set

{{C,i},{C}} is non empty V36() V40() set

dom (~ f) is set

i is set

(curry f) . i is set

(curry' (~ f)) . i is set

C is Relation-like Function-like set

dom C is set

{i} is non empty V36() set

rng (dom f) is set

[:{i},(rng (dom f)):] is Relation-like set

(dom f) /\ [:{i},(rng (dom f)):] is Relation-like set

rng ((dom f) /\ [:{i},(rng (dom f)):]) is set

f is Relation-like Function-like set

dom f is set

dom (~ f) is set

dom (dom (~ f)) is set

[:(dom (dom (~ f))),{i}:] is Relation-like set

(dom (~ f)) /\ [:(dom (dom (~ f))),{i}:] is Relation-like set

dom ((dom (~ f)) /\ [:(dom (dom (~ f))),{i}:]) is set

cf is set

ccf is set

[ccf,cf] is V25() set

{ccf,cf} is non empty V36() set

{ccf} is non empty V36() set

{{ccf,cf},{ccf}} is non empty V36() V40() set

[cf,ccf] is V25() set

{cf,ccf} is non empty V36() set

{cf} is non empty V36() set

{{cf,ccf},{cf}} is non empty V36() V40() set

[:(rng (dom f)),{i}:] is Relation-like set

cf is set

ccf is set

[cf,ccf] is V25() set

{cf,ccf} is non empty V36() set

{cf} is non empty V36() set

{{cf,ccf},{cf}} is non empty V36() V40() set

[ccf,cf] is V25() set

{ccf,cf} is non empty V36() set

{ccf} is non empty V36() set

{{ccf,cf},{ccf}} is non empty V36() V40() set

[:{i},(dom (dom (~ f))):] is Relation-like set

cf is set

[i,cf] is V25() set

{i,cf} is non empty V36() set

{{i,cf},{i}} is non empty V36() V40() set

C . cf is set

f . (i,cf) is set

f . [i,cf] is set

f . cf is set

(~ f) . (cf,i) is set

[cf,i] is V25() set

{cf,i} is non empty V36() set

{cf} is non empty V36() set

{{cf,i},{cf}} is non empty V36() V40() set

(~ f) . [cf,i] is set

dom (uncurry f) is set

~ (uncurry f) is Relation-like Function-like set

~ (~ (uncurry f)) is Relation-like Function-like set

dom (~ (~ (uncurry f))) is set

i is set

C is set

cf is set

[C,cf] is V25() set

{C,cf} is non empty V36() set

{C} is non empty V36() set

{{C,cf},{C}} is non empty V36() V40() set

f is Relation-like Function-like set

f . C is set

dom f is set

[cf,C] is V25() set

{cf,C} is non empty V36() set

{cf} is non empty V36() set

{{cf,C},{cf}} is non empty V36() V40() set

dom (~ (uncurry f)) is set

i is set

dom (~ (uncurry f)) is set

f is set

C is set

[f,C] is V25() set

{f,C} is non empty V36() set

{f} is non empty V36() set

{{f,C},{f}} is non empty V36() V40() set

[C,f] is V25() set

{C,f} is non empty V36() set

{C} is non empty V36() set

{{C,f},{C}} is non empty V36() V40() set

i is set

dom (~ (uncurry f)) is set

f is set

C is set

[f,C] is V25() set

{f,C} is non empty V36() set

{f} is non empty V36() set

{{f,C},{f}} is non empty V36() V40() set

[C,f] is V25() set

{C,f} is non empty V36() set

{C} is non empty V36() set

{{C,f},{C}} is non empty V36() V40() set

(~ (uncurry f)) . (C,f) is set

(~ (uncurry f)) . [C,f] is set

(uncurry f) . (f,C) is set

(uncurry f) . [f,C] is set

(~ (~ (uncurry f))) . (f,C) is set

(~ (~ (uncurry f))) . [f,C] is set

(uncurry f) . i is set

(~ (~ (uncurry f))) . i is set

f is set

i is set

[:f,i:] is Relation-like set

C is set

[:f,i:] --> C is Relation-like [:f,i:] -defined {C} -valued Function-like constant total quasi_total Element of bool [:[:f,i:],{C}:]

{C} is non empty V36() set

[:[:f,i:],{C}:] is Relation-like set

bool [:[:f,i:],{C}:] is set

curry ([:f,i:] --> C) is Relation-like Function-like set

i --> C is Relation-like i -defined {C} -valued Function-like constant total quasi_total Element of bool [:i,{C}:]

[:i,{C}:] is Relation-like set

bool [:i,{C}:] is set

f --> (i --> C) is Relation-like f -defined {(i --> C)} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:f,{(i --> C)}:]

{(i --> C)} is non empty functional V36() set

[:f,{(i --> C)}:] is Relation-like set

bool [:f,{(i --> C)}:] is set

curry' ([:f,i:] --> C) is Relation-like Function-like set

f --> C is Relation-like f -defined {C} -valued Function-like constant total quasi_total Element of bool [:f,{C}:]

[:f,{C}:] is Relation-like set

bool [:f,{C}:] is set

i --> (f --> C) is Relation-like i -defined {(f --> C)} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:i,{(f --> C)}:]

{(f --> C)} is non empty functional V36() set

[:i,{(f --> C)}:] is Relation-like set

bool [:i,{(f --> C)}:] is set

dom ([:f,i:] --> C) is Relation-like set

dom (f --> C) is set

f is set

(curry' ([:f,i:] --> C)) . f is set

rng ([:f,i:] --> C) is trivial V36() set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

ccf is set

cf . ccf is set

([:f,i:] --> C) . (ccf,f) is set

[ccf,f] is V25() set

{ccf,f} is non empty V36() set

{ccf} is non empty V36() set

{{ccf,f},{ccf}} is non empty V36() V40() set

([:f,i:] --> C) . [ccf,f] is set

(f --> C) . ccf is set

(i --> (f --> C)) . f is Relation-like Function-like set

dom (i --> C) is set

f is set

(curry ([:f,i:] --> C)) . f is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

ccf is set

cf . ccf is set

([:f,i:] --> C) . (f,ccf) is set

[f,ccf] is V25() set

{f,ccf} is non empty V36() set

{f} is non empty V36() set

{{f,ccf},{f}} is non empty V36() V40() set

([:f,i:] --> C) . [f,ccf] is set

(i --> C) . ccf is set

(f --> (i --> C)) . f is Relation-like Function-like set

dom (f --> (i --> C)) is set

dom (curry ([:f,i:] --> C)) is set

dom (i --> (f --> C)) is set

dom (curry' ([:f,i:] --> C)) is set

f is set

i is set

[:f,i:] is Relation-like set

[:i,f:] is Relation-like set

C is set

i --> C is Relation-like i -defined {C} -valued Function-like constant total quasi_total Element of bool [:i,{C}:]

{C} is non empty V36() set

[:i,{C}:] is Relation-like set

bool [:i,{C}:] is set

f --> (i --> C) is Relation-like f -defined {(i --> C)} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:f,{(i --> C)}:]

{(i --> C)} is non empty functional V36() set

[:f,{(i --> C)}:] is Relation-like set

bool [:f,{(i --> C)}:] is set

uncurry (f --> (i --> C)) is Relation-like Function-like set

[:f,i:] --> C is Relation-like [:f,i:] -defined {C} -valued Function-like constant total quasi_total Element of bool [:[:f,i:],{C}:]

[:[:f,i:],{C}:] is Relation-like set

bool [:[:f,i:],{C}:] is set

uncurry' (f --> (i --> C)) is Relation-like Function-like set

[:i,f:] --> C is Relation-like [:i,f:] -defined {C} -valued Function-like constant total quasi_total Element of bool [:[:i,f:],{C}:]

[:[:i,f:],{C}:] is Relation-like set

bool [:[:i,f:],{C}:] is set

dom (f --> (i --> C)) is set

dom (i --> C) is set

rng (i --> C) is trivial V36() set

Funcs (i,{C}) is non empty functional FUNCTION_DOMAIN of i,{C}

rng (f --> (i --> C)) is trivial V36() set

dom (uncurry (f --> (i --> C))) is set

f is set

cf is set

uf is set

[cf,uf] is V25() set

{cf,uf} is non empty V36() set

{cf} is non empty V36() set

{{cf,uf},{cf}} is non empty V36() V40() set

ccf is Relation-like Function-like set

(f --> (i --> C)) . cf is Relation-like Function-like set

dom ccf is set

(i --> C) . uf is set

(uncurry (f --> (i --> C))) . (cf,uf) is set

(uncurry (f --> (i --> C))) . [cf,uf] is set

(uncurry (f --> (i --> C))) . f is set

([:f,i:] --> C) . f is set

dom ([:f,i:] --> C) is Relation-like set

~ (uncurry (f --> (i --> C))) is Relation-like Function-like set

f is set

i is Relation-like Function-like set

dom i is set

i . f is set

uncurry i is Relation-like Function-like set

rng (uncurry i) is set

uncurry' i is Relation-like Function-like set

rng (uncurry' i) is set

C is Relation-like Function-like set

rng C is set

f is set

dom C is set

cf is set

C . cf is set

f is set

dom C is set

cf is set

C . cf is set

f is set

i is Relation-like Function-like set

f --> i is Relation-like f -defined {i} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:f,{i}:]

{i} is non empty functional V36() set

[:f,{i}:] is Relation-like set

bool [:f,{i}:] is set

uncurry (f --> i) is Relation-like Function-like set

dom (uncurry (f --> i)) is set

dom i is set

[:f,(dom i):] is Relation-like set

rng (uncurry (f --> i)) is set

rng i is set

uncurry' (f --> i) is Relation-like Function-like set

dom (uncurry' (f --> i)) is set

[:(dom i),f:] is Relation-like set

rng (uncurry' (f --> i)) is set

Funcs ((dom i),(rng i)) is functional set

rng (f --> i) is trivial V36() set

dom (f --> i) is set

f is set

i is Relation-like Function-like set

f --> i is Relation-like f -defined {i} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:f,{i}:]

{i} is non empty functional V36() set

[:f,{i}:] is Relation-like set

bool [:f,{i}:] is set

uncurry (f --> i) is Relation-like Function-like set

rng (uncurry (f --> i)) is set

rng i is set

uncurry' (f --> i) is Relation-like Function-like set

rng (uncurry' (f --> i)) is set

the Element of f is Element of f

dom (f --> i) is set

(f --> i) . the Element of f is Relation-like Function-like set

f is set

i is set

[:f,i:] is Relation-like set

C is set

Funcs ([:f,i:],C) is functional set

Funcs (i,C) is functional set

Funcs (f,(Funcs (i,C))) is functional set

Funcs (f,C) is functional set

Funcs (i,(Funcs (f,C))) is functional set

f is Relation-like Function-like set

curry f is Relation-like Function-like set

curry' f is Relation-like Function-like set

rng (curry f) is set

rng f is set

Funcs (i,(rng f)) is functional set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

rng (curry' f) is set

Funcs (f,(rng f)) is functional set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

dom (curry f) is set

dom (curry' f) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

f is set

i is set

[:f,i:] is Relation-like set

[:i,f:] is Relation-like set

C is set

Funcs (i,C) is functional set

Funcs (f,(Funcs (i,C))) is functional set

Funcs ([:f,i:],C) is functional set

Funcs ([:i,f:],C) is functional set

f is Relation-like Function-like set

uncurry f is Relation-like Function-like set

uncurry' f is Relation-like Function-like set

dom (uncurry f) is set

dom (uncurry' f) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

rng (uncurry f) is set

rng (uncurry' f) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

f is set

i is set

[:f,i:] is Relation-like set

C is set

Funcs (i,C) is functional set

Funcs (f,(Funcs (i,C))) is functional set

Funcs (f,C) is functional set

Funcs (i,(Funcs (f,C))) is functional set

Funcs ([:f,i:],C) is functional set

f is set

cf is set

[:f,cf:] is Relation-like set

ccf is Relation-like Function-like set

curry ccf is Relation-like Function-like set

curry' ccf is Relation-like Function-like set

dom ccf is set

uncurry (curry ccf) is Relation-like Function-like set

uncurry' (curry' ccf) is Relation-like Function-like set

f is set

i is set

[:f,i:] is Relation-like set

[:i,f:] is Relation-like set

C is set

Funcs ([:f,i:],C) is functional set

Funcs ([:i,f:],C) is functional set

Funcs (i,C) is functional set

Funcs (f,(Funcs (i,C))) is functional set

f is set

cf is set

PFuncs (f,cf) is set

ccf is Relation-like Function-like set

uncurry ccf is Relation-like Function-like set

uncurry' ccf is Relation-like Function-like set

rng ccf is set

dom ccf is set

~ (uncurry ccf) is Relation-like Function-like set

dom (uncurry' ccf) is set

uf is Relation-like Function-like set

dom uf is set

rng uf is set

ucf is Relation-like Function-like set

dom ucf is set

rng ucf is set

uf is set

ucf is set

ccf . ucf is set

g is Relation-like Function-like set

dom g is set

rng g is set

x is Relation-like Function-like set

dom x is set

g is set

[g,ucf] is V25() set

{g,ucf} is non empty V36() set

{g} is non empty V36() set

{{g,ucf},{g}} is non empty V36() V40() set

g is set

[g,ucf] is V25() set

{g,ucf} is non empty V36() set

{g} is non empty V36() set

{{g,ucf},{g}} is non empty V36() V40() set

[ucf,g] is V25() set

{ucf,g} is non empty V36() set

{ucf} is non empty V36() set

{{ucf,g},{ucf}} is non empty V36() V40() set

dom (uncurry ccf) is set

h is set

h is set

[h,h] is V25() set

{h,h} is non empty V36() set

{h} is non empty V36() set

{{h,h},{h}} is non empty V36() V40() set

y is Relation-like Function-like set

ccf . h is set

dom y is set

rng x is set

g is set

rng (uncurry ccf) is set

rng (uncurry' ccf) is set

h is set

x . h is set

h is Relation-like Function-like set

dom h is set

rng h is set

y is Relation-like Function-like set

dom y is set

rng y is set

f is set

i is set

[:f,i:] is Relation-like set

C is set

PFuncs ([:f,i:],C) is set

PFuncs (i,C) is set

PFuncs (f,(PFuncs (i,C))) is set

PFuncs (f,C) is set

PFuncs (i,(PFuncs (f,C))) is set

f is Relation-like Function-like set

curry f is Relation-like Function-like set

curry' f is Relation-like Function-like set

dom [:f,i:] is set

dom f is set

dom (dom f) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

rng f is set

PFuncs ((dom (dom f)),(rng f)) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

rng [:f,i:] is set

rng (dom f) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

rng (curry f) is set

PFuncs ((rng (dom f)),(rng f)) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

rng (curry' f) is set

dom (curry f) is set

dom (curry' f) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

f is set

i is set

[:f,i:] is Relation-like set

[:i,f:] is Relation-like set

C is set

PFuncs (i,C) is set

PFuncs (f,(PFuncs (i,C))) is set

PFuncs ([:f,i:],C) is set

PFuncs ([:i,f:],C) is set

f is Relation-like Function-like set

uncurry f is Relation-like Function-like set

uncurry' f is Relation-like Function-like set

dom (uncurry f) is set

dom f is set

[:(dom f),i:] is Relation-like set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

dom (uncurry' f) is set

[:i,(dom f):] is Relation-like set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

rng (uncurry f) is set

rng (uncurry' f) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

f is set

i is set

[:f,i:] is Relation-like set

C is set

PFuncs (i,C) is set

PFuncs (f,(PFuncs (i,C))) is set

PFuncs (f,C) is set

PFuncs (i,(PFuncs (f,C))) is set

PFuncs ([:f,i:],C) is set

f is set

cf is set

[:f,cf:] is Relation-like set

ccf is Relation-like Function-like set

curry ccf is Relation-like Function-like set

curry' ccf is Relation-like Function-like set

dom ccf is set

uncurry (curry ccf) is Relation-like Function-like set

uncurry' (curry' ccf) is Relation-like Function-like set

f is set

i is set

[:f,i:] is Relation-like set

[:i,f:] is Relation-like set

C is set

PFuncs ([:f,i:],C) is set

PFuncs ([:i,f:],C) is set

PFuncs (i,C) is set

PFuncs (f,(PFuncs (i,C))) is set

f is set

cf is set

PFuncs (f,cf) is set

ccf is Relation-like Function-like set

uncurry ccf is Relation-like Function-like set

uncurry' ccf is Relation-like Function-like set

rng ccf is set

dom ccf is set

~ (uncurry ccf) is Relation-like Function-like set

dom (uncurry' ccf) is set

uf is Relation-like Function-like set

dom uf is set

rng uf is set

ucf is Relation-like Function-like set

dom ucf is set

rng ucf is set

uf is set

ucf is set

ccf . ucf is set

g is Relation-like Function-like set

dom g is set

rng g is set

x is Relation-like Function-like set

rng x is set

g is set

dom x is set

rng (uncurry ccf) is set

rng (uncurry' ccf) is set

h is set

x . h is set

h is Relation-like Function-like set

dom h is set

rng h is set

y is Relation-like Function-like set

dom y is set

rng y is set

dom x is set

g is set

[g,ucf] is V25() set

{g,ucf} is non empty V36() set

{g} is non empty V36() set

{{g,ucf},{g}} is non empty V36() V40() set

f is set

i is set

i is set

C is set

f is set

(f) is set

i is set

f is set

i is Relation-like Function-like set

rng i is set

((rng i)) is set

i " ((rng i)) is set

dom i is set

i . f is set

f is set

(f) is set

i is set

C is set

({}) is set

f is Relation-like Function-like set

{f} is non empty functional V36() set

({f}) is set

i is Relation-like Function-like set

{f,i} is non empty functional V36() set

({f,i}) is set

C is Relation-like Function-like set

{f,i,C} is V36() set

({f,i,C}) is set

f is set

f is set

f is set

f is set

(f) is set

i is set

(i) is set

C is set

f is Relation-like Function-like set

rng f is set

((rng f)) is set

f " ((rng f)) is set

i is Relation-like Function-like set

dom i is set

i is Relation-like Function-like set

dom i is set

C is Relation-like Function-like set

dom C is set

f is set

i . f is set

f . f is set

dom (f . f) is set

C . f is set

i is Relation-like Function-like set

dom i is set

i is Relation-like Function-like set

dom i is set

C is Relation-like Function-like set

dom C is set

f is set

i . f is set

f . f is set

rng (f . f) is set

C . f is set

meet (rng f) is set

f is set

i is Relation-like Function-like set

dom i is set

i . f is set

(i) is Relation-like Function-like set

dom (i) is set

(i) . f is set

(i) is Relation-like Function-like set

dom (i) is set

(i) . f is set

C is Relation-like Function-like set

dom C is set

rng C is set

rng i is set

((rng i)) is set

i " ((rng i)) is set

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

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

dom ({}) is set

{} " ({}) is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() set

dom ({}) is set

f is set

i is Relation-like Function-like set

f --> i is Relation-like f -defined {i} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:f,{i}:]

{i} is non empty functional V36() set

[:f,{i}:] is Relation-like set

bool [:f,{i}:] is set

((f --> i)) is Relation-like Function-like set

dom i is set

f --> (dom i) is Relation-like f -defined {(dom i)} -valued Function-like constant total quasi_total Element of bool [:f,{(dom i)}:]

{(dom i)} is non empty V36() set

[:f,{(dom i)}:] is Relation-like set

bool [:f,{(dom i)}:] is set

((f --> i)) is Relation-like Function-like set

rng i is set

f --> (rng i) is Relation-like f -defined {(rng i)} -valued Function-like constant total quasi_total Element of bool [:f,{(rng i)}:]

{(rng i)} is non empty V36() set

[:f,{(rng i)}:] is Relation-like set

bool [:f,{(rng i)}:] is set

dom (f --> (dom i)) is set

dom ((f --> i)) is set

rng (f --> i) is trivial V36() set

((rng (f --> i))) is set

(f --> i) " ((rng (f --> i))) is set

C is set

dom (f --> i) is set

(f --> i) " (rng (f --> i)) is set

C is set

(f --> i) . C is Relation-like Function-like set

(f --> (dom i)) . C is set

((f --> i)) . C is set

C is set

(f --> i) . C is Relation-like Function-like set

(f --> (rng i)) . C is set

((f --> i)) . C is set

dom (f --> (rng i)) is set

dom ((f --> i)) is set

f is set

i is Relation-like Function-like set

(i) is set

rng i is set

meet (rng i) is set

dom i is set

C is set

i . C is set

C is set

f is set

i . f is set

f is set

{} --> f is empty Relation-like non-empty empty-yielding {} -defined {f} -valued Function-like one-to-one constant functional total V18() V19() V20() V22() V23() V24() quasi_total Function-yielding V35() V36() V37() V40() Element of bool [:{},{f}:]

{f} is non empty V36() set

[:{},{f}:] is Relation-like V36() set

bool [:{},{f}:] is V36() V40() set

Union ({} --> f) is set

(({} --> f)) is set

rng ({} --> f) is empty trivial with_non-empty_elements Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() set

meet (rng ({} --> f)) is set

union (rng ({} --> f)) is V18() V19() V20() V36() set

f is set

i is set

f --> i is Relation-like f -defined {i} -valued Function-like constant total quasi_total Element of bool [:f,{i}:]

{i} is non empty V36() set

[:f,{i}:] is Relation-like set

bool [:f,{i}:] is set

Union (f --> i) is set

((f --> i)) is set

rng (f --> i) is trivial V36() set

meet (rng (f --> i)) is set

union (rng (f --> i)) is set

f is Relation-like Function-like set

uncurry f is Relation-like Function-like set

i is set

C is set

(uncurry f) . (i,C) is set

[i,C] is V25() set

{i,C} is non empty V36() set

{i} is non empty V36() set

{{i,C},{i}} is non empty V36() V40() set

(uncurry f) . [i,C] is set

f is set

i is set

C is set

f is Relation-like Function-like set

dom f is set

i --> f is Relation-like i -defined {f} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:i,{f}:]

{f} is non empty functional V36() set

[:i,{f}:] is Relation-like set

bool [:i,{f}:] is set

((i --> f),f,C) is set

uncurry (i --> f) is Relation-like Function-like set

(uncurry (i --> f)) . (f,C) is set

[f,C] is V25() set

{f,C} is non empty V36() set

{f} is non empty V36() set

{{f,C},{f}} is non empty V36() V40() set

(uncurry (i --> f)) . [f,C] is set

f . C is set

(i --> f) . f is Relation-like Function-like set

dom (i --> f) is set

f is Relation-like Function-like set

uncurry' f is Relation-like Function-like set

(f) is Relation-like Function-like set

((f)) is set

rng (f) is set

meet (rng (f)) is set

dom f is set

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

(uncurry' f) | [:((f)),(dom f):] is Relation-like Function-like set

curry ((uncurry' f) | [:((f)),(dom f):]) is Relation-like Function-like set

f is Relation-like Function-like set

(f) is Relation-like Function-like set

uncurry' f is Relation-like Function-like set

(f) is Relation-like Function-like set

((f)) is set

rng (f) is set

meet (rng (f)) is set

dom f is set

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

(uncurry' f) | [:((f)),(dom f):] is Relation-like Function-like set

curry ((uncurry' f) | [:((f)),(dom f):]) is Relation-like Function-like set

dom (f) is set

rng (f) is set

(f) is Relation-like Function-like set

product (f) is set

dom ((uncurry' f) | [:((f)),(dom f):]) is set

dom (f) is set

rng f is set

((rng f)) is set

f " ((rng f)) is set

the Element of rng (f) is Element of rng (f)

f is set

cf is set

(f) . cf is set

f . cf is set

ccf is Relation-like Function-like set

dom ccf is set

[f,cf] is V25() set

{f,cf} is non empty V36() set

{f} is non empty V36() set

{{f,cf},{f}} is non empty V36() V40() set

dom (uncurry' f) is set

(dom (uncurry' f)) /\ [:((f)),(dom f):] is Relation-like set

dom (dom ((uncurry' f) | [:((f)),(dom f):])) is set

dom (f) is set

C is set

dom (uncurry' f) is set

(dom (uncurry' f)) /\ [:((f)),(dom f):] is Relation-like set

uncurry f is Relation-like Function-like set

~ (uncurry f) is Relation-like Function-like set

f is set

(f) . f is set

cf is Relation-like Function-like set

dom cf is set

{f} is non empty V36() set

rng (dom ((uncurry' f) | [:((f)),(dom f):])) is set

[:{f},(rng (dom ((uncurry' f) | [:((f)),(dom f):]))):] is Relation-like set

(dom ((uncurry' f) | [:((f)),(dom f):])) /\ [:{f},(rng (dom ((uncurry' f) | [:((f)),(dom f):]))):] is Relation-like set

rng ((dom ((uncurry' f) | [:((f)),(dom f):])) /\ [:{f},(rng (dom ((uncurry' f) | [:((f)),(dom f):]))):]) is set

ccf is set

[f,ccf] is V25() set

{f,ccf} is non empty V36() set

{{f,ccf},{f}} is non empty V36() V40() set

[ccf,f] is V25() set

{ccf,f} is non empty V36() set

{ccf} is non empty V36() set

{{ccf,f},{ccf}} is non empty V36() V40() set

dom (uncurry f) is set

uf is set

x is set

[uf,x] is V25() set

{uf,x} is non empty V36() set

{uf} is non empty V36() set

{{uf,x},{uf}} is non empty V36() V40() set

ucf is Relation-like Function-like set

f . uf is set

dom ucf is set

f . ccf is set

ccf is set

f . ccf is set

uf is Relation-like Function-like set

dom uf is set

(f) . ccf is set

[ccf,f] is V25() set

{ccf,f} is non empty V36() set

{ccf} is non empty V36() set

{{ccf,f},{ccf}} is non empty V36() V40() set

dom (uncurry f) is set

[f,ccf] is V25() set

{f,ccf} is non empty V36() set

{{f,ccf},{f}} is non empty V36() V40() set

ccf is set

f . ccf is set

uf is Relation-like Function-like set

dom uf is set

(f) . ccf is set

uf . f is set

rng uf is set

cf . ccf is set

((uncurry' f) | [:((f)),(dom f):]) . (f,ccf) is set

[f,ccf] is V25() set

{f,ccf} is non empty V36() set

{{f,ccf},{f}} is non empty V36() V40() set

((uncurry' f) | [:((f)),(dom f):]) . [f,ccf] is set

(uncurry' f) . (f,ccf) is set

(uncurry' f) . [f,ccf] is set

(f) . ccf is set

f is set

i is Relation-like Function-like set

(i) is Relation-like Function-like set

uncurry' i is Relation-like Function-like set

(i) is Relation-like Function-like set

((i)) is set

rng (i) is set

meet (rng (i)) is set

dom i is set

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

(uncurry' i) | [:((i)),(dom i):] is Relation-like Function-like set

curry ((uncurry' i) | [:((i)),(dom i):]) is Relation-like Function-like set

dom (i) is set

(i) . f is set

rng (i) is set

(i) is Relation-like Function-like set

product (i) is set

dom (i) is set

C is Relation-like Function-like set

dom C is set

f is set

i is Relation-like Function-like set

(i) is Relation-like Function-like set

uncurry' i is Relation-like Function-like set

(i) is Relation-like Function-like set

((i)) is set

rng (i) is set

meet (rng (i)) is set

dom i is set

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

(uncurry' i) | [:((i)),(dom i):] is Relation-like Function-like set

curry ((uncurry' i) | [:((i)),(dom i):]) is Relation-like Function-like set

dom (i) is set

(i) . f is set

rng i is set

((rng i)) is set

i " ((rng i)) is set

uncurry i is Relation-like Function-like set

dom (uncurry i) is set

C is Relation-like Function-like set

dom C is set

rng (i) is set

(i) is Relation-like Function-like set

product (i) is set

dom (i) is set

f is set

[f,f] is V25() set

{f,f} is non empty V36() set

{f} is non empty V36() set

{{f,f},{f}} is non empty V36() V40() set

C . f is set

(uncurry i) . (f,f) is set

(uncurry i) . [f,f] is set

[f,f] is V25() set

{f,f} is non empty V36() set

{f} is non empty V36() set

{{f,f},{f}} is non empty V36() V40() set

dom ((uncurry' i) | [:((i)),(dom i):]) is set

dom (uncurry' i) is set

(dom (uncurry' i)) /\ [:((i)),(dom i):] is Relation-like set

((uncurry' i) | [:((i)),(dom i):]) . (f,f) is set

((uncurry' i) | [:((i)),(dom i):]) . [f,f] is set

(uncurry' i) . (f,f) is set

(uncurry' i) . [f,f] is set

~ (uncurry i) is Relation-like Function-like set

f is set

i is Relation-like Function-like set

(i) is Relation-like Function-like set

uncurry' i is Relation-like Function-like set

(i) is Relation-like Function-like set

((i)) is set

rng (i) is set

meet (rng (i)) is set

dom i is set

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

(uncurry' i) | [:((i)),(dom i):] is Relation-like Function-like set

curry ((uncurry' i) | [:((i)),(dom i):]) is Relation-like Function-like set

dom (i) is set

rng i is set

C is Relation-like Function-like set

dom C is set

f is set

i . f is set

dom (i) is set

(i) . f is set

f is set

i is Relation-like Function-like set

C is Relation-like Function-like set

rng C is set

(C) is Relation-like Function-like set

uncurry' C is Relation-like Function-like set

(C) is Relation-like Function-like set

((C)) is set

rng (C) is set

meet (rng (C)) is set

dom C is set

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

(uncurry' C) | [:((C)),(dom C):] is Relation-like Function-like set

curry ((uncurry' C) | [:((C)),(dom C):]) is Relation-like Function-like set

dom (C) is set

f is set

C . f is set

f is set

dom (C) is set

((rng C)) is set

C " ((rng C)) is set

C . f is set

cf is Relation-like Function-like set

dom cf is set

(C) . f is set

f is set

i is set

C is Relation-like Function-like set

dom C is set

C . f is set

(C) is Relation-like Function-like set

uncurry' C is Relation-like Function-like set

(C) is Relation-like Function-like set

((C)) is set

rng (C) is set

meet (rng (C)) is set

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

(uncurry' C) | [:((C)),(dom C):] is Relation-like Function-like set

curry ((uncurry' C) | [:((C)),(dom C):]) is Relation-like Function-like set

dom (C) is set

(C) . i is set

f is Relation-like Function-like set

f . i is set

cf is Relation-like Function-like set

cf . f is set

dom cf is set

rng C is set

((rng C)) is set

C " ((rng C)) is set

uncurry C is Relation-like Function-like set

(uncurry C) . (f,i) is set

[f,i] is V25() set

{f,i} is non empty V36() set

{f} is non empty V36() set

{{f,i},{f}} is non empty V36() V40() set

(uncurry C) . [f,i] is set

dom f is set

f is set

i is set

C is Relation-like Function-like set

dom C is set

C . f is set

(C) is Relation-like Function-like set

uncurry' C is Relation-like Function-like set

(C) is Relation-like Function-like set

((C)) is set

rng (C) is set

meet (rng (C)) is set

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

(uncurry' C) | [:((C)),(dom C):] is Relation-like Function-like set

curry ((uncurry' C) | [:((C)),(dom C):]) is Relation-like Function-like set

dom (C) is set

(C,f,i) is set

uncurry C is Relation-like Function-like set

(uncurry C) . (f,i) is set

[f,i] is V25() set

{f,i} is non empty V36() set

{f} is non empty V36() set

{{f,i},{f}} is non empty V36() V40() set

(uncurry C) . [f,i] is set

((C),i,f) is set

uncurry (C) is Relation-like Function-like set

(uncurry (C)) . (i,f) is set

[i,f] is V25() set

{i,f} is non empty V36() set

{i} is non empty V36() set

{{i,f},{i}} is non empty V36() V40() set

(uncurry (C)) . [i,f] is set

(C) . i is set

cf is Relation-like Function-like set

dom cf is set

rng C is set

((rng C)) is set

C " ((rng C)) is set

f is Relation-like Function-like set

dom f is set

f . i is set

cf . f is set

f is Relation-like Function-like set

(f) is Relation-like Function-like set

product (f) is set

rng f is set

((rng f)) is set

f " ((rng f)) is set

uncurry f is Relation-like Function-like set

i is set

dom (f) is set

C is Relation-like Function-like set

dom C is set

f is Relation-like Function-like set

dom f is set

cf is set

ccf is set

f . ccf is set

C . ccf is set

(uncurry f) . (ccf,(C . ccf)) is set

[ccf,(C . ccf)] is V25() set

{ccf,(C . ccf)} is non empty V36() set

{ccf} is non empty V36() set

{{ccf,(C . ccf)},{ccf}} is non empty V36() V40() set

(uncurry f) . [ccf,(C . ccf)] is set

i is Relation-like Function-like set

dom i is set

C is Relation-like Function-like set

i . C is set

f is Relation-like Function-like set

cf is Relation-like Function-like set

dom cf is set

i is Relation-like Function-like set

dom i is set

C is Relation-like Function-like set

dom C is set

f is set

dom (f) is set

cf is Relation-like Function-like set

dom cf is set

C . cf is set

ccf is Relation-like Function-like set

dom ccf is set

i . cf is set

uf is Relation-like Function-like set

dom uf is set

ucf is set

uf . ucf is set

cf . ucf is set

(uncurry f) . (ucf,(cf . ucf)) is set

[ucf,(cf . ucf)] is V25() set

{ucf,(cf . ucf)} is non empty V36() set

{ucf} is non empty V36() set

{{ucf,(cf . ucf)},{ucf}} is non empty V36() V40() set

(uncurry f) . [ucf,(cf . ucf)] is set

ccf . ucf is set

i . f is set

C . f is set

f is set

i is Relation-like Function-like set

dom i is set

i . f is set

C is Relation-like Function-like set

(C) is Relation-like Function-like set

product (C) is set

(C) is Relation-like Function-like set

((C),i,f) is set

uncurry (C) is Relation-like Function-like set

(uncurry (C)) . (i,f) is set

[i,f] is V25() set

{i,f} is non empty V36() set

{i} is non empty functional V36() set

{{i,f},{i}} is non empty V36() V40() set

(uncurry (C)) . [i,f] is set

(C,f,(i . f)) is set

uncurry C is Relation-like Function-like set

(uncurry C) . (f,(i . f)) is set

[f,(i . f)] is V25() set

{f,(i . f)} is non empty V36() set

{f} is non empty V36() set

{{f,(i . f)},{f}} is non empty V36() V40() set

(uncurry C) . [f,(i . f)] is set

dom (C) is set

rng C is set

((rng C)) is set

C " ((rng C)) is set

(C) . i is set

f is Relation-like Function-like set

dom f is set

dom (C) is set

f . f is set

f is Relation-like Function-like set

(f) is Relation-like Function-like set

rng (f) is set

(f) is Relation-like Function-like set

product (f) is set

i is set

dom (f) is set

C is set

(f) . C is set

(f) is Relation-like Function-like set

product (f) is set

dom (f) is set

f is Relation-like Function-like set

dom f is set

(f) . f is set

rng f is set

((rng f)) is set

f " ((rng f)) is set

uncurry f is Relation-like Function-like set

cf is Relation-like Function-like set

dom cf is set

dom (f) is set

ccf is set

f . ccf is set

f . ccf is set

(f) . ccf is set

dom f is set

(f) . ccf is set

uf is Relation-like Function-like set

rng uf is set

dom uf is set

uf . (f . ccf) is set

(uncurry f) . (ccf,(f . ccf)) is set

[ccf,(f . ccf)] is V25() set

{ccf,(f . ccf)} is non empty V36() set

{ccf} is non empty V36() set

{{ccf,(f . ccf)},{ccf}} is non empty V36() V40() set

(uncurry f) . [ccf,(f . ccf)] is set

cf . ccf is set

f is set

i is Relation-like Function-like set

dom i is set

i . f is set

(i) is Relation-like Function-like set

product (i) is set

(i) is Relation-like Function-like set

(i) is Relation-like Function-like set

product (i) is set

C is Relation-like Function-like set

dom C is set

f is Relation-like Function-like set

(i) . f is set

f . f is set

C . (f . f) is set

cf is Relation-like Function-like set

cf . f is set

rng i is set

((rng i)) is set

i " ((rng i)) is set

dom (i) is set

(i) . f is set

ccf is Relation-like Function-like set

dom ccf is set

uncurry i is Relation-like Function-like set

(uncurry i) . (f,(f . f)) is set

[f,(f . f)] is V25() set

{f,(f . f)} is non empty V36() set

{f} is non empty V36() set

{{f,(f . f)},{f}} is non empty V36() V40() set

(uncurry i) . [f,(f . f)] is set

ccf is Relation-like Function-like set

dom ccf is set

rng (i) is set

dom (i) is set

f is Relation-like Function-like set

(f) is Relation-like Function-like set

product (f) is set

(f) is Relation-like Function-like set

rng (f) is set

i is set

(f) is Relation-like Function-like set

dom (f) is set

C is Relation-like Function-like set

dom C is set

rng f is set

((rng f)) is set

f " ((rng f)) is set

f is Relation-like Function-like set

dom f is set

product (f) is set

dom (f) is set

dom (f) is set

cf is set

rng f is set

ccf is set

f . ccf is set

f . ccf is set

dom f is set

(f) . ccf is set

uf is Relation-like Function-like set

rng uf is set

C . ccf is set

dom uf is set

(f) . ccf is set

ucf is set

uf . ucf is set

cf is non empty set

ccf is Relation-like Function-like set

dom ccf is set

f * ccf is Relation-like Function-like set

dom (f * ccf) is set

uf is set

(f * ccf) . uf is set

f . uf is set

ccf . (f . uf) is set

(f) . uf is set

(f) . (f * ccf) is set

uncurry f is Relation-like Function-like set

uf is Relation-like Function-like set

dom uf is set

ucf is set

uf . ucf is set

(f * ccf) . ucf is set

(uncurry f) . (ucf,((f * ccf) . ucf)) is set

[ucf,((f * ccf) . ucf)] is V25() set

{ucf,((f * ccf) . ucf)} is non empty V36() set

{ucf} is non empty V36() set

{{ucf,((f * ccf) . ucf)},{ucf}} is non empty V36() V40() set

(uncurry f) . [ucf,((f * ccf) . ucf)] is set

f . ucf is set

ccf . (f . ucf) is set

f . ucf is set

C . ucf is set

x is Relation-like Function-like set

x . ((f * ccf) . ucf) is set

(f) . ucf is set

dom x is set

(f) . {} is set

cf is Relation-like Function-like set

dom cf is set

f is Relation-like Function-like set

(f) is Relation-like Function-like set

rng (f) is set

(f) is Relation-like Function-like set

product (f) is set

f is Relation-like Function-like set

rng f is set

(f) is Relation-like Function-like set

(f) is Relation-like Function-like set

product (f) is set

the Element of product (f) is Element of product (f)

dom (f) is set

((rng f)) is set

f " ((rng f)) is set

rng (f) is set

C is set

(f) . C is set

f . C is set

dom f is set

f is Relation-like Function-like set

dom f is set

C is Relation-like Function-like set

dom C is set

dom (f) is set

f is Relation-like Function-like set

cf is set

f . cf is set

ccf is set

dom f is set

f . ccf is set

uf is set

f . uf is set

ucf is Relation-like Function-like set

dom ucf is set

x is set

ucf . x is set

C . x is set

(f) . x is set

(f) . ucf is set

uncurry f is Relation-like Function-like set

x is Relation-like Function-like set

dom x is set

g is Relation-like Function-like set

dom g is set

h is set

g . h is set

C . h is set

(f) . h is set

(f) . g is set

h is Relation-like Function-like set

dom h is set

y is set

h . y is set

g . y is set

(uncurry f) . (y,(g . y)) is set

[y,(g . y)] is V25() set

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

{y} is non empty V36() set

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

(uncurry f) . [y,(g . y)] is set

x . y is set

ucf . y is set

(uncurry f) . (y,(ucf . y)) is set

[y,(ucf . y)] is V25() set

{y,(ucf . y)} is non empty V36() set

{{y,(ucf . y)},{y}} is non empty V36() V40() set

(uncurry f) . [y,(ucf . y)] is set

C . y is set

ucf . cf is set

f is set

(f) . f is set

cf is set

(f) . cf is set

ccf is Relation-like Function-like set

dom ccf is set

uf is Relation-like Function-like set

dom uf is set

(f) . ccf is set

uncurry f is Relation-like Function-like set

ucf is Relation-like Function-like set

dom ucf is set

(f) . uf is set

x is Relation-like Function-like set

dom x is set

g is set

f . g is set

h is Relation-like Function-like set

dom h is set

(f) . g is set

ccf . g is set

uf . g is set

ucf . g is set

(uncurry f) . (g,(ccf . g)) is set

[g,(ccf . g)] is V25() set

{g,(ccf . g)} is non empty V36() set

{g} is non empty V36() set

{{g,(ccf . g)},{g}} is non empty V36() V40() set

(uncurry f) . [g,(ccf . g)] is set

h . (ccf . g) is set

x . g is set

(uncurry f) . (g,(uf . g)) is set

[g,(uf . g)] is V25() set

{g,(uf . g)} is non empty V36() set

{{g,(uf . g)},{g}} is non empty V36() V40() set

(uncurry f) . [g,(uf . g)] is set

h . (uf . g) is set

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

(({})) is set

rng ({}) is set

meet (rng ({})) is set

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

(uncurry' {}) | [:(({})),(dom {}):] is Relation-like Function-like set

curry ((uncurry' {}) | [:(({})),(dom {}):]) is Relation-like Function-like set

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

{} .--> {} is Relation-like {{}} -defined Function-like one-to-one Function-yielding V35() V36() set

{{}} --> {} is non empty Relation-like {{}} -defined {{}} -valued Function-like constant total quasi_total Function-yielding V35() V36() Element of bool [:{{}},{{}}:]

[:{{}},{{}}:] is Relation-like V36() set

bool [:{{}},{{}}:] is V36() V40() set

dom ({}) is set

{} " ({}) is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() set

product ({}) is set

f is set

({}) . {} is set

((rng {})) is set

{} " ((rng {})) is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() set

({}) . f is set

i is Relation-like Function-like set

dom i is set

meet {} is set

dom ({}) is set

dom ({}) is set

f is set

i is Relation-like Function-like set

f --> i is Relation-like f -defined {i} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:f,{i}:]

{i} is non empty functional V36() set

[:f,{i}:] is Relation-like set

bool [:f,{i}:] is set

((f --> i)) is Relation-like Function-like set

uncurry' (f --> i) is Relation-like Function-like set

((f --> i)) is Relation-like Function-like set

(((f --> i))) is set

rng ((f --> i)) is set

meet (rng ((f --> i))) is set

dom (f --> i) is set

[:(((f --> i))),(dom (f --> i)):] is Relation-like set

(uncurry' (f --> i)) | [:(((f --> i))),(dom (f --> i)):] is Relation-like Function-like set

curry ((uncurry' (f --> i)) | [:(((f --> i))),(dom (f --> i)):]) is Relation-like Function-like set

dom ((f --> i)) is set

dom i is set

f --> (dom i) is Relation-like f -defined {(dom i)} -valued Function-like constant total quasi_total Element of bool [:f,{(dom i)}:]

{(dom i)} is non empty V36() set

[:f,{(dom i)}:] is Relation-like set

bool [:f,{(dom i)}:] is set

((f --> (dom i))) is set

rng (f --> (dom i)) is trivial V36() set

meet (rng (f --> (dom i))) is set

rng ((f --> i)) is set

((f --> i)) is Relation-like Function-like set

product ((f --> i)) is set

rng i is set

f --> (rng i) is Relation-like f -defined {(rng i)} -valued Function-like constant total quasi_total Element of bool [:f,{(rng i)}:]

{(rng i)} is non empty V36() set

[:f,{(rng i)}:] is Relation-like set

bool [:f,{(rng i)}:] is set

C is set

((f --> i)) . C is set

i . C is set

f --> (i . C) is Relation-like f -defined {(i . C)} -valued Function-like constant total quasi_total Element of bool [:f,{(i . C)}:]

{(i . C)} is non empty V36() set

[:f,{(i . C)}:] is Relation-like set

bool [:f,{(i . C)}:] is set

dom (f --> (rng i)) is set

f is Relation-like Function-like set

dom f is set

cf is set

f . cf is set

uncurry (f --> i) is Relation-like Function-like set

(uncurry (f --> i)) . (cf,C) is set

[cf,C] is V25() set

{cf,C} is non empty V36() set

{cf} is non empty V36() set

{{cf,C},{cf}} is non empty V36() V40() set

(uncurry (f --> i)) . [cf,C] is set

(f --> i) . cf is Relation-like Function-like set

(f --> (i . C)) . cf is set

dom (f --> (i . C)) is set

f is set

i is Relation-like Function-like set

f --> i is Relation-like f -defined {i} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:f,{i}:]

{i} is non empty functional V36() set

[:f,{i}:] is Relation-like set

bool [:f,{i}:] is set

((f --> i)) is Relation-like Function-like set

dom ((f --> i)) is set

dom i is set

Funcs (f,(dom i)) is functional set

rng ((f --> i)) is set

rng i is set

Funcs (f,(rng i)) is functional set

f --> (dom i) is Relation-like f -defined {(dom i)} -valued Function-like constant total quasi_total Element of bool [:f,{(dom i)}:]

{(dom i)} is non empty V36() set

[:f,{(dom i)}:] is Relation-like set

bool [:f,{(dom i)}:] is set

product (f --> (dom i)) is set

((f --> i)) is Relation-like Function-like set

((f --> i)) is Relation-like Function-like set

f --> (rng i) is Relation-like f -defined {(rng i)} -valued Function-like constant total quasi_total Element of bool [:f,{(rng i)}:]

{(rng i)} is non empty V36() set

[:f,{(rng i)}:] is Relation-like set

bool [:f,{(rng i)}:] is set

product (f --> (rng i)) is set

C is Relation-like Function-like set

((f --> i)) . C is set

C * i is Relation-like Function-like set

rng (f --> i) is trivial V36() set

((rng (f --> i))) is set

(f --> i) " ((rng (f --> i))) is set

uncurry (f --> i) is Relation-like Function-like set

f is Relation-like Function-like set

dom f is set

dom (f --> (dom i)) is set

dom (C * i) is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

dom (f --> i) is set

cf is set

f . cf is set

C . cf is set

(uncurry (f --> i)) . (cf,(C . cf)) is set

[cf,(C . cf)] is V25() set

{cf,(C . cf)} is non empty V36() set

{cf} is non empty V36() set

{{cf,(C . cf)},{cf}} is non empty V36() V40() set

(uncurry (f --> i)) . [cf,(C . cf)] is set

(f --> i) . cf is Relation-like Function-like set

rng C is set

(C * i) . cf is set

i . (C . cf) is set

ccf is Relation-like Function-like set

dom ccf is set

rng ccf is set

ccf is Relation-like Function-like set

dom ccf is set

rng ccf is set

f is set

i is Relation-like Function-like set

dom i is set

product i is set

C is Relation-like Function-like set

dom C is set

product C is set

f is set

i . f is set

C . f is set

cf is Relation-like Function-like set

dom cf is set

rng cf is set

f is Relation-like Function-like set

dom f is set

cf is set

f . cf is set

i . cf is set

C . cf is set

(f) is Relation-like Function-like set

(f) . cf is set

ccf is Relation-like Function-like set

dom ccf is set

rng ccf is set

cf is set

rng f is set

ccf is set

f . ccf is set

i . ccf is set

C . ccf is set

uf is Relation-like Function-like set

dom uf is set

rng uf is set

((rng f)) is set

f " ((rng f)) is set

dom (f) is set

cf is set

f . cf is set

i . cf is set

C . cf is set

(f) is Relation-like Function-like set

(f) . cf is set