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

dom c

dom [|S,A|] is non empty set

dom f is set

pr1 c

dom (pr1 c

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 * S) . f is set

(f * [|S,A|]) . f is set

f . f is set

[|S,A|] . (f . f) is set

c

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

product (f * S) is functional non empty with_common_domain product-like set

dom o is set

o . (pr1 c

rng o is set

pr2 c

s . (pr2 c

[(o . (pr1 c

{(o . (pr1 c

{(o . (pr1 c

{{(o . (pr1 c

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

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 * A) . f is set

(f * [|S,A|]) . f is set

f . f is set

[|S,A|] . (f . f) is set

c

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

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

f . c

pr1 c

o . (pr1 c

pr2 c

s . (pr2 c

[(o . (pr1 c

{(o . (pr1 c

{(o . (pr1 c

{{(o . (pr1 c

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

dom c

f . c

pr1 c

o . (pr1 c

pr2 c

s . (pr2 c

[(o . (pr1 c

{(o . (pr1 c

{(o . (pr1 c

{{(o . (pr1 c

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

A . c

[:((A #) . f),(A . c

bool [:((A #) . f),(A . c

(f #) . (g . f) is set

(g * (f #)) . f is set

(f #) . f is non empty set

f . c

[:((f #) . f),(f . c

bool [:((f #) . f),(f . c

f is Relation-like (A #) . f -defined A . c

f is Relation-like (f #) . f -defined f . c

(I,A,f,f,c

([|A,f|] #) . f is non empty set

[|A,f|] . c

[:(([|A,f|] #) . f),([|A,f|] . c

bool [:(([|A,f|] #) . f),([|A,f|] . c

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

f . c

g . c

o . c

dom o is set

A . (o . c

(o * A) . c

f . (o . c

(o * f) . c

dom g is set

(A #) . (g . c

(g * (A #)) . c

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

(f #) . (g . c

(g * (f #)) . c

(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

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

f is set

c

(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

f . c

f . c

g . c

o . c

dom o is set

A . (o . c

(o * A) . c

f . (o . c

(o * f) . c

dom g is set

(A #) . (g . c

(g * (A #)) . c

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

(f #) . (g . c

(g * (f #)) . c

(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

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

union { (S,(I,S,A,b

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

union { (S,(I,S,A,b

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

(g,S,o,c

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

(g,S,o,c

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

the Charact 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

the Sorts of c

the Arity of S * ( the Sorts of c

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

f . f is set

(uncurry (I,S,A)) . (f,f) is set

(uncurry (I,S,A)) . [f,f] is set

the Charact of c

Den (f,c

Args (f,c

rng ( the Sorts of c

Result (f,c

rng the Sorts of c

[:(Args (f,c

bool [:(Args (f,c

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

union { (S,(I,S,A,b

f is Element of the carrier' of S

(I,S,A,f) is