:: FUNCT_6 semantic presentation

K64() is non empty V18() V19() V20() 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

is non empty functional V36() V40() set

product f is set
dom f is set
Union f is set
Funcs ((dom f),()) is functional set
i is 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

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

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

curry (~ (~ f)) is Relation-like Function-like set
dom (curry (~ (~ f))) is set
dom (~ (~ f)) is set
dom (dom (~ (~ f))) is set
dom () 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
() . i is set
(curry' (~ f)) . i is 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

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 () is set

dom (~ (~ ())) 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 . 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 (~ ()) is set
i is set
dom (~ ()) 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 (~ ()) 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
(~ ()) . (C,f) is set
(~ ()) . [C,f] is set
() . (f,C) is set
() . [f,C] is set
(~ (~ ())) . (f,C) is set
(~ (~ ())) . [f,C] is set
() . i is set
(~ (~ ())) . i is set
f is set
i is set
[:f,i:] is Relation-like set
C is set

{C} is non empty V36() set
[:[:f,i:],{C}:] is Relation-like set
bool [:[:f,i:],{C}:] is set

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

{(i --> C)} is non empty functional V36() set
[:f,{(i --> C)}:] is Relation-like set
bool [:f,{(i --> C)}:] is set

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

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

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

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

{C} is non empty V36() set

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

{(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 set
bool [:[:f,i:],{C}:] is set
uncurry' (f --> (i --> C)) is Relation-like Function-like set

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

(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

dom i is set
i . f is set

rng () is set

rng () is 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 non empty functional V36() set

bool [:f,{i}:] is 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

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 non empty functional V36() set

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

rng (uncurry (f --> i)) is set
rng i is 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

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

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

dom cf is set
rng cf is set
dom () is set
dom () is 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

dom () is set
dom () is set

dom cf is set
rng cf is set
rng () is set
rng () is 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

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

rng ccf is set
dom ccf is set

dom (uncurry' ccf) is set

dom uf is set
rng uf is set

dom ucf is set
rng ucf is set
uf is set
ucf is set
ccf . ucf is set

dom g is set
rng g 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
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

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

dom h is set
rng h is 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

dom [:f,i:] is set
dom f is set
dom (dom f) is set

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

dom cf is set
rng cf is set
rng [:f,i:] is set
rng (dom f) is set

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

dom cf is set
rng cf is set
rng () is set
dom () is set
dom () is 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

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

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

dom cf is set
rng cf is set
rng () is set
rng () is 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

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

rng ccf is set
dom ccf is set

dom (uncurry' ccf) is set

dom uf is set
rng uf is set

dom ucf is set
rng ucf is set
uf is set
ucf is set
ccf . ucf is set

dom g is set
rng g is 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

dom h is set
rng h is 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

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 non empty functional V36() set
({f}) is set

{f,i} is non empty functional V36() set
({f,i}) is 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

rng f is set
((rng f)) is set
f " ((rng f)) is set

dom i is set

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

dom i is set

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

dom i is set
i . f is set

dom (i) is set
(i) . f is set

dom (i) is set
(i) . f is set

dom C is set
rng C is set
rng i is set
((rng i)) is set
i " ((rng i)) is set

dom ({}) is set

dom ({}) is set
f is set

{i} is non empty functional V36() set

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

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

{(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 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 non empty V36() set

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

meet (rng ()) is set
union (rng ()) is V18() V19() V20() V36() set
f is set
i is set

{i} is non empty V36() 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

i is set
C is set
() . (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
() . [i,C] is set
f is set
i is set
C is set

dom f is set

{f} is non empty functional V36() set

bool [:i,{f}:] is set
((i --> f),f,C) is 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 set
rng (f) is set
meet (rng (f)) is set
dom f is set
[:((f)),(dom f):] is Relation-like set
() | [:((f)),(dom f):] is Relation-like Function-like set
curry (() | [:((f)),(dom 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
() | [:((f)),(dom f):] is Relation-like Function-like set
curry (() | [:((f)),(dom f):]) is Relation-like Function-like set
dom (f) is set
rng (f) is set

product (f) is set
dom (() | [:((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

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 () is set
(dom ()) /\ [:((f)),(dom f):] is Relation-like set
dom (dom (() | [:((f)),(dom f):])) is set
dom (f) is set
C is set
dom () is set
(dom ()) /\ [:((f)),(dom f):] is Relation-like set

f is set
(f) . f is set

dom cf is set
{f} is non empty V36() set
rng (dom (() | [:((f)),(dom f):])) is set
[:{f},(rng (dom (() | [:((f)),(dom f):]))):] is Relation-like set
(dom (() | [:((f)),(dom f):])) /\ [:{f},(rng (dom (() | [:((f)),(dom f):]))):] is Relation-like set
rng ((dom (() | [:((f)),(dom f):])) /\ [:{f},(rng (dom (() | [:((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 () 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

f . uf is set
dom ucf is set
f . ccf is set
ccf is set
f . ccf is 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 () 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

dom uf is set
(f) . ccf is set
uf . f is set
rng uf is set
cf . ccf is set
(() | [:((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
(() | [:((f)),(dom f):]) . [f,ccf] is set
() . (f,ccf) is set
() . [f,ccf] is set
(f) . ccf is set
f is set

((i)) is set
rng (i) is set
meet (rng (i)) is set
dom i is set
[:((i)),(dom i):] is Relation-like set
() | [:((i)),(dom i):] is Relation-like Function-like set
curry (() | [:((i)),(dom i):]) is Relation-like Function-like set
dom (i) is set
(i) . f is set
rng (i) is set

product (i) is set
dom (i) is set

dom C is set
f is set

((i)) is set
rng (i) is set
meet (rng (i)) is set
dom i is set
[:((i)),(dom i):] is Relation-like set
() | [:((i)),(dom i):] is Relation-like Function-like set
curry (() | [:((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

dom () is set

dom C is set
rng (i) is 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
() . (f,f) is set
() . [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 (() | [:((i)),(dom i):]) is set
dom () is set
(dom ()) /\ [:((i)),(dom i):] is Relation-like set
(() | [:((i)),(dom i):]) . (f,f) is set
(() | [:((i)),(dom i):]) . [f,f] is set
() . (f,f) is set
() . [f,f] is set

f is set

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

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

rng C is set

((C)) is set
rng (C) is set
meet (rng (C)) is set
dom C is set
[:((C)),(dom C):] is Relation-like set
() | [:((C)),(dom C):] is Relation-like Function-like set
curry (() | [:((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

dom cf is set
(C) . f is set
f is set
i is set

dom C is set
C . f is set

((C)) is set
rng (C) is set
meet (rng (C)) is set
[:((C)),(dom C):] is Relation-like set
() | [:((C)),(dom C):] is Relation-like Function-like set
curry (() | [:((C)),(dom C):]) is Relation-like Function-like set
dom (C) is set
(C) . i is set

f . i is set

cf . f is set
dom cf is set
rng C is set
((rng C)) is set
C " ((rng C)) is set

() . (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
() . [f,i] is set
dom f is set
f is set
i is set

dom C is set
C . f is set

((C)) is set
rng (C) is set
meet (rng (C)) is set
[:((C)),(dom C):] is Relation-like set
() | [:((C)),(dom C):] is Relation-like Function-like set
curry (() | [:((C)),(dom C):]) is Relation-like Function-like set
dom (C) is set
(C,f,i) is set

() . (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
() . [f,i] is set
((C),i,f) is 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

dom cf is set
rng C is set
((rng C)) is set
C " ((rng C)) is set

dom f is set
f . i is set
cf . f is set

product (f) is set
rng f is set
((rng f)) is set
f " ((rng f)) is set

i is set
dom (f) is set

dom C is set

dom f is set
cf is set
ccf is set
f . ccf is set
C . ccf is set
() . (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
() . [ccf,(C . ccf)] is set

dom i is set

i . C is set

dom cf is set

dom i is set

dom C is set
f is set
dom (f) is set

dom cf is set
C . cf is set

dom ccf is set
i . cf is set

dom uf is set
ucf is set
uf . ucf is set
cf . ucf is set
() . (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
() . [ucf,(cf . ucf)] is set
ccf . ucf is set
i . f is set
C . f is set
f is set

dom i is set
i . f is set

product (C) is set

((C),i,f) is 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

() . (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
() . [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

dom f is set
dom (C) is set
f . f is set

rng (f) is set

product (f) is set
i is set
dom (f) is set
C is set
(f) . C is set

product (f) is set
dom (f) is set

dom f is set
(f) . f is set
rng f is set
((rng f)) is set
f " ((rng f)) is 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

rng uf is set
dom uf is set
uf . (f . ccf) is set
() . (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
() . [ccf,(f . ccf)] is set
cf . ccf is set
f is set

dom i is set
i . f is set

product (i) is set

product (i) is set

dom C is set

(i) . f is set
f . f is set
C . (f . f) is 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

dom ccf is set

() . (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
() . [f,(f . f)] is set

dom ccf is set
rng (i) is set
dom (i) is set

product (f) is set

rng (f) is set
i is set

dom (f) is set

dom C is set
rng f is set
((rng f)) is set
f " ((rng f)) is 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

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

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

dom uf is set
ucf is set
uf . ucf is set
(f * ccf) . ucf is set
() . (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
() . [ucf,((f * ccf) . ucf)] is set
f . ucf is set
ccf . (f . ucf) is set
f . ucf is set
C . ucf is set

x . ((f * ccf) . ucf) is set
(f) . ucf is set
dom x is set
(f) . {} is set

dom cf is set

rng (f) is set

product (f) is set

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

dom f is set

dom C is set
dom (f) is 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

dom ucf is set
x is set
ucf . x is set
C . x is set
(f) . x is set
(f) . ucf is set

dom x is set

dom g is set
h is set
g . h is set
C . h is set
(f) . h is set
(f) . g is set

dom h is set
y is set
h . y is set
g . y is set
() . (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
() . [y,(g . y)] is set
x . y is set
ucf . y is set
() . (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
() . [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

dom ccf is set

dom uf is set
(f) . ccf is set

dom ucf is set
(f) . uf is set

dom x is set
g is set
f . g is set

dom h is set
(f) . g is set
ccf . g is set
uf . g is set
ucf . g is set
() . (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
() . [g,(ccf . g)] is set
h . (ccf . g) is set
x . g is set
() . (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
() . [g,(uf . g)] is set
h . (uf . g) is set

(({})) is set
rng ({}) is set
meet (rng ({})) is set
[:(({})),():] is Relation-like set
() | [:(({})),():] is Relation-like Function-like set
curry (() | [:(({})),():]) is Relation-like Function-like set

bool is V36() V40() set
dom ({}) is set

product ({}) is set
f is set
({}) . {} is set
(()) is set

({}) . f is set

dom i is set

dom ({}) is set
dom ({}) is set
f is set

{i} is non empty functional V36() set

bool [:f,{i}:] is set
((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

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

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

dom f is set
cf is set
f . cf is 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 non empty functional V36() 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

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

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

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

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

dom f is set
dom (f --> (dom i)) is set
dom (C * i) is 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

dom ccf is set
rng ccf is set

dom ccf is set
rng ccf is set
f is set

dom i is set
product i is set

dom C is set
product C is set
f is set
i . f is set
C . f is set

dom cf is set
rng cf is set

dom f is set
cf is set
f . cf is set
i . cf is set
C . cf is set

(f) . cf is 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

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) . cf is set