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