:: PRALG_2 semantic presentation

K153() is V33() countable denumerable Element of bool K149()
K149() is set
bool K149() is set
K120() is V33() countable denumerable set
bool K120() is set
bool K153() is set
K198() is set
{} is Relation-like non-empty empty-yielding K153() -defined Function-like one-to-one constant functional empty Function-yielding V25() V33() Cardinal-yielding countable V61() V62() V63() set
the Relation-like non-empty empty-yielding K153() -defined Function-like one-to-one constant functional empty Function-yielding V25() V33() Cardinal-yielding countable V61() V62() V63() set is Relation-like non-empty empty-yielding K153() -defined Function-like one-to-one constant functional empty Function-yielding V25() V33() Cardinal-yielding countable V61() V62() V63() set
{{}} is functional non empty with_common_domain set
{{}} * is functional non empty V63() M8({{}})
[:({{}} *),{{}}:] is Relation-like set
bool [:({{}} *),{{}}:] is set
PFuncs (({{}} *),{{}}) is set
1 is non empty 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
2 is non empty set
3 is non empty set
product {} is functional non empty with_common_domain product-like set
commute {} is Relation-like Function-like Function-yielding V25() set
uncurry {} is Relation-like Function-like set
curry' (uncurry {}) is Relation-like Function-like set
uncurry' {} is Relation-like Function-like set
dom {} is Relation-like non-empty empty-yielding K153() -defined Function-like one-to-one constant functional empty Function-yielding V25() V33() Cardinal-yielding countable V61() V62() V63() set
rng {} is Relation-like non-empty empty-yielding K153() -defined Function-like one-to-one constant functional empty trivial Function-yielding V25() V33() Cardinal-yielding countable V61() V62() V63() V85() set
I is functional non empty with_common_domain set
DOM I is set
S is Relation-like Function-like Element of I
dom S is set
I is functional non empty with_common_domain set
DOM I is set
S is Relation-like DOM I -defined Function-like Element of I
dom S is set
I is Relation-like Function-like set
dom I is set
S is set
g is Relation-like Function-like set
A is set
commute g is Relation-like Function-like Function-yielding V25() set
uncurry g is Relation-like Function-like set
curry' (uncurry g) is Relation-like Function-like set
o is Relation-like Function-like set
f is set
commute o is Relation-like Function-like Function-yielding V25() set
uncurry o is Relation-like Function-like set
curry' (uncurry o) is Relation-like Function-like set
S is set
A is set
g is set
o is Relation-like Function-like set
commute o is Relation-like Function-like Function-yielding V25() set
uncurry o is Relation-like Function-like set
curry' (uncurry o) is Relation-like Function-like set
f is Relation-like Function-like set
commute f is Relation-like Function-like Function-yielding V25() set
uncurry f is Relation-like Function-like set
curry' (uncurry f) is Relation-like Function-like set
I . (commute f) is set
g is set
o is Relation-like Function-like set
commute o is Relation-like Function-like Function-yielding V25() set
uncurry o is Relation-like Function-like set
curry' (uncurry o) is Relation-like Function-like set
I . (commute o) is set
A is Relation-like Function-like set
dom A is set
f is set
g is set
s is Relation-like Function-like set
commute s is Relation-like Function-like Function-yielding V25() set
uncurry s is Relation-like Function-like set
curry' (uncurry s) is Relation-like Function-like set
o is Relation-like Function-like set
s is Relation-like Function-like set
commute s is Relation-like Function-like Function-yielding V25() set
uncurry s is Relation-like Function-like set
curry' (uncurry s) is Relation-like Function-like set
f is Relation-like Function-like set
commute f is Relation-like Function-like Function-yielding V25() set
uncurry f is Relation-like Function-like set
curry' (uncurry f) is Relation-like Function-like set
g is Relation-like Function-like set
commute g is Relation-like Function-like Function-yielding V25() set
uncurry g is Relation-like Function-like set
curry' (uncurry g) is Relation-like Function-like set
f is Relation-like Function-like set
A . f is set
commute f is Relation-like Function-like Function-yielding V25() set
uncurry f is Relation-like Function-like set
curry' (uncurry f) is Relation-like Function-like set
I . (commute f) is set
S is Relation-like Function-like set
dom S is set
A is Relation-like Function-like set
dom A is set
f is set
g is Relation-like Function-like set
commute g is Relation-like Function-like Function-yielding V25() set
uncurry g is Relation-like Function-like set
curry' (uncurry g) is Relation-like Function-like set
g is Relation-like Function-like set
commute g is Relation-like Function-like Function-yielding V25() set
uncurry g is Relation-like Function-like set
curry' (uncurry g) is Relation-like Function-like set
f is set
g is Relation-like Function-like set
commute g is Relation-like Function-like Function-yielding V25() set
uncurry g is Relation-like Function-like set
curry' (uncurry g) is Relation-like Function-like set
S . f is set
commute (commute g) is Relation-like Function-like Function-yielding V25() set
uncurry (commute g) is Relation-like Function-like set
curry' (uncurry (commute g)) is Relation-like Function-like set
I . (commute (commute g)) is set
A . 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
S is set
A is Relation-like Function-like set
commute A is Relation-like Function-like Function-yielding V25() set
uncurry A is Relation-like Function-like set
curry' (uncurry A) is Relation-like Function-like set
S is set
S is set
(I) . S is set
I . S is set
I is Relation-like Function-like Function-yielding V25() set
Frege I is Relation-like Function-like set
doms I is Relation-like Function-like set
product (doms I) is functional with_common_domain product-like set
dom (Frege I) is set
S is set
(Frege I) . S is set
A is Relation-like Function-like set
(Frege I) . A is set
rng I is set
SubFuncs (rng I) is set
I " (SubFuncs (rng I)) is set
uncurry I is Relation-like Function-like set
f is Relation-like Function-like set
dom f is set
S is Relation-like product (doms I) -defined Function-like total Function-yielding V25() set
rng I is set
A is set
dom I is set
f is set
I . f is Relation-like Function-like set
SubFuncs (rng I) is set
A is Relation-like Function-like set
S . A is Relation-like Function-like set
I .. A is Relation-like Function-like set
I " (SubFuncs (rng I)) is set
uncurry I is Relation-like Function-like set
f is Relation-like Function-like set
dom f is set
dom I is set
g is set
f . g is set
I . g is Relation-like Function-like set
A . g is set
(I . g) . (A . g) is set
dom (doms I) is set
(doms I) . g is set
dom (I . g) is set
I .. (g,(A . g)) is set
(uncurry I) . (g,(A . g)) is set
[g,(A . g)] is V15() set
{g,(A . g)} is non empty set
{g} is non empty set
{{g,(A . g)},{g}} is non empty set
(uncurry I) . [g,(A . g)] is set
I " (SubFuncs (rng I)) is set
uncurry I is Relation-like Function-like set
A is Relation-like Function-like set
S . A is Relation-like Function-like set
I .. A is Relation-like Function-like set
dom (S . A) is set
dom I is set
f is set
(S . A) . f is set
A . f is set
(uncurry I) . (f,(A . f)) is set
[f,(A . f)] is V15() set
{f,(A . f)} is non empty set
{f} is non empty set
{{f,(A . f)},{f}} is non empty set
(uncurry I) . [f,(A . f)] is set
dom (doms I) is set
(doms I) . f is set
I . f is Relation-like Function-like set
dom (I . f) is set
(I .. A) . f is set
(I . f) . (A . f) is set
dom S is set
I is set
S is Relation-like non-empty I -defined Function-like total set
A is Relation-like non-empty I -defined Function-like total set
[|S,A|] is Relation-like I -defined Function-like total set
f is set
[|S,A|] . f is set
S . f is set
A . f is set
[:(S . f),(A . f):] is Relation-like set
I is non empty set
S is set
[:S,I:] is Relation-like set
bool [:S,I:] is set
A is Relation-like I -defined Function-like non empty total set
f is Relation-like I -defined Function-like non empty total set
[|A,f|] is Relation-like I -defined Function-like non empty total set
g is Relation-like S -defined I -valued Function-like quasi_total Element of bool [:S,I:]
g * [|A,f|] is Relation-like S -defined Function-like total set
g * A is Relation-like S -defined Function-like total set
g * f is Relation-like S -defined Function-like total set
[|(g * A),(g * f)|] is Relation-like S -defined Function-like total set
dom (g * f) is set
o is set
(g * [|A,f|]) . o is set
[|(g * A),(g * f)|] . o is set
dom (g * A) is set
g . o is set
dom (g * [|A,f|]) is set
[|A,f|] . (g . o) is set
A . (g . o) is set
f . (g . o) is set
[:(A . (g . o)),(f . (g . o)):] is Relation-like set
(g * A) . o is set
[:((g * A) . o),(f . (g . o)):] is Relation-like set
(g * f) . o is set
[:((g * A) . o),((g * f) . o):] is Relation-like set
I is non empty set
I * is functional non empty V63() M8(I)
S is Relation-like non-empty non empty-yielding I -defined Function-like non empty total set
S # is Relation-like non-empty non empty-yielding I * -defined Function-like non empty total set
f is Relation-like K153() -defined I -valued Function-like V33() countable V61() V62() Element of I *
(S #) . f is non empty set
g is Element of I
S . g is non empty set
[:((S #) . f),(S . g):] is Relation-like set
bool [:((S #) . f),(S . g):] is set
A is Relation-like non-empty non empty-yielding I -defined Function-like non empty total set
A # is Relation-like non-empty non empty-yielding I * -defined Function-like non empty total set
(A #) . f is non empty set
A . g is non empty set
[:((A #) . f),(A . g):] is Relation-like set
bool [:((A #) . f),(A . g):] is set
[|S,A|] is Relation-like non-empty non empty-yielding I -defined Function-like non empty total set
[|S,A|] # is Relation-like non-empty non empty-yielding I * -defined Function-like non empty total set
([|S,A|] #) . f is non empty set
[|S,A|] . g is non empty set
[:(([|S,A|] #) . f),([|S,A|] . g):] is Relation-like set
bool [:(([|S,A|] #) . f),([|S,A|] . g):] is set
o is Relation-like (S #) . f -defined S . g -valued Function-like quasi_total Element of bool [:((S #) . f),(S . g):]
s is Relation-like (A #) . f -defined A . g -valued Function-like quasi_total Element of bool [:((A #) . f),(A . g):]
f * [|S,A|] is Relation-like non-empty K153() -defined Function-like set
product (f * [|S,A|]) is functional non empty with_common_domain product-like set
f is set
rng f is set
dom (f * [|S,A|]) is set
c₁₁ is Relation-like Function-like set
dom c₁₁ is set
dom [|S,A|] is non empty set
dom f is set
pr1 c₁₁ is Relation-like Function-like set
dom (pr1 c₁₁) is set
dom S is non empty set
f * S is Relation-like non-empty K153() -defined Function-like set
dom (f * S) is set
f is set
(pr1 c₁₁) . f is set
(f * S) . f is set
(f * [|S,A|]) . f is set
f . f is set
[|S,A|] . (f . f) is set
c₁₁ . f is set
S . (f . f) is set
A . (f . f) is set
[:(S . (f . f)),(A . (f . f)):] is Relation-like set
f is set
o is set
[f,o] is V15() set
{f,o} is non empty set
{f} is non empty set
{{f,o},{f}} is non empty set
[f,o] `1 is set
(c<sub>11</sub> . f) `1 is set
product (f * S) is functional non empty with_common_domain product-like set
dom o is set
o . (pr1 c₁₁) is set
rng o is set
pr2 c₁₁ is Relation-like Function-like set
s . (pr2 c₁₁) is set
[(o . (pr1 c₁₁)),(s . (pr2 c₁₁))] is V15() set
{(o . (pr1 c₁₁)),(s . (pr2 c₁₁))} is non empty set
{(o . (pr1 c₁₁))} is non empty set
{{(o . (pr1 c₁₁)),(s . (pr2 c₁₁))},{(o . (pr1 c₁₁))}} is non empty set
f is V15() set
rng s is set
[:(rng o),(rng s):] is Relation-like set
[:(S . g),(A . g):] is Relation-like set
dom (pr2 c₁₁) is set
dom A is non empty set
f * A is Relation-like non-empty K153() -defined Function-like set
dom (f * A) is set
f is set
(pr2 c₁₁) . f is set
(f * A) . f is set
(f * [|S,A|]) . f is set
f . f is set
[|S,A|] . (f . f) is set
c₁₁ . f is set
S . (f . f) is set
A . (f . f) is set
[:(S . (f . f)),(A . (f . f)):] is Relation-like set
o is set
C is set
[o,C] is V15() set
{o,C} is non empty set
{o} is non empty set
{{o,C},{o}} is non empty set
[o,C] `2 is set
(c<sub>11</sub> . f) `2 is set
product (f * A) is functional non empty with_common_domain product-like set
dom s is set
f is Relation-like Function-like set
pr1 f is Relation-like Function-like set
o . (pr1 f) is set
pr2 f is Relation-like Function-like set
s . (pr2 f) is set
[(o . (pr1 f)),(s . (pr2 f))] is V15() set
{(o . (pr1 f)),(s . (pr2 f))} is non empty set
{(o . (pr1 f))} is non empty set
{{(o . (pr1 f)),(s . (pr2 f))},{(o . (pr1 f))}} is non empty set
f is Relation-like ([|S,A|] #) . f -defined [|S,A|] . g -valued Function-like quasi_total Element of bool [:(([|S,A|] #) . f),([|S,A|] . g):]
c₁₁ is Relation-like Function-like set
f . c₁₁ is set
pr1 c₁₁ is Relation-like Function-like set
o . (pr1 c₁₁) is set
pr2 c₁₁ is Relation-like Function-like set
s . (pr2 c₁₁) is set
[(o . (pr1 c₁₁)),(s . (pr2 c₁₁))] is V15() set
{(o . (pr1 c₁₁)),(s . (pr2 c₁₁))} is non empty set
{(o . (pr1 c₁₁))} is non empty set
{{(o . (pr1 c₁₁)),(s . (pr2 c₁₁))},{(o . (pr1 c₁₁))}} is non empty set
f is Relation-like ([|S,A|] #) . f -defined [|S,A|] . g -valued Function-like quasi_total Element of bool [:(([|S,A|] #) . f),([|S,A|] . g):]
f is Relation-like ([|S,A|] #) . f -defined [|S,A|] . g -valued Function-like quasi_total Element of bool [:(([|S,A|] #) . f),([|S,A|] . g):]
f is Element of ([|S,A|] #) . f
f . f is set
f . f is set
f * [|S,A|] is Relation-like non-empty K153() -defined Function-like set
product (f * [|S,A|]) is functional non empty with_common_domain product-like set
dom (f * [|S,A|]) is set
c₁₁ is Relation-like Function-like set
dom c₁₁ is set
f . c₁₁ is set
pr1 c₁₁ is Relation-like Function-like set
o . (pr1 c₁₁) is set
pr2 c₁₁ is Relation-like Function-like set
s . (pr2 c₁₁) is set
[(o . (pr1 c₁₁)),(s . (pr2 c₁₁))] is V15() set
{(o . (pr1 c₁₁)),(s . (pr2 c₁₁))} is non empty set
{(o . (pr1 c₁₁))} is non empty set
{{(o . (pr1 c₁₁)),(s . (pr2 c₁₁))},{(o . (pr1 c₁₁))}} is non empty set
f . f is Element of [|S,A|] . g
f . f is Element of [|S,A|] . g
I is non empty set
S is set
I * is functional non empty V63() M8(I)
[:S,(I *):] is Relation-like set
bool [:S,(I *):] is set
[:S,I:] is Relation-like set
bool [:S,I:] is set
g is Relation-like S -defined I * -valued Function-like quasi_total Function-yielding V25() Element of bool [:S,(I *):]
A is Relation-like non-empty non empty-yielding I -defined Function-like non empty total set
A # is Relation-like non-empty non empty-yielding I * -defined Function-like non empty total set
g * (A #) is Relation-like non-empty S -defined Function-like total set
o is Relation-like S -defined I -valued Function-like quasi_total Element of bool [:S,I:]
o * A is Relation-like non-empty S -defined Function-like total set
f is Relation-like non-empty non empty-yielding I -defined Function-like non empty total set
f # is Relation-like non-empty non empty-yielding I * -defined Function-like non empty total set
g * (f #) is Relation-like non-empty S -defined Function-like total set
o * f is Relation-like non-empty S -defined Function-like total set
[|A,f|] is Relation-like non-empty non empty-yielding I -defined Function-like non empty total set
[|A,f|] # is Relation-like non-empty non empty-yielding I * -defined Function-like non empty total set
g * ([|A,f|] #) is Relation-like non-empty S -defined Function-like total set
o * [|A,f|] is Relation-like non-empty S -defined Function-like total set
s is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of g * (A #),o * A
f is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of g * (f #),o * f
f is set
g . f is Relation-like K153() -defined Function-like V33() countable V61() V62() set
o . f is set
s . f is Relation-like Function-like set
f . f is Relation-like Function-like set
dom o is set
A . (o . f) is set
(o * A) . f is set
f . (o . f) is set
(o * f) . f is set
dom g is set
(A #) . (g . f) is set
(g * (A #)) . f is set
f is Relation-like K153() -defined I -valued Function-like V33() countable V61() V62() Element of I *
(A #) . f is non empty set
c₁₁ is Element of I
A . c₁₁ is non empty set
[:((A #) . f),(A . c₁₁):] is Relation-like set
bool [:((A #) . f),(A . c₁₁):] is set
(f #) . (g . f) is set
(g * (f #)) . f is set
(f #) . f is non empty set
f . c₁₁ is non empty set
[:((f #) . f),(f . c₁₁):] is Relation-like set
bool [:((f #) . f),(f . c₁₁):] is set
f is Relation-like (A #) . f -defined A . c₁₁ -valued Function-like quasi_total Element of bool [:((A #) . f),(A . c₁₁):]
f is Relation-like (f #) . f -defined f . c₁₁ -valued Function-like quasi_total Element of bool [:((f #) . f),(f . c₁₁):]
(I,A,f,f,c₁₁,f,f) is Relation-like ([|A,f|] #) . f -defined [|A,f|] . c₁₁ -valued Function-like quasi_total Element of bool [:(([|A,f|] #) . f),([|A,f|] . c₁₁):]
([|A,f|] #) . f is non empty set
[|A,f|] . c₁₁ is non empty set
[:(([|A,f|] #) . f),([|A,f|] . c₁₁):] is Relation-like set
bool [:(([|A,f|] #) . f),([|A,f|] . c₁₁):] is set
o is Relation-like K153() -defined I -valued Function-like V33() countable V61() V62() Element of I *
(A #) . o is non empty set
C is Element of I
A . C is non empty set
[:((A #) . o),(A . C):] is Relation-like set
bool [:((A #) . o),(A . C):] is set
(f #) . o is non empty set
f . C is non empty set
[:((f #) . o),(f . C):] is Relation-like set
bool [:((f #) . o),(f . C):] is set
F is Relation-like (A #) . o -defined A . C -valued Function-like quasi_total Element of bool [:((A #) . o),(A . C):]
Ar is Relation-like (f #) . o -defined f . C -valued Function-like quasi_total Element of bool [:((f #) . o),(f . C):]
(I,A,f,o,C,F,Ar) is Relation-like ([|A,f|] #) . o -defined [|A,f|] . C -valued Function-like quasi_total Element of bool [:(([|A,f|] #) . o),([|A,f|] . C):]
([|A,f|] #) . o is non empty set
[|A,f|] . C is non empty set
[:(([|A,f|] #) . o),([|A,f|] . C):] is Relation-like set
bool [:(([|A,f|] #) . o),([|A,f|] . C):] is set
f is Relation-like Function-like set
dom f is set
f is Relation-like S -defined Function-like total set
dom f is set
c₁₁ is set
f . c₁₁ is set
g . c₁₁ is Relation-like K153() -defined Function-like V33() countable V61() V62() set
o . c₁₁ is set
dom o is set
A . (o . c₁₁) is set
(o * A) . c₁₁ is set
f . (o . c₁₁) is set
(o * f) . c₁₁ is set
dom g is set
(A #) . (g . c₁₁) is set
(g * (A #)) . c₁₁ is set
f is Relation-like K153() -defined I -valued Function-like V33() countable V61() V62() Element of I *
(A #) . f is non empty set
f is Element of I
A . f is non empty set
[:((A #) . f),(A . f):] is Relation-like set
bool [:((A #) . f),(A . f):] is set
s . c₁₁ is Relation-like Function-like set
(f #) . (g . c₁₁) is set
(g * (f #)) . c₁₁ is set
(f #) . f is non empty set
f . f is non empty set
[:((f #) . f),(f . f):] is Relation-like set
bool [:((f #) . f),(f . f):] is set
f . c₁₁ is Relation-like Function-like set
o is Relation-like (A #) . f -defined A . f -valued Function-like quasi_total Element of bool [:((A #) . f),(A . f):]
C is Relation-like (f #) . f -defined f . f -valued Function-like quasi_total Element of bool [:((f #) . f),(f . f):]
(I,A,f,f,f,o,C) is Relation-like ([|A,f|] #) . f -defined [|A,f|] . f -valued Function-like quasi_total Element of bool [:(([|A,f|] #) . f),([|A,f|] . f):]
([|A,f|] #) . f is non empty set
[|A,f|] . f is non empty set
[:(([|A,f|] #) . f),([|A,f|] . f):] is Relation-like set
bool [:(([|A,f|] #) . f),([|A,f|] . f):] is set
c₁₁ is Relation-like S -defined Function-like total Function-yielding V25() set
f is set
c₁₁ . f is Relation-like Function-like set
(g * ([|A,f|] #)) . f is set
(o * [|A,f|]) . f is set
[:((g * ([|A,f|] #)) . f),((o * [|A,f|]) . f):] is Relation-like set
bool [:((g * ([|A,f|] #)) . f),((o * [|A,f|]) . f):] is set
g . f is Relation-like K153() -defined Function-like V33() countable V61() V62() set
o . f is set
dom g is set
([|A,f|] #) . (g . f) is set
dom o is set
A . (o . f) is set
(o * A) . f is set
[|A,f|] . (o . f) is set
f . (o . f) is set
(o * f) . f is set
(f #) . (g . f) is set
(g * (f #)) . f is set
f is Relation-like K153() -defined I -valued Function-like V33() countable V61() V62() Element of I *
(f #) . f is non empty set
o is Element of I
f . o is non empty set
[:((f #) . f),(f . o):] is Relation-like set
bool [:((f #) . f),(f . o):] is set
f . f is Relation-like Function-like set
(A #) . (g . f) is set
(g * (A #)) . f is set
(A #) . f is non empty set
A . o is non empty set
[:((A #) . f),(A . o):] is Relation-like set
bool [:((A #) . f),(A . o):] is set
s . f is Relation-like Function-like set
F is Relation-like (A #) . f -defined A . o -valued Function-like quasi_total Element of bool [:((A #) . f),(A . o):]
C is Relation-like (f #) . f -defined f . o -valued Function-like quasi_total Element of bool [:((f #) . f),(f . o):]
(I,A,f,f,o,F,C) is Relation-like ([|A,f|] #) . f -defined [|A,f|] . o -valued Function-like quasi_total Element of bool [:(([|A,f|] #) . f),([|A,f|] . o):]
([|A,f|] #) . f is non empty set
[|A,f|] . o is non empty set
[:(([|A,f|] #) . f),([|A,f|] . o):] is Relation-like set
bool [:(([|A,f|] #) . f),([|A,f|] . o):] is set
f is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of g * ([|A,f|] #),o * [|A,f|]
o is Relation-like K153() -defined I -valued Function-like V33() countable V61() V62() Element of I *
(A #) . o is non empty set
C is Element of I
A . C is non empty set
[:((A #) . o),(A . C):] is Relation-like set
bool [:((A #) . o),(A . C):] is set
(f #) . o is non empty set
f . C is non empty set
[:((f #) . o),(f . C):] is Relation-like set
bool [:((f #) . o),(f . C):] is set
f is set
g . f is Relation-like K153() -defined Function-like V33() countable V61() V62() set
o . f is set
F is Relation-like (A #) . o -defined A . C -valued Function-like quasi_total Element of bool [:((A #) . o),(A . C):]
s . f is Relation-like Function-like set
Ar is Relation-like (f #) . o -defined f . C -valued Function-like quasi_total Element of bool [:((f #) . o),(f . C):]
f . f is Relation-like Function-like set
f . f is Relation-like Function-like set
(I,A,f,o,C,F,Ar) is Relation-like ([|A,f|] #) . o -defined [|A,f|] . C -valued Function-like quasi_total Element of bool [:(([|A,f|] #) . o),([|A,f|] . C):]
([|A,f|] #) . o is non empty set
[|A,f|] . C is non empty set
[:(([|A,f|] #) . o),([|A,f|] . C):] is Relation-like set
bool [:(([|A,f|] #) . o),([|A,f|] . C):] is set
f is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of g * ([|A,f|] #),o * [|A,f|]
f is Relation-like S -defined Function-like total Function-yielding V25() ManySortedFunction of g * ([|A,f|] #),o * [|A,f|]
c₁₁ is set
f . c₁₁ is Relation-like Function-like set
f . c₁₁ is Relation-like Function-like set
g . c₁₁ is Relation-like K153() -defined Function-like V33() countable V61() V62() set
o . c₁₁ is set
dom o is set
A . (o . c₁₁) is set
(o * A) . c₁₁ is set
f . (o . c₁₁) is set
(o * f) . c₁₁ is set
dom g is set
(A #) . (g . c₁₁) is set
(g * (A #)) . c₁₁ is set
f is Relation-like K153() -defined I -valued Function-like V33() countable V61() V62() Element of I *
(A #) . f is non empty set
f is Element of I
A . f is non empty set
[:((A #) . f),(A . f):] is Relation-like set
bool [:((A #) . f),(A . f):] is set
s . c₁₁ is Relation-like Function-like set
(f #) . (g . c₁₁) is set
(g * (f #)) . c₁₁ is set
(f #) . f is non empty set
f . f is non empty set
[:((f #) . f),(f . f):] is Relation-like set
bool [:((f #) . f),(f . f):] is set
f . c₁₁ is Relation-like Function-like set
o is Relation-like (A #) . f -defined A . f -valued Function-like quasi_total Element of bool [:((A #) . f),(A . f):]
C is Relation-like (f #) . f -defined f . f -valued Function-like quasi_total Element of bool [:((f #) . f),(f . f):]
(I,A,f,f,f,o,C) is Relation-like ([|A,f|] #) . f -defined [|A,f|] . f -valued Function-like quasi_total Element of bool [:(([|A,f|] #) . f),([|A,f|] . f):]
([|A,f|] #) . f is non empty set
[|A,f|] . f is non empty set
[:(([|A,f|] #) . f),([|A,f|] . f):] is Relation-like set
bool [:(([|A,f|] #) . f),([|A,f|] . f):] is set
I is set
S is non empty V59() ManySortedSign
the non-empty MSAlgebra over S is non-empty MSAlgebra over S
I --> the non-empty MSAlgebra over S is Relation-like I -defined { the non-empty MSAlgebra over S} -valued Function-like constant total quasi_total Element of bool [:I,{ the non-empty MSAlgebra over S}:]
{ the non-empty MSAlgebra over S} is non empty set
[:I,{ the non-empty MSAlgebra over S}:] is Relation-like set
bool [:I,{ the non-empty MSAlgebra over S}:] is set
g is Relation-like I -defined Function-like total set
o is set
g . o is set
I is non empty set
S is non empty V59() ManySortedSign
A is Relation-like I -defined Function-like non empty total (I,S)
f is Element of I
A . f is set
I is non empty V59() ManySortedSign
S is MSAlgebra over I
the Sorts of S is Relation-like the carrier of I -defined Function-like non empty total set
the carrier of I is non empty set
rng the Sorts of S is non empty set
union (rng the Sorts of S) is set
I is non empty V59() ManySortedSign
S is non-empty MSAlgebra over I
(I,S) is set
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the carrier of I is non empty set
rng the Sorts of S is non empty V85() set
union (rng the Sorts of S) is set
the Element of the carrier of I is Element of the carrier of I
dom the Sorts of S is non empty set
the Sorts of S . the Element of the carrier of I is non empty set
A is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
A . the Element of the carrier of I is non empty set
g is set
I is non empty set
S is non empty V59() ManySortedSign
A is Relation-like I -defined Function-like non empty total (I,S)
{ (S,(I,S,A,b₁)) where b₁ is Element of I : verum } is set
union { (S,(I,S,A,b₁)) where b₁ is Element of I : verum } is set
I is non empty set
S is non empty V59() ManySortedSign
A is Relation-like I -defined Function-like non empty total (I,S)
(I,S,A) is set
{ (S,(I,S,A,b₁)) where b₁ is Element of I : verum } is set
union { (S,(I,S,A,b₁)) where b₁ is Element of I : verum } is set
the Element of I is Element of I
(I,S,A, the Element of I) is non-empty MSAlgebra over S
(S,(I,S,A, the Element of I)) is non empty set
the Sorts of (I,S,A, the Element of I) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
rng the Sorts of (I,S,A, the Element of I) is non empty V85() set
union (rng the Sorts of (I,S,A, the Element of I)) is set
o is set
I is non empty non void V59() ManySortedSign
the carrier' of I is non empty set
S is MSAlgebra over I
the Sorts of S is Relation-like the carrier of I -defined Function-like non empty total set
the carrier of I is non empty set
A is Element of the carrier' of I
Args (A,S) is Element of rng ( the Sorts of S #)
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
the carrier of I * is functional non empty V63() M8( the carrier of I)
rng ( the Sorts of S #) is non empty set
the_arity_of A is Relation-like K153() -defined the carrier of I -valued Function-like V33() countable V61() V62() Element of the carrier of I *
(the_arity_of A) * the Sorts of S is Relation-like K153() -defined Function-like set
product ((the_arity_of A) * the Sorts of S) is functional with_common_domain product-like set
dom ((the_arity_of A) * the Sorts of S) is set
dom (the_arity_of A) is set
Result (A,S) is Element of rng the Sorts of S
rng the Sorts of S is non empty set
the_result_sort_of A is Element of the carrier of I
the Sorts of S . (the_result_sort_of A) is set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of I,( the carrier of I *):]
[: the carrier' of I,( the carrier of I *):] is Relation-like set
bool [: the carrier' of I,( the carrier of I *):] is set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like set
bool [: the carrier' of I, the carrier of I:] is set
the Arity of I * ( the Sorts of S #) is Relation-like the carrier' of I -defined Function-like non empty total set
the ResultSort of I * the Sorts of S is Relation-like the carrier' of I -defined Function-like non empty total set
dom the Arity of I is set
dom ( the Arity of I * ( the Sorts of S #)) is non empty set
( the Arity of I * ( the Sorts of S #)) . A is set
the Arity of I . A is Relation-like K153() -defined Function-like V33() countable V61() V62() Element of the carrier of I *
( the Sorts of S #) . ( the Arity of I . A) is set
( the Sorts of S #) . (the_arity_of A) is set
rng (the_arity_of A) is set
dom the Sorts of S is non empty set
dom the ResultSort of I is set
dom ( the ResultSort of I * the Sorts of S) is non empty set
( the ResultSort of I * the Sorts of S) . A is set
the ResultSort of I . A is Element of the carrier of I
the Sorts of S . ( the ResultSort of I . A) is set
I is non empty non void V59() ManySortedSign
the carrier' of I is non empty set
S is MSAlgebra over I
A is Element of the carrier' of I
the_arity_of A is Relation-like K153() -defined the carrier of I -valued Function-like V33() countable V61() V62() Element of the carrier of I *
the carrier of I is non empty set
the carrier of I * is functional non empty V63() M8( the carrier of I)
Args (A,S) is Element of rng ( the Sorts of S #)
the Sorts of S is Relation-like the carrier of I -defined Function-like non empty total set
the Sorts of S # is Relation-like the carrier of I * -defined Function-like non empty total set
rng ( the Sorts of S #) is non empty set
(the_arity_of A) * the Sorts of S is Relation-like K153() -defined Function-like set
product ((the_arity_of A) * the Sorts of S) is functional with_common_domain product-like set
I is non empty V59() ManySortedSign
the carrier of I is non empty set
S is non-empty MSAlgebra over I
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
A is non-empty MSAlgebra over I
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of S, the Sorts of A|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the carrier' of I is set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty V63() M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like set
bool [: the carrier' of I,( the carrier of I *):] is set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like set
bool [: the carrier' of I, the carrier of I:] is set
the Charact of S is Relation-like the carrier' of I -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the Sorts of S # is Relation-like non-empty non empty-yielding the carrier of I * -defined Function-like non empty total set
the Arity of I * ( the Sorts of S #) is Relation-like non-empty the carrier' of I -defined Function-like total set
the ResultSort of I * the Sorts of S is Relation-like non-empty the carrier' of I -defined Function-like total set
the Charact of A is Relation-like the carrier' of I -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of I * ( the Sorts of A #), the ResultSort of I * the Sorts of A
the Sorts of A # is Relation-like non-empty non empty-yielding the carrier of I * -defined Function-like non empty total set
the Arity of I * ( the Sorts of A #) is Relation-like non-empty the carrier' of I -defined Function-like total set
the ResultSort of I * the Sorts of A is Relation-like non-empty the carrier' of I -defined Function-like total set
( the carrier of I, the carrier' of I, the Sorts of S, the Sorts of A, the Arity of I, the ResultSort of I, the Charact of S, the Charact of A) is Relation-like the carrier' of I -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of I * ([| the Sorts of S, the Sorts of A|] #), the ResultSort of I * [| the Sorts of S, the Sorts of A|]
[| the Sorts of S, the Sorts of A|] # is Relation-like non-empty non empty-yielding the carrier of I * -defined Function-like non empty total set
the Arity of I * ([| the Sorts of S, the Sorts of A|] #) is Relation-like non-empty the carrier' of I -defined Function-like total set
the ResultSort of I * [| the Sorts of S, the Sorts of A|] is Relation-like non-empty the carrier' of I -defined Function-like total set
MSAlgebra(# [| the Sorts of S, the Sorts of A|],( the carrier of I, the carrier' of I, the Sorts of S, the Sorts of A, the Arity of I, the ResultSort of I, the Charact of S, the Charact of A) #) is strict MSAlgebra over I
I is non empty V59() ManySortedSign
S is non-empty MSAlgebra over I
A is non-empty MSAlgebra over I
(I,S,A) is MSAlgebra over I
the carrier of I is non empty set
the Sorts of S is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the Sorts of A is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
[| the Sorts of S, the Sorts of A|] is Relation-like non-empty non empty-yielding the carrier of I -defined Function-like non empty total set
the carrier' of I is set
the Arity of I is Relation-like the carrier' of I -defined the carrier of I * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of I,( the carrier of I *):]
the carrier of I * is functional non empty V63() M8( the carrier of I)
[: the carrier' of I,( the carrier of I *):] is Relation-like set
bool [: the carrier' of I,( the carrier of I *):] is set
the ResultSort of I is Relation-like the carrier' of I -defined the carrier of I -valued Function-like quasi_total Element of bool [: the carrier' of I, the carrier of I:]
[: the carrier' of I, the carrier of I:] is Relation-like set
bool [: the carrier' of I, the carrier of I:] is set
the Charact of S is Relation-like the carrier' of I -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of I * ( the Sorts of S #), the ResultSort of I * the Sorts of S
the Sorts of S # is Relation-like non-empty non empty-yielding the carrier of I * -defined Function-like non empty total set
the Arity of I * ( the Sorts of S #) is Relation-like non-empty the carrier' of I -defined Function-like total set
the ResultSort of I * the Sorts of S is Relation-like non-empty the carrier' of I -defined Function-like total set
the Charact of A is Relation-like the carrier' of I -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of I * ( the Sorts of A #), the ResultSort of I * the Sorts of A
the Sorts of A # is Relation-like non-empty non empty-yielding the carrier of I * -defined Function-like non empty total set
the Arity of I * ( the Sorts of A #) is Relation-like non-empty the carrier' of I -defined Function-like total set
the ResultSort of I * the Sorts of A is Relation-like non-empty the carrier' of I -defined Function-like total set
( the carrier of I, the carrier' of I, the Sorts of S, the Sorts of A, the Arity of I, the ResultSort of I, the Charact of S, the Charact of A) is Relation-like the carrier' of I -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of I * ([| the Sorts of S, the Sorts of A|] #), the ResultSort of I * [| the Sorts of S, the Sorts of A|]
[| the Sorts of S, the Sorts of A|] # is Relation-like non-empty non empty-yielding the carrier of I * -defined Function-like non empty total set
the Arity of I * ([| the Sorts of S, the Sorts of A|] #) is Relation-like non-empty the carrier' of I -defined Function-like total set
the ResultSort of I * [| the Sorts of S, the Sorts of A|] is Relation-like non-empty the carrier' of I -defined Function-like total set
MSAlgebra(# [| the Sorts of S, the Sorts of A|],( the carrier of I, the carrier' of I, the Sorts of S, the Sorts of A, the Arity of I, the ResultSort of I, the Charact of S, the Charact of A) #) is strict MSAlgebra over I
S is non empty V59() ManySortedSign
the carrier of S is non empty set
I is set
f is Relation-like I -defined Function-like total (I,S)
A is Element of the carrier of S
g is non empty set
o is Relation-like g -defined Function-like non empty total (g,S)
s is Relation-like Function-like set
dom s is set
f is Relation-like I -defined Function-like total set
f is set
c₁₁ is Element of g
(g,S,o,c₁₁) is non-empty MSAlgebra over S
f is MSAlgebra over S
f is MSAlgebra over S
f . f is set
f is Relation-like I -defined Function-like total set
f . f is set
the Sorts of f is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of f . A is set
[[0]] I is Relation-like empty-yielding I -defined Function-like total set
I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]
[:I,{{}}:] is Relation-like set
bool [:I,{{}}:] is set
g is Relation-like I -defined Function-like total set
o is Relation-like I -defined Function-like total set
s is set
g . s is set
o . s is set
f is Element of I
f . f is set
g . f is set
o . f is set
f is MSAlgebra over S
the Sorts of f is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of f . A is set
f is MSAlgebra over S
the Sorts of f is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of f . A is set
S is non empty V59() ManySortedSign
the carrier of S is non empty set
I is set
A is Element of the carrier of S
f is Relation-like I -defined Function-like total (I,S)
(I,S,A,f) is Relation-like I -defined Function-like total set
g is set
(I,S,A,f) . g is set
f . g is set
o is MSAlgebra over S
the Sorts of o is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of o . A is set
I is set
S is non empty V59() ManySortedSign
the carrier of S is non empty set
A is Relation-like I -defined Function-like total (I,S)
f is Relation-like Function-like set
dom f is set
g is Relation-like the carrier of S -defined Function-like non empty total set
o is Element of the carrier of S
g . o is set
(I,S,o,A) is Relation-like non-empty I -defined Function-like total set
product (I,S,o,A) is functional non empty with_common_domain product-like set
f is Relation-like the carrier of S -defined Function-like non empty total set
g is Relation-like the carrier of S -defined Function-like non empty total set
o is set
f . o is set
g . o is set
s is Element of the carrier of S
f . s is set
(I,S,s,A) is Relation-like non-empty I -defined Function-like total set
product (I,S,s,A) is functional non empty with_common_domain product-like set
I is set
S is non empty V59() ManySortedSign
A is Relation-like I -defined Function-like total (I,S)
(I,S,A) is Relation-like the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
f is set
(I,S,A) . f is set
g is Element of the carrier of S
(I,S,A) . g is set
(I,S,g,A) is Relation-like non-empty I -defined Function-like total set
product (I,S,g,A) is functional non empty with_common_domain product-like set
I is set
S is non empty V59() ManySortedSign
A is Relation-like I -defined Function-like total (I,S)
[[0]] I is Relation-like empty-yielding I -defined Function-like total set
I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]
[:I,{{}}:] is Relation-like set
bool [:I,{{}}:] is set
g is non empty set
o is Relation-like g -defined Function-like non empty total (g,S)
the carrier' of S is set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S is non empty set
the carrier of S * is functional non empty V63() M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
s is Relation-like g -defined Function-like non empty total set
dom s is non empty set
f is set
s . f is set
f is Element of g
s . f is set
(g,S,o,f) is non-empty MSAlgebra over S
the Charact of (g,S,o,f) is Relation-like the carrier' of S -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of S * ( the Sorts of (g,S,o,f) #), the ResultSort of S * the Sorts of (g,S,o,f)
the Sorts of (g,S,o,f) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (g,S,o,f) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of (g,S,o,f) #) is Relation-like non-empty the carrier' of S -defined Function-like total set
the ResultSort of S * the Sorts of (g,S,o,f) is Relation-like non-empty the carrier' of S -defined Function-like total set
f is Relation-like I -defined Function-like total Function-yielding V25() set
f is set
c₁₁ is Element of g
(g,S,o,c₁₁) is non-empty MSAlgebra over S
f is MSAlgebra over S
f is MSAlgebra over S
A . f is set
f is Relation-like I -defined Function-like total Function-yielding V25() set
f . f is Relation-like Function-like set
the Charact of f is Relation-like the carrier' of S -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of S * ( the Sorts of f #), the ResultSort of S * the Sorts of f
the Sorts of f is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of f # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of f #) is Relation-like the carrier' of S -defined Function-like total set
the ResultSort of S * the Sorts of f is Relation-like the carrier' of S -defined Function-like total set
f is Relation-like I -defined Function-like total Function-yielding V25() set
f is Relation-like I -defined Function-like total Function-yielding V25() set
g is Relation-like I -defined Function-like total Function-yielding V25() set
o is set
f . o is Relation-like Function-like set
g . o is Relation-like Function-like set
s is Element of I
A . s is set
f . s is Relation-like Function-like set
g . s is Relation-like Function-like set
f is MSAlgebra over S
the Charact of f is Relation-like the carrier' of S -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of S * ( the Sorts of f #), the ResultSort of S * the Sorts of f
the carrier' of S is set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S is non empty set
the carrier of S * is functional non empty V63() M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
the Sorts of f is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of f # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of f #) is Relation-like the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * the Sorts of f is Relation-like the carrier' of S -defined Function-like total set
f is MSAlgebra over S
the Charact of f is Relation-like the carrier' of S -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of S * ( the Sorts of f #), the ResultSort of S * the Sorts of f
the Sorts of f is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of f # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of f #) is Relation-like the carrier' of S -defined Function-like total set
the ResultSort of S * the Sorts of f is Relation-like the carrier' of S -defined Function-like total set
I is set
S is non empty V59() ManySortedSign
the carrier' of S is set
[:I, the carrier' of S:] is Relation-like set
A is Relation-like I -defined Function-like total (I,S)
(I,S,A) is Relation-like I -defined Function-like total Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
dom (uncurry (I,S,A)) is set
f is set
dom (I,S,A) is set
g is set
s is set
[g,s] is V15() set
{g,s} is non empty set
{g} is non empty set
{{g,s},{g}} is non empty set
o is Relation-like Function-like set
(I,S,A) . g is Relation-like Function-like set
dom o is set
f is Element of I
A . f is set
(I,S,A) . f is Relation-like Function-like set
f is MSAlgebra over S
the Charact of f is Relation-like the carrier' of S -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of S * ( the Sorts of f #), the ResultSort of S * the Sorts of f
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S is non empty set
the carrier of S * is functional non empty V63() M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
the Sorts of f is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of f # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of f #) is Relation-like the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * the Sorts of f is Relation-like the carrier' of S -defined Function-like total set
f is set
g is set
o is set
[g,o] is V15() set
{g,o} is non empty set
{g} is non empty set
{{g,o},{g}} is non empty set
s is Element of I
A . s is set
(I,S,A) . s is Relation-like Function-like set
f is MSAlgebra over S
the Charact of f is Relation-like the carrier' of S -defined Function-like total Function-yielding V25() ManySortedFunction of the Arity of S * ( the Sorts of f #), the ResultSort of S * the Sorts of f
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S is non empty set
the carrier of S * is functional non empty V63() M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
the Sorts of f is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of f # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of f #) is Relation-like the carrier' of S -defined Function-like total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * the Sorts of f is Relation-like the carrier' of S -defined Function-like total set
dom the Charact of f is set
dom (I,S,A) is set
I is non empty set
S is non empty non void V59() ManySortedSign
the carrier' of S is non empty set
A is Relation-like I -defined Function-like non empty total (I,S)
(I,S,A) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
rng (uncurry (I,S,A)) is set
Funcs (I,(rng (uncurry (I,S,A)))) is set
Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (I,S,A)))))) is set
dom (uncurry (I,S,A)) is set
[:I, the carrier' of S:] is Relation-like set
Funcs ([:I, the carrier' of S:],(rng (uncurry (I,S,A)))) is set
I is set
S is non empty non void V59() ManySortedSign
the carrier' of S is non empty set
A is Relation-like I -defined Function-like total (I,S)
(I,S,A) is Relation-like I -defined Function-like total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
f is Element of the carrier' of S
(commute (I,S,A)) . f is Relation-like Function-like set
dom (uncurry (I,S,A)) is set
[:I, the carrier' of S:] is Relation-like set
rng (uncurry (I,S,A)) is set
Funcs (I,(rng (uncurry (I,S,A)))) is set
Funcs ( the carrier' of S,(Funcs (I,(rng (uncurry (I,S,A)))))) is set
rng (commute (I,S,A)) is set
s is Relation-like Function-like set
dom s is set
rng s is set
s is Relation-like Function-like set
dom s is set
rng s is set
s is Relation-like Function-like set
dom s is set
rng s is set
f is Relation-like I -defined Function-like total set
dom f is set
f is set
f . f is set
f is Element of I
[f,f] is V15() set
{f,f} is non empty set
{f} is non empty set
{{f,f},{f}} is non empty set
[f,f] `1 is set
[f,f] `2 is set
A . f is set
(I,S,A) . f is Relation-like Function-like set
c₁₁ is MSAlgebra over S
the Charact of c₁₁ is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ( the Sorts of c₁₁ #), the ResultSort of S * the Sorts of c₁₁
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S is non empty set
the carrier of S * is functional non empty V63() M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
the Sorts of c₁₁ is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of c₁₁ # is Relation-like the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of c₁₁ #) is Relation-like the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * the Sorts of c₁₁ is Relation-like the carrier' of S -defined Function-like non empty total set
f . f is set
(uncurry (I,S,A)) . (f,f) is set
(uncurry (I,S,A)) . [f,f] is set
the Charact of c₁₁ . f is Relation-like Function-like set
Den (f,c₁₁) is Relation-like Args (f,c₁₁) -defined Result (f,c₁₁) -valued Function-like quasi_total Element of bool [:(Args (f,c₁₁)),(Result (f,c₁₁)):]
Args (f,c₁₁) is Element of rng ( the Sorts of c₁₁ #)
rng ( the Sorts of c₁₁ #) is non empty set
Result (f,c₁₁) is Element of rng the Sorts of c₁₁
rng the Sorts of c₁₁ is non empty set
[:(Args (f,c₁₁)),(Result (f,c₁₁)):] is Relation-like set
bool [:(Args (f,c₁₁)),(Result (f,c₁₁)):] is set
[[0]] I is Relation-like empty-yielding I -defined Function-like total set
I --> {} is Relation-like I -defined {{}} -valued Function-like constant total quasi_total Function-yielding V25() Element of bool [:I,{{}}:]
[:I,{{}}:] is Relation-like set
bool [:I,{{}}:] is set
s is Relation-like I -defined Function-like total Function-yielding V25() set
(commute {}) . f is Relation-like Function-like set
I is non empty set
S is Element of I
A is non empty non void V59() ManySortedSign
the carrier' of A is non empty set
f is Relation-like I -defined Function-like non empty total (I,A)
(I,A,f,S) is non-empty MSAlgebra over A
g is Element of the carrier' of A
(I,A,f,g) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
(I,A,f) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
commute (I,A,f) is Relation-like Function-like Function-yielding V25() set
uncurry (I,A,f) is Relation-like Function-like set
curry' (uncurry (I,A,f)) is Relation-like Function-like set
(commute (I,A,f)) . g is Relation-like Function-like set
(I,A,f,g) . S is Relation-like Function-like set
Den (g,(I,A,f,S)) is Relation-like Args (g,(I,A,f,S)) -defined Result (g,(I,A,f,S)) -valued Function-like quasi_total Element of bool [:(Args (g,(I,A,f,S))),(Result (g,(I,A,f,S))):]
Args (g,(I,A,f,S)) is non empty Element of rng ( the Sorts of (I,A,f,S) #)
the carrier of A is non empty set
the Sorts of (I,A,f,S) is Relation-like non-empty non empty-yielding the carrier of A -defined Function-like non empty total set
the Sorts of (I,A,f,S) # is Relation-like non-empty non empty-yielding the carrier of A * -defined Function-like non empty total set
the carrier of A * is functional non empty V63() M8( the carrier of A)
rng ( the Sorts of (I,A,f,S) #) is non empty V85() set
Result (g,(I,A,f,S)) is non empty Element of rng the Sorts of (I,A,f,S)
rng the Sorts of (I,A,f,S) is non empty V85() set
[:(Args (g,(I,A,f,S))),(Result (g,(I,A,f,S))):] is Relation-like set
bool [:(Args (g,(I,A,f,S))),(Result (g,(I,A,f,S))):] is set
[S,g] is V15() set
{S,g} is non empty set
{S} is non empty set
{{S,g},{S}} is non empty set
[S,g] `1 is set
[S,g] `2 is set
(I,A,f) . S is Relation-like Function-like set
dom (uncurry (I,A,f)) is set
[:I, the carrier' of A:] is Relation-like set
(curry' (uncurry (I,A,f))) . g is set
rng (uncurry (I,A,f)) is set
f is Relation-like Function-like set
dom f is set
rng f is set
f . S is set
(uncurry (I,A,f)) . (S,g) is set
(uncurry (I,A,f)) . [S,g] is set
the Charact of (I,A,f,S) is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of A * ( the Sorts of (I,A,f,S) #), the ResultSort of A * the Sorts of (I,A,f,S)
the Arity of A is Relation-like the carrier' of A -defined the carrier of A * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of A,( the carrier of A *):]
[: the carrier' of A,( the carrier of A *):] is Relation-like set
bool [: the carrier' of A,( the carrier of A *):] is set
the Arity of A * ( the Sorts of (I,A,f,S) #) is Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like non empty total set
the ResultSort of A is Relation-like the carrier' of A -defined the carrier of A -valued Function-like quasi_total Element of bool [: the carrier' of A, the carrier of A:]
[: the carrier' of A, the carrier of A:] is Relation-like set
bool [: the carrier' of A, the carrier of A:] is set
the ResultSort of A * the Sorts of (I,A,f,S) is Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like non empty total set
the Charact of (I,A,f,S) . g is Relation-like Function-like set
f is MSAlgebra over A
the Charact of f is Relation-like the carrier' of A -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of A * ( the Sorts of f #), the ResultSort of A * the Sorts of f
the Sorts of f is Relation-like the carrier of A -defined Function-like non empty total set
the Sorts of f # is Relation-like the carrier of A * -defined Function-like non empty total set
the Arity of A * ( the Sorts of f #) is Relation-like the carrier' of A -defined Function-like non empty total set
the ResultSort of A * the Sorts of f is Relation-like the carrier' of A -defined Function-like non empty total set
I is non empty set
S is non empty non void V59() ManySortedSign
the carrier' of S is non empty set
A is Relation-like I -defined Function-like non empty total (I,S)
f is Element of the carrier' of S
(I,S,A,f) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . f is Relation-like Function-like set
((I,S,A,f)) is Relation-like product (doms (I,S,A,f)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,f) is Relation-like Function-like set
product (doms (I,S,A,f)) is functional with_common_domain product-like set
rng ((I,S,A,f)) is set
g is set
dom ((I,S,A,f)) is set
o is set
((I,S,A,f)) . o is Relation-like Function-like set
I is non empty set
S is non empty non void V59() ManySortedSign
the carrier' of S is non empty set
A is Relation-like I -defined Function-like non empty total (I,S)
f is Element of the carrier' of S
(I,S,A,f) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . f is Relation-like Function-like set
((I,S,A,f)) is Relation-like product (doms (I,S,A,f)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,f) is Relation-like Function-like set
product (doms (I,S,A,f)) is functional with_common_domain product-like set
rng ((I,S,A,f)) is set
g is Relation-like Function-like set
dom g is set
dom (I,S,A,f) is non empty set
rng (I,S,A,f) is non empty set
SubFuncs (rng (I,S,A,f)) is set
o is set
s is set
(I,S,A,f) . s is Relation-like Function-like set
dom ((I,S,A,f)) is set
o is set
((I,S,A,f)) . o is Relation-like Function-like set
dom (doms (I,S,A,f)) is set
s is Relation-like Function-like set
dom s is set
(I,S,A,f) .. s is Relation-like Function-like set
f is Element of I
g . f is set
(I,S,A,f) is non-empty MSAlgebra over S
Result (f,(I,S,A,f)) is non empty Element of rng the Sorts of (I,S,A,f)
the Sorts of (I,S,A,f) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
rng the Sorts of (I,S,A,f) is non empty V85() set
(I,S,A,f) . f is Relation-like Function-like set
Den (f,(I,S,A,f)) is Relation-like Args (f,(I,S,A,f)) -defined Result (f,(I,S,A,f)) -valued Function-like quasi_total Element of bool [:(Args (f,(I,S,A,f))),(Result (f,(I,S,A,f))):]
Args (f,(I,S,A,f)) is non empty Element of rng ( the Sorts of (I,S,A,f) #)
the Sorts of (I,S,A,f) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the carrier of S * is functional non empty V63() M8( the carrier of S)
rng ( the Sorts of (I,S,A,f) #) is non empty V85() set
[:(Args (f,(I,S,A,f))),(Result (f,(I,S,A,f))):] is Relation-like set
bool [:(Args (f,(I,S,A,f))),(Result (f,(I,S,A,f))):] is set
(I,S,A,f) " (SubFuncs (rng (I,S,A,f))) is set
s . f is set
(doms (I,S,A,f)) . f is set
dom (Den (f,(I,S,A,f))) is set
(Den (f,(I,S,A,f))) . (s . f) is set
rng (Den (f,(I,S,A,f))) is set
I is non empty set
S is non empty non void V59() ManySortedSign
the carrier' of S is non empty set
A is Relation-like I -defined Function-like non empty total (I,S)
(I,S,A) is non empty set
{ (S,(I,S,A,b₁)) where b₁ is Element of I : verum } is set
union { (S,(I,S,A,b₁)) where b₁ is Element of I : verum } is set
f is Element of the carrier' of S
(I,S,A,f) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . f is Relation-like Function-like set
((I,S,A,f)) is Relation-like product (doms (I,S,A,f)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,f) is Relation-like Function-like set
product (doms (I,S,A,f)) is functional with_common_domain product-like set
dom ((I,S,A,f)) is set
the_arity_of f is Relation-like K153() -defined the carrier of S -valued Function-like V33() countable V61() V62() Element of the carrier of S *
the carrier of S is non empty set
the carrier of S * is functional non empty V63() M8( the carrier of S)
dom (the_arity_of f) is set
Funcs ((dom (the_arity_of f)),(I,S,A)) is non empty FUNCTION_DOMAIN of dom (the_arity_of f),(I,S,A)
g is Relation-like Function-like set
dom g is set
rng g is set
dom (I,S,A,f) is non empty set
rng (I,S,A,f) is non empty set
SubFuncs (rng (I,S,A,f)) is set
o is set
s is set
(I,S,A,f) . s is Relation-like Function-like set
dom (doms (I,S,A,f)) is set
(I,S,A,f) " (SubFuncs (rng (I,S,A,f))) is set
o is Element of I
g . o is set
(I,S,A,o) is non-empty MSAlgebra over S
Args (f,(I,S,A,o)) is non empty Element of rng ( the Sorts of (I,S,A,o) #)
the Sorts of (I,S,A,o) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (I,S,A,o) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
rng ( the Sorts of (I,S,A,o) #) is non empty V85() set
(I,S,A,f) . o is Relation-like Function-like set
Den (f,(I,S,A,o)) is Relation-like Args (f,(I,S,A,o)) -defined Result (f,(I,S,A,o)) -valued Function-like quasi_total Element of bool [:(Args (f,(I,S,A,o))),(Result (f,(I,S,A,o))):]
Result (f,(I,S,A,o)) is non empty Element of rng the Sorts of (I,S,A,o)
rng the Sorts of (I,S,A,o) is non empty V85() set
[:(Args (f,(I,S,A,o))),(Result (f,(I,S,A,o))):] is Relation-like set
bool [:(Args (f,(I,S,A,o))),(Result (f,(I,S,A,o))):] is set
(doms (I,S,A,f)) . o is set
dom (Den (f,(I,S,A,o))) is set
o is set
s is set
g . s is set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
f is Element of I
(I,S,A,f) is non-empty MSAlgebra over S
the Sorts of (I,S,A,f) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (I,S,A,f) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of (I,S,A,f) #) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
dom the Arity of S is set
dom ( the Arity of S * ( the Sorts of (I,S,A,f) #)) is non empty set
Args (f,(I,S,A,f)) is non empty Element of rng ( the Sorts of (I,S,A,f) #)
rng ( the Sorts of (I,S,A,f) #) is non empty V85() set
( the Arity of S * ( the Sorts of (I,S,A,f) #)) . f is non empty set
the Arity of S . f is Relation-like K153() -defined Function-like V33() countable V61() V62() Element of the carrier of S *
( the Sorts of (I,S,A,f) #) . ( the Arity of S . f) is non empty set
( the Sorts of (I,S,A,f) #) . (the_arity_of f) is non empty set
(the_arity_of f) * the Sorts of (I,S,A,f) is Relation-like non-empty K153() -defined Function-like set
product ((the_arity_of f) * the Sorts of (I,S,A,f)) is functional non empty with_common_domain product-like set
dom ((the_arity_of f) * the Sorts of (I,S,A,f)) is set
C is Relation-like Function-like set
dom C is set
rng (the_arity_of f) is set
dom the Sorts of (I,S,A,f) is non empty set
rng C is set
(S,(I,S,A,f)) is non empty set
rng the Sorts of (I,S,A,f) is non empty V85() set
union (rng the Sorts of (I,S,A,f)) is set
F is set
Ar is set
C . Ar is set
(the_arity_of f) . Ar is set
the Sorts of (I,S,A,f) . ((the_arity_of f) . Ar) is set
((the_arity_of f) * the Sorts of (I,S,A,f)) . Ar is set
I is non empty set
S is non empty non void V59() ManySortedSign
the carrier' of S is non empty set
A is Relation-like I -defined Function-like non empty total (I,S)
f is Element of the carrier' of S
(I,S,A,f) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like non empty total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . f is Relation-like Function-like set
doms (I,S,A,f) is Relation-like Function-like set
dom (doms (I,S,A,f)) is set
rng (I,S,A,f) is non empty set
SubFuncs (rng (I,S,A,f)) is set
g is set
dom (I,S,A,f) is non empty set
o is set
(I,S,A,f) . o is Relation-like Function-like set
(I,S,A,f) " (SubFuncs (rng (I,S,A,f))) is set
dom (I,S,A,f) is non empty set
g is Element of I
(doms (I,S,A,f)) . g is set
(I,S,A,g) is non-empty MSAlgebra over S
Args (f,(I,S,A,g)) is non empty Element of rng ( the Sorts of (I,S,A,g) #)
the carrier of S is non empty set
the Sorts of (I,S,A,g) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (I,S,A,g) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the carrier of S * is functional non empty V63() M8( the carrier of S)
rng ( the Sorts of (I,S,A,g) #) is non empty V85() set
(I,S,A,f) . g is Relation-like Function-like set
Den (f,(I,S,A,g)) is Relation-like Args (f,(I,S,A,g)) -defined Result (f,(I,S,A,g)) -valued Function-like quasi_total Element of bool [:(Args (f,(I,S,A,g))),(Result (f,(I,S,A,g))):]
Result (f,(I,S,A,g)) is non empty Element of rng the Sorts of (I,S,A,g)
rng the Sorts of (I,S,A,g) is non empty V85() set
[:(Args (f,(I,S,A,g))),(Result (f,(I,S,A,g))):] is Relation-like set
bool [:(Args (f,(I,S,A,g))),(Result (f,(I,S,A,g))):] is set
dom (Den (f,(I,S,A,g))) is set
g is Element of I
(doms (I,S,A,f)) . g is set
(I,S,A,g) is non-empty MSAlgebra over S
Args (f,(I,S,A,g)) is non empty Element of rng ( the Sorts of (I,S,A,g) #)
the carrier of S is non empty set
the Sorts of (I,S,A,g) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (I,S,A,g) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the carrier of S * is functional non empty V63() M8( the carrier of S)
rng ( the Sorts of (I,S,A,g) #) is non empty V85() set
I is set
S is non empty non void V59() ManySortedSign
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S is non empty set
the carrier of S * is functional non empty V63() M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
A is Relation-like I -defined Function-like total (I,S)
(I,S,A) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
(I,S,A) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the Arity of S * ((I,S,A) #) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (I,S,A) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
s is set
f is Element of the carrier' of S
the_arity_of f is Relation-like K153() -defined the carrier of S -valued Function-like V33() countable V61() V62() Element of the carrier of S *
(I,S,A,f) is Relation-like I -defined Function-like total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . f is Relation-like Function-like set
commute (I,S,A,f) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A,f) is Relation-like Function-like set
curry' (uncurry (I,S,A,f)) is Relation-like Function-like set
((I,S,A,f)) is Relation-like product (doms (I,S,A,f)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,f) is Relation-like Function-like set
product (doms (I,S,A,f)) is functional with_common_domain product-like set
(((I,S,A,f))) is Relation-like Function-like set
IFEQ ((the_arity_of f),{},(commute (I,S,A,f)),(((I,S,A,f)))) is set
f is Element of the carrier' of S
the_arity_of f is Relation-like K153() -defined the carrier of S -valued Function-like V33() countable V61() V62() Element of the carrier of S *
(I,S,A,f) is Relation-like I -defined Function-like total Function-yielding V25() set
(commute (I,S,A)) . f is Relation-like Function-like set
commute (I,S,A,f) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A,f) is Relation-like Function-like set
curry' (uncurry (I,S,A,f)) is Relation-like Function-like set
((I,S,A,f)) is Relation-like product (doms (I,S,A,f)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,f) is Relation-like Function-like set
product (doms (I,S,A,f)) is functional with_common_domain product-like set
(((I,S,A,f))) is Relation-like Function-like set
IFEQ ((the_arity_of f),{},(commute (I,S,A,f)),(((I,S,A,f)))) is set
s is Relation-like Function-like set
dom s is set
f is Relation-like the carrier' of S -defined Function-like non empty total set
dom f is non empty set
f is set
f . f is set
f is Element of the carrier' of S
the_arity_of f is Relation-like K153() -defined the carrier of S -valued Function-like V33() countable V61() V62() Element of the carrier of S *
(I,S,A,f) is Relation-like I -defined Function-like total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . f is Relation-like Function-like set
commute (I,S,A,f) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A,f) is Relation-like Function-like set
curry' (uncurry (I,S,A,f)) is Relation-like Function-like set
((I,S,A,f)) is Relation-like product (doms (I,S,A,f)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,f) is Relation-like Function-like set
product (doms (I,S,A,f)) is functional with_common_domain product-like set
(((I,S,A,f))) is Relation-like Function-like set
IFEQ ((the_arity_of f),{},(commute (I,S,A,f)),(((I,S,A,f)))) is set
f is Element of the carrier' of S
the_arity_of f is Relation-like K153() -defined the carrier of S -valued Function-like V33() countable V61() V62() Element of the carrier of S *
(I,S,A,f) is Relation-like I -defined Function-like total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . f is Relation-like Function-like set
commute (I,S,A,f) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A,f) is Relation-like Function-like set
curry' (uncurry (I,S,A,f)) is Relation-like Function-like set
((I,S,A,f)) is Relation-like product (doms (I,S,A,f)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,f) is Relation-like Function-like set
product (doms (I,S,A,f)) is functional with_common_domain product-like set
(((I,S,A,f))) is Relation-like Function-like set
IFEQ ((the_arity_of f),{},(commute (I,S,A,f)),(((I,S,A,f)))) is set
f is Element of the carrier' of S
the_arity_of f is Relation-like K153() -defined the carrier of S -valued Function-like V33() countable V61() V62() Element of the carrier of S *
f is non empty set
f is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() set
f is set
f . f is Relation-like Function-like set
( the Arity of S * ((I,S,A) #)) . f is set
( the ResultSort of S * (I,S,A)) . f is set
[:(( the Arity of S * ((I,S,A) #)) . f),(( the ResultSort of S * (I,S,A)) . f):] is Relation-like set
bool [:(( the Arity of S * ((I,S,A) #)) . f),(( the ResultSort of S * (I,S,A)) . f):] is set
f is Element of the carrier' of S
the_arity_of f is Relation-like K153() -defined the carrier of S -valued Function-like V33() countable V61() V62() Element of the carrier of S *
(I,S,A,f) is Relation-like I -defined Function-like total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . f is Relation-like Function-like set
((I,S,A,f)) is Relation-like product (doms (I,S,A,f)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,f) is Relation-like Function-like set
product (doms (I,S,A,f)) is functional with_common_domain product-like set
(((I,S,A,f))) is Relation-like Function-like set
commute (I,S,A,f) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A,f) is Relation-like Function-like set
curry' (uncurry (I,S,A,f)) is Relation-like Function-like set
rng (the_arity_of f) is set
dom the Arity of S is set
dom ( the Arity of S * ((I,S,A) #)) is non empty set
( the Arity of S * ((I,S,A) #)) . f is non empty set
the Arity of S . f is Relation-like K153() -defined Function-like V33() countable V61() V62() Element of the carrier of S *
((I,S,A) #) . ( the Arity of S . f) is non empty set
((I,S,A) #) . (the_arity_of f) is non empty set
(the_arity_of f) * (I,S,A) is Relation-like non-empty K153() -defined Function-like set
product ((the_arity_of f) * (I,S,A)) is functional non empty with_common_domain product-like set
dom the ResultSort of S is set
dom ( the ResultSort of S * (I,S,A)) is non empty set
( the ResultSort of S * (I,S,A)) . f is non empty set
the ResultSort of S . f is Element of the carrier of S
(I,S,A) . ( the ResultSort of S . f) is non empty set
the_result_sort_of f is Element of the carrier of S
(I,S,A) . (the_result_sort_of f) is non empty set
(I,S,(the_result_sort_of f),A) is Relation-like non-empty I -defined Function-like total set
product (I,S,(the_result_sort_of f),A) is functional non empty with_common_domain product-like set
dom (I,S,A) is non empty set
dom ((the_arity_of f) * (I,S,A)) is set
dom (the_arity_of f) is set
rng (I,S,A,f) is set
c₁₁ is Relation-like f -defined Function-like non empty total (f,S)
(f,S,c₁₁) is non empty set
{ (S,(f,S,c₁₁,b₁)) where b₁ is Element of f : verum } is set
union { (S,(f,S,c₁₁,b₁)) where b₁ is Element of f : verum } is set
Funcs ({{}},(f,S,c₁₁)) is non empty FUNCTION_DOMAIN of {{}},(f,S,c₁₁)
CA is set
dom (I,S,A,f) is set
x is set
(I,S,A,f) . x is Relation-like Function-like set
g is Element of f
(f,S,c₁₁,g) is non-empty MSAlgebra over S
the Sorts of (f,S,c₁₁,g) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
(S,(f,S,c₁₁,g)) is non empty set
rng the Sorts of (f,S,c₁₁,g) is non empty V85() set
union (rng the Sorts of (f,S,c₁₁,g)) is set
dom the Sorts of (f,S,c₁₁,g) is non empty set
the Sorts of (f,S,c₁₁,g) . (the_result_sort_of f) is non empty set
Den (f,(f,S,c₁₁,g)) is Relation-like Args (f,(f,S,c₁₁,g)) -defined Result (f,(f,S,c₁₁,g)) -valued Function-like quasi_total Element of bool [:(Args (f,(f,S,c₁₁,g))),(Result (f,(f,S,c₁₁,g))):]
Args (f,(f,S,c₁₁,g)) is non empty Element of rng ( the Sorts of (f,S,c₁₁,g) #)
the Sorts of (f,S,c₁₁,g) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
rng ( the Sorts of (f,S,c₁₁,g) #) is non empty V85() set
Result (f,(f,S,c₁₁,g)) is non empty Element of rng the Sorts of (f,S,c₁₁,g)
[:(Args (f,(f,S,c₁₁,g))),(Result (f,(f,S,c₁₁,g))):] is Relation-like set
bool [:(Args (f,(f,S,c₁₁,g))),(Result (f,(f,S,c₁₁,g))):] is set
rng (Den (f,(f,S,c₁₁,g))) is set
dom (Den (f,(f,S,c₁₁,g))) is set
dom (I,S,A,f) is set
Funcs (I,(Funcs ({{}},(f,S,c₁₁)))) is non empty FUNCTION_DOMAIN of I, Funcs ({{}},(f,S,c₁₁))
Funcs (I,(f,S,c₁₁)) is non empty FUNCTION_DOMAIN of I,(f,S,c₁₁)
Funcs ({{}},(Funcs (I,(f,S,c₁₁)))) is non empty FUNCTION_DOMAIN of {{}}, Funcs (I,(f,S,c₁₁))
rng (commute (I,S,A,f)) is set
CA is set
dom (I,S,(the_result_sort_of f),A) is set
dom (commute (I,S,A,f)) is set
x is set
(commute (I,S,A,f)) . x is Relation-like Function-like set
g is Relation-like Function-like set
f is set
g . f is set
(I,S,(the_result_sort_of f),A) . f is set
g is Element of f
A . g is set
(I,S,(the_result_sort_of f),A) . g is set
(f,S,c₁₁,g) is non-empty MSAlgebra over S
Den (f,(f,S,c₁₁,g)) is Relation-like Args (f,(f,S,c₁₁,g)) -defined Result (f,(f,S,c₁₁,g)) -valued Function-like quasi_total Element of bool [:(Args (f,(f,S,c₁₁,g))),(Result (f,(f,S,c₁₁,g))):]
Args (f,(f,S,c₁₁,g)) is non empty Element of rng ( the Sorts of (f,S,c₁₁,g) #)
the Sorts of (f,S,c₁₁,g) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (f,S,c₁₁,g) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
rng ( the Sorts of (f,S,c₁₁,g) #) is non empty V85() set
Result (f,(f,S,c₁₁,g)) is non empty Element of rng the Sorts of (f,S,c₁₁,g)
rng the Sorts of (f,S,c₁₁,g) is non empty V85() set
[:(Args (f,(f,S,c₁₁,g))),(Result (f,(f,S,c₁₁,g))):] is Relation-like set
bool [:(Args (f,(f,S,c₁₁,g))),(Result (f,(f,S,c₁₁,g))):] is set
dom (Den (f,(f,S,c₁₁,g))) is set
(Den (f,(f,S,c₁₁,g))) . x is set
rng (Den (f,(f,S,c₁₁,g))) is set
h is Relation-like Function-like set
dom h is set
rng h is set
(I,S,A,f) . g is Relation-like Function-like set
g . g is set
h is Relation-like Function-like set
dom h is set
rng h is set
h is MSAlgebra over S
the Sorts of h is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of h . (the_result_sort_of f) 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
rng f is set
IFEQ ((the_arity_of f),{},(commute (I,S,A,f)),(((I,S,A,f)))) is set
CA is Relation-like Function-like set
dom CA is set
rng CA is set
dom (((I,S,A,f))) is set
rs is set
dom ((I,S,A,f)) is set
CA is Relation-like Function-like set
commute CA is Relation-like Function-like Function-yielding V25() set
uncurry CA is Relation-like Function-like set
curry' (uncurry CA) is Relation-like Function-like set
rng CA is set
c₁₁ is Relation-like f -defined Function-like non empty total (f,S)
(f,S,c₁₁) is non empty set
{ (S,(f,S,c₁₁,b₁)) where b₁ is Element of f : verum } is set
union { (S,(f,S,c₁₁,b₁)) where b₁ is Element of f : verum } is set
Funcs ((dom (the_arity_of f)),(f,S,c₁₁)) is non empty FUNCTION_DOMAIN of dom (the_arity_of f),(f,S,c₁₁)
dom CA is set
Funcs (I,(Funcs ((dom (the_arity_of f)),(f,S,c₁₁)))) is non empty FUNCTION_DOMAIN of I, Funcs ((dom (the_arity_of f)),(f,S,c₁₁))
Funcs (I,(f,S,c₁₁)) is non empty FUNCTION_DOMAIN of I,(f,S,c₁₁)
Funcs ((dom (the_arity_of f)),(Funcs (I,(f,S,c₁₁)))) is non empty FUNCTION_DOMAIN of dom (the_arity_of f), Funcs (I,(f,S,c₁₁))
g is set
(commute CA) . g is Relation-like Function-like set
((the_arity_of f) * (I,S,A)) . g is set
(the_arity_of f) . g is set
rng (commute CA) 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
f is Element of the carrier of S
(I,S,f,A) is Relation-like non-empty I -defined Function-like total set
dom (I,S,f,A) is set
h is set
g . h is set
(I,S,f,A) . h is set
j is Element of f
(f,S,c₁₁,j) is non-empty MSAlgebra over S
the Sorts of (f,S,c₁₁,j) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the Sorts of (f,S,c₁₁,j) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the Arity of S * ( the Sorts of (f,S,c₁₁,j) #) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
dom ( the Arity of S * ( the Sorts of (f,S,c₁₁,j) #)) is non empty set
Args (f,(f,S,c₁₁,j)) is non empty Element of rng ( the Sorts of (f,S,c₁₁,j) #)
rng ( the Sorts of (f,S,c₁₁,j) #) is non empty V85() set
( the Arity of S * ( the Sorts of (f,S,c₁₁,j) #)) . f is non empty set
( the Sorts of (f,S,c₁₁,j) #) . ( the Arity of S . f) is non empty set
( the Sorts of (f,S,c₁₁,j) #) . (the_arity_of f) is non empty set
(the_arity_of f) * the Sorts of (f,S,c₁₁,j) is Relation-like non-empty K153() -defined Function-like set
product ((the_arity_of f) * the Sorts of (f,S,c₁₁,j)) is functional non empty with_common_domain product-like set
CA . j is set
i is Relation-like Function-like set
dom i is set
rng i is set
A . j is set
(I,S,f,A) . j is set
dom the Sorts of (f,S,c₁₁,j) is non empty set
dom ((the_arity_of f) * the Sorts of (f,S,c₁₁,j)) is set
((the_arity_of f) * the Sorts of (f,S,c₁₁,j)) . g is set
the Sorts of (f,S,c₁₁,j) . f is non empty set
i . g is set
k is MSAlgebra over S
the Sorts of k is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of k . f is set
(I,S,A) . f is non empty set
product (I,S,f,A) is functional non empty with_common_domain product-like set
g is Relation-like Function-like set
dom g is set
rng g is set
rs is set
CA is Relation-like Function-like set
dom CA is set
rng CA is set
c₁₁ is Relation-like f -defined Function-like non empty total (f,S)
(f,S,c₁₁) is non empty set
{ (S,(f,S,c₁₁,b₁)) where b₁ is Element of f : verum } is set
union { (S,(f,S,c₁₁,b₁)) where b₁ is Element of f : verum } is set
Funcs (I,(f,S,c₁₁)) is non empty FUNCTION_DOMAIN of I,(f,S,c₁₁)
x is set
g is set
CA . g is set
(the_arity_of f) . g is set
((the_arity_of f) * (I,S,A)) . g is set
f is Element of the carrier of S
(I,S,A) . f is non empty set
(I,S,f,A) is Relation-like non-empty I -defined Function-like total set
product (I,S,f,A) is functional non empty with_common_domain product-like set
dom (I,S,f,A) is set
g is Relation-like Function-like set
dom g is set
rng g is set
h is set
j is set
g . j is set
i is Element of f
A . i is set
(I,S,f,A) . i is set
(f,S,c₁₁,i) is non-empty MSAlgebra over S
the Sorts of (f,S,c₁₁,i) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
dom the Sorts of (f,S,c₁₁,i) is non empty set
rng the Sorts of (f,S,c₁₁,i) is non empty V85() set
k is MSAlgebra over S
the Sorts of k is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of k . f is set
g . i is set
(S,(f,S,c₁₁,i)) is non empty set
union (rng the Sorts of (f,S,c₁₁,i)) is set
Funcs ((dom (the_arity_of f)),(Funcs (I,(f,S,c₁₁)))) is non empty FUNCTION_DOMAIN of dom (the_arity_of f), Funcs (I,(f,S,c₁₁))
commute CA is Relation-like Function-like Function-yielding V25() set
uncurry CA is Relation-like Function-like set
curry' (uncurry CA) is Relation-like Function-like set
commute (commute CA) is Relation-like Function-like Function-yielding V25() set
uncurry (commute CA) is Relation-like Function-like set
curry' (uncurry (commute CA)) is Relation-like Function-like set
Funcs ((dom (the_arity_of f)),(f,S,c₁₁)) is non empty FUNCTION_DOMAIN of dom (the_arity_of f),(f,S,c₁₁)
Funcs (I,(Funcs ((dom (the_arity_of f)),(f,S,c₁₁)))) is non empty FUNCTION_DOMAIN of I, Funcs ((dom (the_arity_of f)),(f,S,c₁₁))
dom (doms (I,S,A,f)) is set
g is set
(commute CA) . g is Relation-like Function-like set
(doms (I,S,A,f)) . g is set
f is Element of f
(f,S,c₁₁,f) is non-empty MSAlgebra over S
the Sorts of (f,S,c₁₁,f) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
(commute CA) . f is Relation-like Function-like set
h is Relation-like Function-like set
rng (commute CA) is set
j is Relation-like Function-like set
dom j is set
rng j is set
j is Relation-like Function-like set
dom j is set
rng j is set
(the_arity_of f) * the Sorts of (f,S,c₁₁,f) is Relation-like non-empty K153() -defined Function-like set
dom ((the_arity_of f) * the Sorts of (f,S,c₁₁,f)) is set
j is set
h . j is set
((the_arity_of f) * the Sorts of (f,S,c₁₁,f)) . j is set
(the_arity_of f) . j is set
i is Element of the carrier of S
the Sorts of (f,S,c₁₁,f) . i is non empty set
CA . j is set
k is Relation-like Function-like set
dom k is set
rng k is set
(I,S,i,A) is Relation-like non-empty I -defined Function-like total set
(I,S,i,A) . f is set
dom (I,S,i,A) is set
((the_arity_of f) * (I,S,A)) . j is set
(I,S,A) . i is non empty set
product (I,S,i,A) is functional non empty with_common_domain product-like set
k . f is set
c₃₁ is MSAlgebra over S
the Sorts of c₃₁ is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of c₃₁ . i is set
(doms (I,S,A,f)) . f is set
Args (f,(f,S,c₁₁,f)) is non empty Element of rng ( the Sorts of (f,S,c₁₁,f) #)
the Sorts of (f,S,c₁₁,f) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
rng ( the Sorts of (f,S,c₁₁,f) #) is non empty V85() set
product ((the_arity_of f) * the Sorts of (f,S,c₁₁,f)) is functional non empty with_common_domain product-like set
j is Relation-like Function-like set
dom j is set
rng j is set
dom ((I,S,A,f)) is set
x is Relation-like Function-like set
dom x is set
rng x is set
rng (((I,S,A,f))) is set
x is set
dom (I,S,(the_result_sort_of f),A) is set
g is set
(((I,S,A,f))) . g is set
dom ((I,S,A,f)) is set
f is Relation-like Function-like set
commute f is Relation-like Function-like Function-yielding V25() set
uncurry f is Relation-like Function-like set
curry' (uncurry f) is Relation-like Function-like set
dom f is set
rng f is set
c₁₁ is Relation-like f -defined Function-like non empty total (f,S)
(f,S,c₁₁) is non empty set
{ (S,(f,S,c₁₁,b₁)) where b₁ is Element of f : verum } is set
union { (S,(f,S,c₁₁,b₁)) where b₁ is Element of f : verum } is set
Funcs ((dom (the_arity_of f)),(f,S,c₁₁)) is non empty FUNCTION_DOMAIN of dom (the_arity_of f),(f,S,c₁₁)
Funcs (I,(Funcs ((dom (the_arity_of f)),(f,S,c₁₁)))) is non empty FUNCTION_DOMAIN of I, Funcs ((dom (the_arity_of f)),(f,S,c₁₁))
g is Relation-like Function-like set
commute g is Relation-like Function-like Function-yielding V25() set
uncurry g is Relation-like Function-like set
curry' (uncurry g) is Relation-like Function-like set
((I,S,A,f)) . f is Relation-like Function-like set
rng ((I,S,A,f)) is set
h is Relation-like Function-like set
j is set
h . j is set
(I,S,(the_result_sort_of f),A) . j is set
i is Element of f
(f,S,c₁₁,i) is non-empty MSAlgebra over S
the Sorts of (f,S,c₁₁,i) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the ResultSort of S * the Sorts of (f,S,c₁₁,i) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
dom ( the ResultSort of S * the Sorts of (f,S,c₁₁,i)) is non empty set
(I,S,(the_result_sort_of f),A) . i is set
Result (f,(f,S,c₁₁,i)) is non empty Element of rng the Sorts of (f,S,c₁₁,i)
rng the Sorts of (f,S,c₁₁,i) is non empty V85() set
( the ResultSort of S * the Sorts of (f,S,c₁₁,i)) . f is non empty set
the Sorts of (f,S,c₁₁,i) . ( the ResultSort of S . f) is non empty set
k is MSAlgebra over S
the Sorts of k is Relation-like the carrier of S -defined Function-like non empty total set
the Sorts of k . (the_result_sort_of f) is set
dom h is set
IFEQ ((the_arity_of f),{},(commute (I,S,A,f)),(((I,S,A,f)))) is set
f is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ((I,S,A) #), the ResultSort of S * (I,S,A)
f is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ((I,S,A) #), the ResultSort of S * (I,S,A)
o is Element of the carrier' of S
f . o is Relation-like Function-like set
the_arity_of o is Relation-like K153() -defined the carrier of S -valued Function-like V33() countable V61() V62() Element of the carrier of S *
(I,S,A,o) is Relation-like I -defined Function-like total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . o is Relation-like Function-like set
commute (I,S,A,o) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A,o) is Relation-like Function-like set
curry' (uncurry (I,S,A,o)) is Relation-like Function-like set
((I,S,A,o)) is Relation-like product (doms (I,S,A,o)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,o) is Relation-like Function-like set
product (doms (I,S,A,o)) is functional with_common_domain product-like set
(((I,S,A,o))) is Relation-like Function-like set
IFEQ ((the_arity_of o),{},(commute (I,S,A,o)),(((I,S,A,o)))) is set
the Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ((I,S,A) #), the ResultSort of S * (I,S,A) is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ((I,S,A) #), the ResultSort of S * (I,S,A)
f is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ((I,S,A) #), the ResultSort of S * (I,S,A)
g is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ((I,S,A) #), the ResultSort of S * (I,S,A)
o is set
f . o is Relation-like Function-like set
g . o is Relation-like Function-like set
s is Element of the carrier' of S
f . s is Relation-like Function-like set
the_arity_of s is Relation-like K153() -defined the carrier of S -valued Function-like V33() countable V61() V62() Element of the carrier of S *
(I,S,A,s) is Relation-like I -defined Function-like total Function-yielding V25() set
(I,S,A) is Relation-like I -defined Function-like total Function-yielding V25() set
commute (I,S,A) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A) is Relation-like Function-like set
curry' (uncurry (I,S,A)) is Relation-like Function-like set
(commute (I,S,A)) . s is Relation-like Function-like set
commute (I,S,A,s) is Relation-like Function-like Function-yielding V25() set
uncurry (I,S,A,s) is Relation-like Function-like set
curry' (uncurry (I,S,A,s)) is Relation-like Function-like set
((I,S,A,s)) is Relation-like product (doms (I,S,A,s)) -defined Function-like total Function-yielding V25() set
doms (I,S,A,s) is Relation-like Function-like set
product (doms (I,S,A,s)) is functional with_common_domain product-like set
(((I,S,A,s))) is Relation-like Function-like set
IFEQ ((the_arity_of s),{},(commute (I,S,A,s)),(((I,S,A,s)))) is set
o is set
the ResultSort of S . o is set
dom the ResultSort of S is set
( the ResultSort of S * (I,S,A)) . o is set
s is Element of the carrier of S
(I,S,A) . s is non empty set
(I,S,s,A) is Relation-like non-empty I -defined Function-like total set
product (I,S,s,A) is functional non empty with_common_domain product-like set
f . o is Relation-like Function-like set
( the Arity of S * ((I,S,A) #)) . o is set
[:(( the Arity of S * ((I,S,A) #)) . o),(( the ResultSort of S * (I,S,A)) . o):] is Relation-like set
bool [:(( the Arity of S * ((I,S,A) #)) . o),(( the ResultSort of S * (I,S,A)) . o):] is set
g . o is Relation-like Function-like set
dom f is non empty set
dom g is non empty set
I is set
S is non empty non void V59() ManySortedSign
A is Relation-like I -defined Function-like total (I,S)
(I,S,A) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
(I,S,A) is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ((I,S,A) #), the ResultSort of S * (I,S,A)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S * is functional non empty V63() M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
(I,S,A) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the Arity of S * ((I,S,A) #) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (I,S,A) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (I,S,A),(I,S,A) #) is strict MSAlgebra over S
I is set
S is non empty non void V59() ManySortedSign
A is Relation-like I -defined Function-like total (I,S)
(I,S,A) is MSAlgebra over S
(I,S,A) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
the carrier of S is non empty set
(I,S,A) is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ((I,S,A) #), the ResultSort of S * (I,S,A)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S * is functional non empty V63() M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
(I,S,A) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the Arity of S * ((I,S,A) #) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (I,S,A) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (I,S,A),(I,S,A) #) is strict MSAlgebra over S
I is set
S is non empty non void V59() ManySortedSign
f is set
g is non empty non void V59() ManySortedSign
the carrier of S is non empty set
A is Relation-like I -defined Function-like total (I,S)
(I,S,A) is strict MSAlgebra over S
(I,S,A) is Relation-like non-empty non empty-yielding the carrier of S -defined Function-like non empty total set
(I,S,A) is Relation-like the carrier' of S -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of S * ((I,S,A) #), the ResultSort of S * (I,S,A)
the carrier' of S is non empty set
the Arity of S is Relation-like the carrier' of S -defined the carrier of S * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of S,( the carrier of S *):]
the carrier of S * is functional non empty V63() M8( the carrier of S)
[: the carrier' of S,( the carrier of S *):] is Relation-like set
bool [: the carrier' of S,( the carrier of S *):] is set
(I,S,A) # is Relation-like non-empty non empty-yielding the carrier of S * -defined Function-like non empty total set
the Arity of S * ((I,S,A) #) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
the ResultSort of S is Relation-like the carrier' of S -defined the carrier of S -valued Function-like quasi_total Element of bool [: the carrier' of S, the carrier of S:]
[: the carrier' of S, the carrier of S:] is Relation-like set
bool [: the carrier' of S, the carrier of S:] is set
the ResultSort of S * (I,S,A) is Relation-like non-empty non empty-yielding the carrier' of S -defined Function-like non empty total set
MSAlgebra(# (I,S,A),(I,S,A) #) is strict MSAlgebra over S
the Sorts of (I,S,A) is Relation-like the carrier of S -defined Function-like non empty total set
the carrier' of g is non empty set
o is Relation-like f -defined Function-like total (f,g)
(f,g,o) is strict MSAlgebra over g
(f,g,o) is Relation-like non-empty non empty-yielding the carrier of g -defined Function-like non empty total set
the carrier of g is non empty set
(f,g,o) is Relation-like the carrier' of g -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of g * ((f,g,o) #), the ResultSort of g * (f,g,o)
the Arity of g is Relation-like the carrier' of g -defined the carrier of g * -valued Function-like quasi_total Function-yielding V25() Element of bool [: the carrier' of g,( the carrier of g *):]
the carrier of g * is functional non empty V63() M8( the carrier of g)
[: the carrier' of g,( the carrier of g *):] is Relation-like set
bool [: the carrier' of g,( the carrier of g *):] is set
(f,g,o) # is Relation-like non-empty non empty-yielding the carrier of g * -defined Function-like non empty total set
the Arity of g * ((f,g,o) #) is Relation-like non-empty non empty-yielding the carrier' of g -defined Function-like non empty total set
the ResultSort of g is Relation-like the carrier' of g -defined the carrier of g -valued Function-like quasi_total Element of bool [: the carrier' of g, the carrier of g:]
[: the carrier' of g, the carrier of g:] is Relation-like set
bool [: the carrier' of g, the carrier of g:] is set
the ResultSort of g * (f,g,o) is Relation-like non-empty non empty-yielding the carrier' of g -defined Function-like non empty total set
MSAlgebra(# (f,g,o),(f,g,o) #) is strict MSAlgebra over g
the Charact of (f,g,o) is Relation-like the carrier' of g -defined Function-like non empty total Function-yielding V25() ManySortedFunction of the Arity of g * ( the Sorts of (f,g,o) #), the ResultSort of g * the Sorts of (f,g,o)
the Sorts of (f,g,o) is Relation-like the carrier of g -defined Function-like non empty total set
the Sorts of (f,g,o) # is Relation-like the carrier of g * -defined Function-like non empty total set
the Arity of g * ( the Sorts of (f,g,o) #) is Relation-like the carrier' of g -defined Function-like non empty total set
the ResultSort of g * the Sorts of (f,g,o) is Relation-like the carrier' of g -defined Function-like non empty total set