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
ccf is Relation-like Function-like set
dom ccf is set
rng ccf is set
dom (f) is set
cf is set
f . cf is set
i . cf is set
C . cf is set
rng i is set
ccf is Relation-like Function-like set
dom ccf is set
rng ccf is set
rng C is set
ccf is Relation-like Function-like set
dom ccf is set
rng ccf is set
cf is Relation-like Function-like 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
(f) is Relation-like Function-like set
dom (f) is set
rng (f) is set
f is Relation-like Function-like set
dom f is set
product f is set
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
product C is set
i " is Relation-like Function-like set
(i ") * i is Relation-like Function-like set
id (dom C) is Relation-like dom C -defined dom C -valued Function-like one-to-one total quasi_total Element of bool [:(dom C),(dom C):]
[:(dom C),(dom C):] is Relation-like set
bool [:(dom C),(dom C):] is set
i * C is Relation-like Function-like set
dom (i * C) is set
cf is set
f . cf is set
i . cf is set
C . (i . cf) is set
(i * C) . cf is set
product (i * C) is set
cf is set
ccf is Relation-like Function-like set
dom ccf is set
ccf is Relation-like Function-like set
(i ") * ccf is Relation-like Function-like set
cf is Relation-like Function-like set
dom cf is set
rng (i ") is set
ccf is set
cf . ccf is set
uf is set
cf . uf is set
ucf is Relation-like Function-like set
(i ") * ucf is Relation-like Function-like set
dom ucf is set
x is Relation-like Function-like set
(i ") * x is Relation-like Function-like set
dom x is set
(i ") * (i * C) is Relation-like Function-like set
((i ") * i) * C is Relation-like Function-like set
(id (dom C)) * C is Relation-like dom C -defined Function-like set
rng cf is set
ccf is set
uf is Relation-like Function-like set
dom uf is set
i * uf is Relation-like Function-like set
dom (i * uf) is set
ucf is set
i . ucf is set
(i ") . (i . ucf) is set
(i * uf) . ucf is set
uf . (i . ucf) is set
((i ") * (i * C)) . (i . ucf) is set
(i * C) . ucf is set
cf . (i * uf) is set
(id (dom C)) * uf is Relation-like dom C -defined Function-like set
ucf is Relation-like Function-like set
(i ") * ucf is Relation-like Function-like set
dom (i ") is set
ccf is set
uf is set
cf . uf is set
ucf is Relation-like Function-like set
dom ucf is set
(i ") * ucf is Relation-like Function-like set
dom ((i ") * ucf) is set
x is set
(i ") . x is set
C . x is set
(i * C) . ((i ") . x) is set
((i ") * ucf) . x is set
ucf . ((i ") . x) is set
x is Relation-like Function-like set
(i ") * x is Relation-like Function-like set
f is set
[:f,f:] is Relation-like set
bool [:f,f:] is set
i is Relation-like Function-like set
dom i is set
product i is set
C is Relation-like f -defined f -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:f,f:]
C * i is Relation-like f -defined Function-like set
product (C * i) is set
rng C is set
dom C is set
dom (C * i) is set
C " is Relation-like f -defined f -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:f,f:]
rng (C ") is set
dom (C ") is set
f is set
(C ") . f is set
(C * i) . ((C ") . f) is set
C . ((C ") . f) is set
i . (C . ((C ") . f)) is set
i . f is set
f is Relation-like Function-like set
dom f is set
i is set
C is Relation-like Function-like set
dom C 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
C . cf is set
f . cf is set
Funcs ((f . cf),i) is functional set
f . cf is set
f is Relation-like Function-like set
rng f is set
(f,{}) is Relation-like Function-like set
dom f is set
(dom f) --> {} is Relation-like dom f -defined {{}} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:(dom f),{{}}:]
[:(dom f),{{}}:] is Relation-like set
bool [:(dom f),{{}}:] is set
i is set
f . i is set
((dom f) --> {}) . i is Relation-like Function-like set
Funcs ((f . i),{}) is functional set
dom ((dom f) --> {}) is set
f is set
({},f) is Relation-like Function-like set
dom ({},f) is 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
C is set
((f --> i),C) is Relation-like Function-like set
Funcs (i,C) is functional set
f --> (Funcs (i,C)) is Relation-like f -defined {(Funcs (i,C))} -valued Function-like constant total quasi_total Element of bool [:f,{(Funcs (i,C))}:]
{(Funcs (i,C))} is non empty V36() set
[:f,{(Funcs (i,C))}:] is Relation-like set
bool [:f,{(Funcs (i,C))}:] is set
dom (f --> i) is set
f is set
((f --> i),C) . f is set
(f --> i) . f is set
Funcs (((f --> i) . f),C) is functional set
dom ((f --> i),C) is set
f is set
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
C is set
[f,C] is V25() set
{f,C} is non empty V36() set
{{f,C},{f}} is non empty V36() V40() set
f is Relation-like Function-like set
dom f is set
curry f is Relation-like Function-like set
(curry f) . f is set
cf is Relation-like Function-like set
dom cf is set
dom (dom f) is set
rng (dom f) is set
[:{f},(rng (dom f)):] is Relation-like set
(dom f) /\ [:{f},(rng (dom f)):] is Relation-like set
rng ((dom f) /\ [:{f},(rng (dom f)):]) is set
ccf is Relation-like Function-like set
dom ccf is set
ccf is set
[ccf,C] is V25() set
{ccf,C} is non empty V36() set
{ccf} is non empty V36() set
{{ccf,C},{ccf}} is non empty V36() V40() set
f is set
i is Relation-like Function-like set
disjoin i is Relation-like Function-like set
Union (disjoin i) is set
Funcs ((Union (disjoin i)),f) is functional set
(i,f) is Relation-like Function-like set
product (i,f) is set
dom i is set
C is set
f is Relation-like Function-like set
dom f is set
rng f is set
curry' f is Relation-like Function-like set
cf is Relation-like Function-like set
dom cf is set
C is Relation-like Function-like set
dom C is set
rng C is set
f is set
C . f is set
cf is set
C . cf is set
ccf is Relation-like Function-like set
uf is Relation-like Function-like set
dom uf is set
curry' ccf is Relation-like Function-like set
ucf is Relation-like Function-like set
x is Relation-like Function-like set
dom x is set
curry' ucf is Relation-like Function-like set
g is set
g `1 is set
g `2 is set
[(g `1),(g `2)] is V25() set
{(g `1),(g `2)} is non empty V36() set
{(g `1)} is non empty V36() set
{{(g `1),(g `2)},{(g `1)}} is non empty V36() V40() set
i . (g `2) is set
x . (g `2) is set
(curry' ucf) . (g `2) is set
uf . (g `2) is set
h is Relation-like Function-like set
dom h is set
rng h is set
ucf . ((g `1),(g `2)) is set
ucf . [(g `1),(g `2)] is set
y is Relation-like Function-like set
y . (g `1) is set
h is Relation-like Function-like set
dom h is set
rng h is set
(curry' ccf) . (g `2) is set
ccf . ((g `1),(g `2)) is set
ccf . [(g `1),(g `2)] is set
h is Relation-like Function-like set
h . (g `1) is set
h is Relation-like Function-like set
dom h is set
rng h is set
ccf . g is set
ucf . g is set
g is Relation-like Function-like set
dom g is set
rng g is set
h is Relation-like Function-like set
dom h is set
rng h is set
f is set
cf is set
C . cf is set
ccf is Relation-like Function-like set
uf is Relation-like Function-like set
dom uf is set
curry' ccf is Relation-like Function-like set
ucf is set
dom (i,f) is set
(i,f) . ucf is set
i . ucf is set
Funcs ((i . ucf),f) is functional set
the Element of i . ucf is Element of i . ucf
[ the Element of i . ucf,ucf] is V25() set
{ the Element of i . ucf,ucf} is non empty V36() set
{ the Element of i . ucf} is non empty V36() set
{{ the Element of i . ucf,ucf},{ the Element of i . ucf}} is non empty V36() V40() set
[ the Element of i . ucf,ucf] `1 is set
[ the Element of i . ucf,ucf] `2 is set
(curry' ccf) . ucf is set
h is Relation-like Function-like set
dom h is set
rng h is set
dom (curry' ccf) is set
h is Relation-like Function-like set
dom h is set
rng h is set
g is Relation-like Function-like set
rng g is set
rng ccf is set
h is Relation-like Function-like set
dom h is set
rng h is set
dom g is set
dom ccf is set
dom (dom ccf) is set
{ucf} is non empty V36() set
[:(dom (dom ccf)),{ucf}:] is Relation-like set
(dom ccf) /\ [:(dom (dom ccf)),{ucf}:] is Relation-like set
dom ((dom ccf) /\ [:(dom (dom ccf)),{ucf}:]) is set
h is set
y is set
[h,y] is V25() set
{h,y} is non empty V36() set
{h} is non empty V36() set
{{h,y},{h}} is non empty V36() V40() set
[h,y] `1 is set
[h,y] `2 is set
i . y is set
h is Relation-like Function-like set
dom h is set
rng h is set
h is set
[h,ucf] is V25() set
{h,ucf} is non empty V36() set
{h} is non empty V36() set
{{h,ucf},{h}} is non empty V36() V40() set
[h,ucf] `1 is set
[h,ucf] `2 is set
y is Relation-like Function-like set
dom y is set
rng y is set
uf . ucf is set
f is set
dom (i,f) is set
cf is Relation-like Function-like set
dom cf is set
uncurry' cf is Relation-like Function-like set
uncurry cf is Relation-like Function-like set
~ (uncurry cf) is Relation-like Function-like set
dom (uncurry' cf) is set
ccf is set
uf is set
ucf is set
[uf,ucf] is V25() set
{uf,ucf} is non empty V36() set
{uf} is non empty V36() set
{{uf,ucf},{uf}} is non empty V36() V40() set
ccf `1 is set
ccf `2 is set
[ucf,uf] is V25() set
{ucf,uf} is non empty V36() set
{ucf} is non empty V36() set
{{ucf,uf},{ucf}} is non empty V36() V40() set
dom (uncurry cf) is set
x is set
h is set
[x,h] is V25() set
{x,h} is non empty V36() set
{x} is non empty V36() set
{{x,h},{x}} is non empty V36() V40() set
g is Relation-like Function-like set
cf . x is set
dom g is set
[x,h] `1 is set
[ucf,uf] `1 is set
(i,f) . x is set
i . x is set
Funcs ((i . x),f) is functional set
i . ucf is set
[x,h] `2 is set
[ucf,uf] `2 is set
y is Relation-like Function-like set
dom y is set
rng y is set
ccf is set
ccf `1 is set
ccf `2 is set
i . (ccf `2) is set
[(ccf `1),(ccf `2)] is V25() set
{(ccf `1),(ccf `2)} is non empty V36() set
{(ccf `1)} is non empty V36() set
{{(ccf `1),(ccf `2)},{(ccf `1)}} is non empty V36() V40() set
cf . (ccf `2) is set
(i,f) . (ccf `2) is set
Funcs ((i . (ccf `2)),f) is functional set
uf is Relation-like Function-like set
dom uf is set
rng uf is set
rng (uncurry' cf) is set
ccf is set
uf is set
(uncurry' cf) . uf is set
ucf is set
x is set
[ucf,x] is V25() set
{ucf,x} is non empty V36() set
{ucf} is non empty V36() set
{{ucf,x},{ucf}} is non empty V36() V40() set
[x,ucf] is V25() set
{x,ucf} is non empty V36() set
{x} is non empty V36() set
{{x,ucf},{x}} is non empty V36() V40() set
dom (uncurry cf) is set
g is set
y is set
[g,y] is V25() set
{g,y} is non empty V36() set
{g} is non empty V36() set
{{g,y},{g}} is non empty V36() V40() set
h is Relation-like Function-like set
cf . g is set
dom h is set
[g,y] `1 is set
[x,ucf] `1 is set
(i,f) . g is set
i . g is set
Funcs ((i . g),f) is functional set
i . x is set
[g,y] `2 is set
[x,ucf] `2 is set
(uncurry' cf) . (y,g) is set
[y,g] is V25() set
{y,g} is non empty V36() set
{y} is non empty V36() set
{{y,g},{y}} is non empty V36() V40() set
(uncurry' cf) . [y,g] is set
h . y is set
rng h is set
h is Relation-like Function-like set
dom h is set
rng h is set
C . (uncurry' cf) is set
ccf is Relation-like Function-like set
uf is Relation-like Function-like set
dom uf is set
curry' ccf is Relation-like Function-like set
ucf is set
cf . ucf is set
(i,f) . ucf is set
i . ucf is set
Funcs ((i . ucf),f) is functional set
x is Relation-like Function-like set
dom x is set
rng x is set
the Element of i . ucf is Element of i . ucf
[ the Element of i . ucf,ucf] is V25() set
{ the Element of i . ucf,ucf} is non empty V36() set
{ the Element of i . ucf} is non empty V36() set
{{ the Element of i . ucf,ucf},{ the Element of i . ucf}} is non empty V36() V40() set
curry' (uncurry' cf) is Relation-like Function-like set
(curry' (uncurry' cf)) . ucf is set
h is Relation-like Function-like set
~ (uncurry' cf) is Relation-like Function-like set
curry (~ (uncurry' cf)) is Relation-like Function-like set
(curry (~ (uncurry' cf))) . ucf is set
[ucf, the Element of i . ucf] is V25() set
{ucf, the Element of i . ucf} is non empty V36() set
{ucf} is non empty V36() set
{{ucf, the Element of i . ucf},{ucf}} is non empty V36() V40() set
dom (uncurry cf) is set
dom h is set
y is set
[ucf,y] is V25() set
{ucf,y} is non empty V36() set
{{ucf,y},{ucf}} is non empty V36() V40() set
h is set
a2 is set
[h,a2] is V25() set
{h,a2} is non empty V36() set
{h} is non empty V36() set
{{h,a2},{h}} is non empty V36() V40() set
g1 is Relation-like Function-like set
cf . h is set
dom g1 is set
y is set
[ucf,y] is V25() set
{ucf,y} is non empty V36() set
{{ucf,y},{ucf}} is non empty V36() V40() set
y is set
[ucf,y] is V25() set
{ucf,y} is non empty V36() set
{{ucf,y},{ucf}} is non empty V36() V40() set
h is set
a2 is set
[h,a2] is V25() set
{h,a2} is non empty V36() set
{h} is non empty V36() set
{{h,a2},{h}} is non empty V36() V40() set
g1 is Relation-like Function-like set
cf . h is set
dom g1 is set
h . y is set
(uncurry cf) . (ucf,y) is set
(uncurry cf) . [ucf,y] is set
x . y is set
uf . ucf is set
i is Relation-like Function-like set
dom i is set
f is set
C is Relation-like Function-like set
dom C 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
C . cf is set
i . cf is set
Funcs (f,(i . cf)) is functional set
f . cf is set
f is set
i is Relation-like Function-like set
(f,i) is Relation-like Function-like set
product (f,i) is set
product i is set
Funcs (f,(product i)) is functional set
C is set
dom (f,i) 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
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
cf is set
C is Relation-like Function-like set
dom C is set
rng C is 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
((rng f)) is set
rng (f) is set
f " (rng f) is set
dom (f,i) is set
dom i is set
cf is set
ccf is set
f . ccf is set
(f,i) . ccf is set
i . ccf is set
Funcs (f,(i . ccf)) is functional set
cf is set
f . cf is set
(f,i) . cf is set
i . cf is set
Funcs (f,(i . cf)) is functional set
(dom i) --> f is Relation-like dom i -defined {f} -valued Function-like constant total quasi_total Element of bool [:(dom i),{f}:]
{f} is non empty V36() set
[:(dom i),{f}:] is Relation-like set
bool [:(dom i),{f}:] is set
((dom i) --> f) . cf is set
dom (f . cf) is set
ccf is Relation-like Function-like set
dom ccf is set
rng ccf is set
dom ((dom i) --> f) is set
cf is set
ccf is set
(f) . ccf is set
uf is Relation-like Function-like set
dom uf is set
ucf is set
uncurry f is Relation-like Function-like set
(uncurry f) . (ucf,ccf) is set
[ucf,ccf] is V25() set
{ucf,ccf} is non empty V36() set
{ucf} is non empty V36() set
{{ucf,ccf},{ucf}} is non empty V36() V40() set
(uncurry f) . [ucf,ccf] is set
uf . ucf is set
f . ucf is set
(f,i) . ucf is set
i . ucf is set
Funcs (f,(i . ucf)) is functional set
x is Relation-like Function-like set
dom x is set
rng x is set
x . ccf is set
f is set
C . f is set
cf is set
C . cf is set
ccf is Relation-like Function-like set
(ccf) is Relation-like Function-like set
uncurry' ccf is Relation-like Function-like set
(ccf) is Relation-like Function-like set
((ccf)) is set
rng (ccf) is set
meet (rng (ccf)) is set
dom ccf is set
[:((ccf)),(dom ccf):] is Relation-like set
(uncurry' ccf) | [:((ccf)),(dom ccf):] is Relation-like Function-like set
curry ((uncurry' ccf) | [:((ccf)),(dom ccf):]) is Relation-like Function-like set
uf is Relation-like Function-like set
(uf) is Relation-like Function-like set
uncurry' uf is Relation-like Function-like set
(uf) is Relation-like Function-like set
((uf)) is set
rng (uf) is set
meet (rng (uf)) is set
dom uf is set
[:((uf)),(dom uf):] is Relation-like set
(uncurry' uf) | [:((uf)),(dom uf):] is Relation-like Function-like set
curry ((uncurry' uf) | [:((uf)),(dom uf):]) is Relation-like Function-like set
dom (f,i) is set
dom i is set
ucf is set
(f,i) . ucf is set
i . ucf is set
Funcs (f,(i . ucf)) is functional set
ccf . ucf is set
x is Relation-like Function-like set
dom x is set
rng x is set
uf . ucf is set
g is Relation-like Function-like set
dom g is set
rng g is set
dom (uf) is set
rng uf is set
((rng uf)) is set
uf " (rng uf) is set
h is set
(uf) . h is set
uncurry uf is Relation-like Function-like set
(uncurry uf) . (ucf,h) is set
[ucf,h] is V25() set
{ucf,h} is non empty V36() set
{ucf} is non empty V36() set
{{ucf,h},{ucf}} is non empty V36() V40() set
(uncurry uf) . [ucf,h] is set
g . h is set
uncurry ccf is Relation-like Function-like set
(uncurry ccf) . (ucf,h) is set
(uncurry ccf) . [ucf,h] is set
x . h is set
y is Relation-like Function-like set
dom y is set
y . ucf is set
f is set
cf is set
C . cf is set
ccf is Relation-like Function-like set
(ccf) is Relation-like Function-like set
uncurry' ccf is Relation-like Function-like set
(ccf) is Relation-like Function-like set
((ccf)) is set
rng (ccf) is set
meet (rng (ccf)) is set
dom ccf is set
[:((ccf)),(dom ccf):] is Relation-like set
(uncurry' ccf) | [:((ccf)),(dom ccf):] is Relation-like Function-like set
curry ((uncurry' ccf) | [:((ccf)),(dom ccf):]) is Relation-like Function-like set
dom (ccf) is set
rng (ccf) is set
f is set
cf is Relation-like Function-like set
dom cf is set
rng cf is set
(cf) is Relation-like Function-like set
uncurry' cf is Relation-like Function-like set
(cf) is Relation-like Function-like set
((cf)) is set
rng (cf) is set
meet (rng (cf)) is set
[:((cf)),(dom cf):] is Relation-like set
(uncurry' cf) | [:((cf)),(dom cf):] is Relation-like Function-like set
curry ((uncurry' cf) | [:((cf)),(dom cf):]) is Relation-like Function-like set
cf " (rng cf) is set
uf is set
cf . uf 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)) . uf is set
(cf) . uf is set
ucf is Relation-like Function-like set
dom ucf is set
dom (cf) is set
uf is set
ucf is Relation-like Function-like set
dom ucf is set
((rng cf)) is set
dom (cf) is set
cf " ((rng cf)) is set
(dom cf) --> (dom i) is Relation-like dom cf -defined {(dom i)} -valued Function-like constant total quasi_total Element of bool [:(dom cf),{(dom i)}:]
[:(dom cf),{(dom i)}:] is Relation-like set
bool [:(dom cf),{(dom i)}:] is set
dom ((dom cf) --> (dom i)) is set
uf is set
(cf) . uf is set
ucf is Relation-like Function-like set
dom ucf is set
rng ucf is set
i . uf is set
x is set
g is set
ucf . g is set
cf . g is set
h is Relation-like Function-like set
dom h is set
uncurry cf is Relation-like Function-like set
(uncurry cf) . (g,uf) is set
[g,uf] is V25() set
{g,uf} is non empty V36() set
{g} is non empty V36() set
{{g,uf},{g}} is non empty V36() V40() set
(uncurry cf) . [g,uf] is set
h . uf is set
Funcs (f,(i . uf)) is functional set
(f,i) . uf is set
((cf)) is Relation-like Function-like set
(((cf))) is set
rng ((cf)) is set
meet (rng ((cf))) is set
((cf)) is Relation-like Function-like set
uncurry' (cf) is Relation-like Function-like set
[:(((cf))),(dom (cf)):] is Relation-like set
(uncurry' (cf)) | [:(((cf))),(dom (cf)):] is Relation-like Function-like set
curry ((uncurry' (cf)) | [:(((cf))),(dom (cf)):]) is Relation-like Function-like set
dom ((cf)) is set
Union i is set
Funcs ((dom i),(Union i)) is functional set
uncurry cf is Relation-like Function-like set
dom (uncurry cf) is set
[:(dom cf),(dom i):] is Relation-like set
dom (f,i) is set
C . (cf) is set
dom (uncurry' cf) is set
[:(dom i),(dom cf):] is Relation-like set
~ (uncurry cf) is Relation-like Function-like set
curry (~ (uncurry cf)) is Relation-like Function-like set
curry' (uncurry cf) is Relation-like Function-like set
(uncurry cf) | [:(((cf))),(dom (cf)):] is Relation-like Function-like set
uncurry' (curry' (uncurry cf)) is Relation-like Function-like set
uf is Relation-like Function-like set
(uf) is Relation-like Function-like set
uncurry' uf is Relation-like Function-like set
(uf) is Relation-like Function-like set
((uf)) is set
rng (uf) is set
meet (rng (uf)) is set
dom uf is set
[:((uf)),(dom uf):] is Relation-like set
(uncurry' uf) | [:((uf)),(dom uf):] is Relation-like Function-like set
curry ((uncurry' uf) | [:((uf)),(dom uf):]) is Relation-like Function-like set
f is Relation-like Function-like set
({},f) is Relation-like Function-like set
dom f is set
(dom f) --> {{}} is Relation-like non-empty dom f -defined {{{}}} -valued Function-like constant total quasi_total Element of bool [:(dom f),{{{}}}:]
{{{}}} is non empty V36() V40() set
[:(dom f),{{{}}}:] is Relation-like set
bool [:(dom f),{{{}}}:] is set
i is set
({},f) . i is set
f . i is set
Funcs ({},(f . i)) is functional set
dom ({},f) is set
f is set
(f,{}) is Relation-like Function-like set
dom (f,{}) is set
f is set
i is 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 Function-like set
Funcs (f,C) is functional set
i --> (Funcs (f,C)) is Relation-like i -defined {(Funcs (f,C))} -valued Function-like constant total quasi_total Element of bool [:i,{(Funcs (f,C))}:]
{(Funcs (f,C))} is non empty V36() set
[:i,{(Funcs (f,C))}:] is Relation-like set
bool [:i,{(Funcs (f,C))}:] is set
dom (i --> C) is set
f is set
(f,(i --> C)) . f is set
(i --> C) . f is set
Funcs (f,((i --> C) . f)) is functional set
dom (f,(i --> C)) is set
f is set
i is Relation-like Function-like set
(f,i) is Relation-like Function-like set
product (f,i) is set
product i is set
Funcs (f,(product i)) is functional set
Funcs (f,(product {})) is functional set
f --> {} is Relation-like f -defined {{}} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:f,{{}}:]
[:f,{{}}:] is Relation-like set
bool [:f,{{}}:] is set
{(f --> {})} is non empty functional V36() set
({},i) is Relation-like Function-like set
product ({},i) is set
dom i is set
(dom i) --> {{}} is Relation-like non-empty dom i -defined {{{}}} -valued Function-like constant total quasi_total Element of bool [:(dom i),{{{}}}:]
{{{}}} is non empty V36() V40() set
[:(dom i),{{{}}}:] is Relation-like set
bool [:(dom i),{{{}}}:] is set
product ((dom i) --> {{}}) is set
Funcs ((dom i),{{}}) is non empty functional FUNCTION_DOMAIN of dom i,{{}}
(dom i) --> {} is Relation-like dom i -defined {{}} -valued Function-like constant total quasi_total Function-yielding V35() Element of bool [:(dom i),{{}}:]
[:(dom i),{{}}:] is Relation-like set
bool [:(dom i),{{}}:] is set
{((dom i) --> {})} is non empty functional V36() set
Funcs ({},(product i)) is functional set
(f,{}) is Relation-like Function-like set
product (f,{}) is set
f is Relation-like Function-like set
uncurry f is Relation-like Function-like set
curry' (uncurry f) is Relation-like Function-like set
dom (curry' (uncurry f)) is set
C is set
(curry' (uncurry f)) . C is set
i is set
f is Relation-like Function-like set
(f) is Relation-like Function-like Function-yielding V35() set
uncurry f is Relation-like Function-like set
curry' (uncurry f) is Relation-like Function-like set
dom (f) is set
(f) . i is Relation-like Function-like set
f is set
i is 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
f is Relation-like Function-like set
(f) is Relation-like Function-like Function-yielding V35() set
uncurry f is Relation-like Function-like set
curry' (uncurry f) is Relation-like Function-like set
[:f,i:] is Relation-like set
Funcs ([:f,i:],C) is functional set
f is set
i is set
C is set
Funcs (i,C) is functional set
Funcs (f,(Funcs (i,C))) is functional set
f is Relation-like Function-like set
(f) is Relation-like Function-like Function-yielding V35() set
uncurry f is Relation-like Function-like set
curry' (uncurry f) is Relation-like Function-like set
uf is Relation-like Function-like set
ucf is Relation-like Function-like set
dom ucf is set
dom uf is set
rng ucf is set
rng uf is set
x is set
g is set
f . x is set
(f) . g is Relation-like Function-like set
ucf . x is set
uf . g is set
Funcs (f,C) is functional set
Funcs (i,(Funcs (f,C))) is functional set
rng (f) is set
h is Relation-like Function-like set
dom h is set
rng h is set
h is Relation-like Function-like set
dom h is set
rng h is set
rng f is set
h is Relation-like Function-like set
dom h is set
rng h is set
h is Relation-like Function-like set
dom h is set
rng h is set
[x,g] is V25() set
{x,g} is non empty V36() set
{x} is non empty V36() set
{{x,g},{x}} is non empty V36() V40() set
dom (uncurry f) is set
(uncurry f) . (x,g) is set
(uncurry f) . [x,g] 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
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
C is set
Funcs (i,C) is functional set
Funcs (f,(Funcs (i,C))) is functional set
f is Relation-like Function-like set
(f) is Relation-like Function-like Function-yielding V35() set
uncurry f is Relation-like Function-like set
curry' (uncurry f) is Relation-like Function-like set
((f)) is Relation-like Function-like Function-yielding V35() set
uncurry (f) is Relation-like Function-like set
curry' (uncurry (f)) is Relation-like Function-like set
Funcs (f,C) is functional set
Funcs (i,(Funcs (f,C))) is functional set
x is set
f . x is set
((f)) . x is Relation-like Function-like set
rng f is set
g is Relation-like Function-like set
dom g is set
rng g is set
g is Relation-like Function-like set
dom g is set
rng g is set
g is Relation-like Function-like set
dom g is set
rng g is set
rng ((f)) is set
h is Relation-like Function-like set
dom h is set
rng h is set
h is Relation-like Function-like set
dom h is set
rng h is set
h is Relation-like Function-like set
dom h is set
rng h is set
y is set
(f) . y is Relation-like Function-like set
g . y is set
[x,y] is V25() set
{x,y} is non empty V36() set
{x} is non empty V36() set
{{x,y},{x}} is non empty V36() V40() set
dom (uncurry f) is set
(uncurry f) . (x,y) is set
(uncurry f) . [x,y] is set
h is Relation-like Function-like set
dom h is set
rng h is set
h is Relation-like Function-like set
dom h is set
h . x is set
dom (uncurry (f)) is set
y is set
[y,x] is V25() set
{y,x} is non empty V36() set
{y} is non empty V36() set
{{y,x},{y}} is non empty V36() V40() set
(uncurry (f)) . (y,x) is set
(uncurry (f)) . [y,x] is set
g . y is set
(f) . y is Relation-like Function-like set
h is Relation-like Function-like set
dom h is set
h . x is set
g1 is Relation-like Function-like set
dom g1 is set
rng g1 is set
y is set
h . y is set
g . y is set
[y,x] is V25() set
{y,x} is non empty V36() set
{y} is non empty V36() set
{{y,x},{y}} is non empty V36() V40() set
(uncurry (f)) . (y,x) is set
(uncurry (f)) . [y,x] is set
ccf is Relation-like Function-like set
dom ccf is set
rng ccf is set
uf is Relation-like Function-like set
dom uf is set
rng uf is set
({}) is Relation-like Function-like Function-yielding V35() set
curry' (uncurry {}) is Relation-like Function-like set
f is Relation-like Function-like Function-yielding V35() set
(f) is Relation-like Function-like set
dom (f) is set
dom f is set
i is set
rng f is set
((rng f)) is set
f " ((rng f)) is set
i is set
f . i is Relation-like Function-like set
rng f is set
((rng f)) is set
f " ((rng f)) is set
f is Relation-like Function-like Function-yielding V35() set
(f) is Relation-like Function-like set
dom (f) is set
dom f is set
i is set
rng f is set
((rng f)) is set
f " ((rng f)) is set
i is set
f . i is Relation-like Function-like set
rng f is set
((rng f)) is set
f " ((rng f)) is set