:: ALG_1 semantic presentation

NAT is non empty V35() V36() V37() V42() V47() V48() Element of K10(REAL)

REAL is set

K10(REAL) is set

NAT is non empty V35() V36() V37() V42() V47() V48() set

K10(NAT) is V42() set

K10(NAT) is V42() set

K219() is non empty set

K133() is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of NAT

{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set

the empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set

1 is non empty set

{K133(),1} is non empty set

2 is non empty set

3 is non empty set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

K10( the carrier of U1) is set

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

U2 is non empty Element of K10( the carrier of U1)

Opers (U1,U2) is Relation-like NAT -defined PFuncs ((U2 *),U2) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((U2 *),U2)

U2 * is non empty functional FinSequence-membered FinSequenceSet of U2

PFuncs ((U2 *),U2) is non empty functional set

dom (Opers (U1,U2)) is Element of K10(NAT)

dom the charact of U1 is non empty Element of K10(NAT)

f is V35() V36() V37() V41() V42() V47() set

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

the charact of U1 . f is Relation-like Function-like homogeneous set

(Opers (U1,U2)) . f is Relation-like Function-like set

c

c

K11((U2 *),U2) is Relation-like set

K10(K11((U2 *),U2)) is set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

<*> the carrier of U1 is empty Relation-like non-empty empty-yielding NAT -defined the carrier of U1 -valued Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of the carrier of U1

f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))

f * (<*> the carrier of U1) is empty Relation-like non-empty empty-yielding NAT -defined the carrier of U2 -valued Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of the carrier of U2

<*> the carrier of U2 is empty Relation-like non-empty empty-yielding NAT -defined the carrier of U2 -valued Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of the carrier of U2

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))

K11( the carrier of U1, the carrier of U1) is Relation-like set

K10(K11( the carrier of U1, the carrier of U1)) is set

U2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

(id the carrier of U1) * U2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

dom ((id the carrier of U1) * U2) is Element of K10(NAT)

dom U2 is Element of K10(NAT)

c

U2 . c

u1 is Element of the carrier of U1

(id the carrier of U1) . u1 is Element of the carrier of U1

((id the carrier of U1) * U2) . c

len ((id the carrier of U1) * U2) is V35() V36() V37() V41() V42() V47() Element of NAT

len U2 is V35() V36() V37() V41() V42() V47() Element of NAT

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

f is non empty V91() quasi_total non-empty UAStr

the carrier of f is non empty set

K11( the carrier of U2, the carrier of f) is Relation-like set

K10(K11( the carrier of U2, the carrier of f)) is set

c

u1 is non empty Relation-like the carrier of U2 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of f))

u1 * c

K11( the carrier of U1, the carrier of f) is Relation-like set

K10(K11( the carrier of U1, the carrier of f)) is set

u2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

c

u1 * (c

(u1 * c

dom u2 is Element of K10(NAT)

len u2 is V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len u2) is V42() V49( len u2) Element of K10(NAT)

dom (u1 * (c

dom (c

len ((u1 * c

dom ((u1 * c

F is V35() V36() V37() V41() V42() V47() set

(u1 * (c

(c

u1 . ((c

u2 . F is set

c

u1 . (c

(u1 * c

((u1 * c

len (u1 * (c

len (c

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))

K11( the carrier of U1, the carrier of U1) is Relation-like set

K10(K11( the carrier of U1, the carrier of U1)) is set

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

dom the charact of U1 is non empty Element of K10(NAT)

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

U2 is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U1 . U2 is Relation-like Function-like homogeneous set

f is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

c

dom f is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))

K10(( the carrier of U1 *)) is set

u2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

f . u2 is set

(id the carrier of U1) . (f . u2) is set

(id the carrier of U1) * u2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

c

rng f is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

F is Element of the carrier of U1

(id the carrier of U1) . F is Element of the carrier of U1

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

f is non empty V91() quasi_total non-empty UAStr

the carrier of f is non empty set

K11( the carrier of U2, the carrier of f) is Relation-like set

K10(K11( the carrier of U2, the carrier of f)) is set

c

u1 is non empty Relation-like the carrier of U2 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of f))

u1 * c

K11( the carrier of U1, the carrier of f) is Relation-like set

K10(K11( the carrier of U1, the carrier of f)) is set

signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

signature U2 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

signature f is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

dom the charact of U1 is non empty Element of K10(NAT)

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

the carrier of f * is non empty functional FinSequence-membered FinSequenceSet of the carrier of f

Operations f is non empty PFuncsDomHQN of the carrier of f

the charact of f is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of f *), the carrier of f) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of f *), the carrier of f)

PFuncs (( the carrier of f *), the carrier of f) is non empty functional set

rng the charact of f is non empty V4() set

y is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U1 . y is Relation-like Function-like homogeneous set

the charact of f . y is Relation-like Function-like homogeneous set

y is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

dom y is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))

K10(( the carrier of U1 *)) is set

u is non empty Relation-like the carrier of f * -defined the carrier of f -valued Function-like homogeneous quasi_total Element of Operations f

a is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

y . a is set

(u1 * c

(u1 * c

u . ((u1 * c

the carrier of U2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2

c

rng y is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

arity y is V35() V36() V37() V41() V42() V47() Element of NAT

(arity y) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

{ b

len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT

len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)

len (signature U2) is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U2 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U2 *), the carrier of U2) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U2 *), the carrier of U2)

PFuncs (( the carrier of U2 *), the carrier of U2) is non empty functional set

len the charact of U2 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

dom the charact of U2 is non empty Element of K10(NAT)

Seg (len the charact of U2) is non empty V42() V49( len the charact of U2) Element of K10(NAT)

Operations U2 is non empty PFuncsDomHQN of the carrier of U2

rng the charact of U2 is non empty V4() set

the charact of U2 . y is Relation-like Function-like homogeneous set

dom (signature U1) is Element of K10(NAT)

Seg (len (signature U1)) is V42() V49( len (signature U1)) Element of K10(NAT)

(signature U2) . y is set

b is non empty Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like homogeneous quasi_total Element of Operations U2

arity b is V35() V36() V37() V41() V42() V47() Element of NAT

(signature U1) . y is set

len (c

b is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *

len b is V35() V36() V37() V41() V42() V47() Element of NAT

dom b is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U2 *))

K10(( the carrier of U2 *)) is set

(arity b) -tuples_on the carrier of U2 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2

a is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U2 *

{ b

b . (c

u1 . (b . (c

u1 * (c

u . (u1 * (c

c

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))

rng f is non empty Element of K10( the carrier of U2)

K10( the carrier of U2) is set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))

dom f is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

rng f is non empty Element of K10( the carrier of U2)

K10( the carrier of U2) is set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

K11( the carrier of U2, the carrier of U1) is Relation-like set

K10(K11( the carrier of U2, the carrier of U1)) is set

f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))

f " is Relation-like Function-like set

c

signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

signature U2 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

dom the charact of U1 is non empty Element of K10(NAT)

Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)

dom (signature U2) is Element of K10(NAT)

len (signature U2) is V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len (signature U2)) is V42() V49( len (signature U2)) Element of K10(NAT)

the charact of U2 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U2 *), the carrier of U2) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U2 *), the carrier of U2)

the carrier of U2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2

PFuncs (( the carrier of U2 *), the carrier of U2) is non empty functional set

len the charact of U2 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

dom the charact of U2 is non empty Element of K10(NAT)

Seg (len the charact of U2) is non empty V42() V49( len the charact of U2) Element of K10(NAT)

rng f is non empty Element of K10( the carrier of U2)

K10( the carrier of U2) is set

u1 is V35() V36() V37() V41() V42() V47() Element of NAT

Operations U2 is non empty PFuncsDomHQN of the carrier of U2

rng the charact of U2 is non empty V4() set

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

u2 is non empty Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like homogeneous quasi_total Element of Operations U2

the charact of U2 . u1 is Relation-like Function-like homogeneous set

F is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

the charact of U1 . u1 is Relation-like Function-like homogeneous set

x is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2

dom x is Element of K10(NAT)

len x is V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len x) is V42() V49( len x) Element of K10(NAT)

y is V35() V36() V37() V41() V42() V47() set

x . y is set

dom f is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

y is set

f . y is set

u is Element of the carrier of U1

f . u is set

y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

dom y is Element of K10(NAT)

f * y is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2

dom (f * y) is Element of K10(NAT)

y is V35() V36() V37() V41() V42() V47() set

x . y is set

y . y is set

f . (y . y) is set

(f * y) . y is set

len y is V35() V36() V37() V41() V42() V47() Element of NAT

dom u2 is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U2 *))

K10(( the carrier of U2 *)) is set

arity u2 is V35() V36() V37() V41() V42() V47() Element of NAT

(arity u2) -tuples_on the carrier of U2 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2

{ b

c

K11( the carrier of U1, the carrier of U1) is Relation-like set

K10(K11( the carrier of U1, the carrier of U1)) is set

dom f is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

id (dom f) is non empty Relation-like dom f -defined dom f -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11((dom f),(dom f)))

K11((dom f),(dom f)) is Relation-like set

K10(K11((dom f),(dom f))) is set

id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))

c

(id the carrier of U1) * y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

(signature U1) . u1 is set

arity F is V35() V36() V37() V41() V42() V47() Element of NAT

(signature U2) . u1 is set

y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *

{ b

u is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U2 *

len u is V35() V36() V37() V41() V42() V47() Element of NAT

(arity F) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

dom F is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))

K10(( the carrier of U1 *)) is set

u2 . x is set

c

F . y is set

f . (F . y) is set

c

(id the carrier of U1) . (F . y) is set

F . (c

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

K11( the carrier of U2, the carrier of U1) is Relation-like set

K10(K11( the carrier of U2, the carrier of U1)) is set

f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))

f " is Relation-like Function-like set

c

rng c

K10( the carrier of U1) is set

dom f is non empty Element of K10( the carrier of U1)

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

f is non empty V91() quasi_total non-empty UAStr

the carrier of f is non empty set

K11( the carrier of U2, the carrier of f) is Relation-like set

K10(K11( the carrier of U2, the carrier of f)) is set

c

u1 is non empty Relation-like the carrier of U2 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of f))

u1 * c

K11( the carrier of U1, the carrier of f) is Relation-like set

K10(K11( the carrier of U1, the carrier of f)) is set

dom u1 is non empty Element of K10( the carrier of U2)

K10( the carrier of U2) is set

rng c

rng (u1 * c

K10( the carrier of f) is set

rng u1 is non empty Element of K10( the carrier of f)

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))

K11( the carrier of U1, the carrier of U1) is Relation-like set

K10(K11( the carrier of U1, the carrier of U1)) is set

rng (id the carrier of U1) is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

U1 is non empty V91() quasi_total non-empty UAStr

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))

f " is Relation-like Function-like set

rng (f ") is set

dom f is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

dom (f ") is set

rng f is non empty Element of K10( the carrier of U2)

K10( the carrier of U2) is set

K11( the carrier of U2, the carrier of U1) is Relation-like set

K10(K11( the carrier of U2, the carrier of U1)) is set

c

U1 is non empty V91() quasi_total non-empty UAStr

U2 is non empty V91() quasi_total non-empty UAStr

f is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

c

the carrier of f is non empty set

K11( the carrier of U2, the carrier of f) is Relation-like set

K10(K11( the carrier of U2, the carrier of f)) is set

u1 is non empty Relation-like the carrier of U2 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of f))

u1 * c

K11( the carrier of U1, the carrier of f) is Relation-like set

K10(K11( the carrier of U1, the carrier of f)) is set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))

f .: the carrier of U1 is Element of K10( the carrier of U2)

K10( the carrier of U2) is set

dom f is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

c

UniAlgSetClosed c

u1 is non empty strict V91() quasi_total non-empty SubAlgebra of U2

the carrier of u1 is non empty set

the carrier of U2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2

Operations U2 is non empty PFuncsDomHQN of the carrier of U2

the charact of U2 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U2 *), the carrier of U2) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U2 *), the carrier of U2)

PFuncs (( the carrier of U2 *), the carrier of U2) is non empty functional set

rng the charact of U2 is non empty V4() set

u2 is non empty Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like homogeneous quasi_total Element of Operations U2

dom the charact of U2 is non empty Element of K10(NAT)

F is V35() V36() V37() V41() V42() V47() set

the charact of U2 . F is Relation-like Function-like homogeneous set

x is Relation-like NAT -defined c

len x is V35() V36() V37() V41() V42() V47() Element of NAT

arity u2 is V35() V36() V37() V41() V42() V47() Element of NAT

u2 . x is set

dom x is Element of K10(NAT)

y is set

x . y is set

y is V35() V36() V37() V41() V42() V47() Element of NAT

x . y is set

u is set

f . u is set

y is Relation-like Function-like set

dom y is set

rng y is set

Seg (len x) is V42() V49( len x) Element of K10(NAT)

y is Relation-like NAT -defined Function-like V42() FinSequence-like FinSubsequence-like set

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

u is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

a is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *

len a is V35() V36() V37() V41() V42() V47() Element of NAT

signature U2 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U2) is Element of K10(NAT)

len (signature U2) is V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len (signature U2)) is V42() V49( len (signature U2)) Element of K10(NAT)

signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

dom (signature U1) is Element of K10(NAT)

len the charact of U2 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len the charact of U2) is non empty V42() V49( len the charact of U2) Element of K10(NAT)

(signature U2) . F is set

f * a is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2

len (f * a) is V35() V36() V37() V41() V42() V47() Element of NAT

dom (f * a) is Element of K10(NAT)

Seg (len (f * a)) is V42() V49( len (f * a)) Element of K10(NAT)

Seg (len a) is V42() V49( len a) Element of K10(NAT)

a is V35() V36() V37() V41() V42() V47() set

a . a is set

f . (a . a) is set

x . a is set

(f * a) . a is set

len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len (signature U1)) is V42() V49( len (signature U1)) Element of K10(NAT)

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

dom the charact of U1 is non empty Element of K10(NAT)

Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

the charact of U1 . F is Relation-like Function-like homogeneous set

(signature U1) . F is set

a is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

arity a is V35() V36() V37() V41() V42() V47() Element of NAT

{ b

(arity a) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

dom a is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))

K10(( the carrier of U1 *)) is set

a . a is set

rng a is non empty Element of K10( the carrier of U1)

f . (a . a) is set

u2 . (f * a) is set

Opers (U2,c

c

PFuncs ((c

UAStr(# c

c

the carrier of c

u1 is non empty strict V91() quasi_total non-empty SubAlgebra of U2

the carrier of u1 is non empty set

the charact of c

the carrier of c

PFuncs (( the carrier of c

u2 is non empty Element of K10( the carrier of U2)

Opers (U2,u2) is Relation-like NAT -defined PFuncs ((u2 *),u2) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((u2 *),u2)

u2 * is non empty functional FinSequence-membered FinSequenceSet of u2

PFuncs ((u2 *),u2) is non empty functional set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))

rng f is non empty Element of K10( the carrier of U2)

K10( the carrier of U2) is set

(U1,U2,f) is non empty strict V91() quasi_total non-empty SubAlgebra of U2

the carrier of (U1,U2,f) is non empty set

dom f is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

f .: the carrier of U1 is Element of K10( the carrier of U2)

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is non empty strict V91() quasi_total non-empty UAStr

the carrier of U2 is non empty set

K11( the carrier of U1, the carrier of U2) is Relation-like set

K10(K11( the carrier of U1, the carrier of U2)) is set

f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))

(U1,U2,f) is non empty strict V91() quasi_total non-empty SubAlgebra of U2

K10( the carrier of U2) is set

the carrier of (U1,U2,f) is non empty set

rng f is non empty Element of K10( the carrier of U2)

dom f is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

f .: (dom f) is Element of K10( the carrier of U2)

f .: the carrier of U1 is Element of K10( the carrier of U2)

the charact of (U1,U2,f) is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of (U1,U2,f) *), the carrier of (U1,U2,f)) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (U1,U2,f) *), the carrier of (U1,U2,f))

the carrier of (U1,U2,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (U1,U2,f)

PFuncs (( the carrier of (U1,U2,f) *), the carrier of (U1,U2,f)) is non empty functional set

c

Opers (U2,c

c

PFuncs ((c

f .: the carrier of U1 is Element of K10( the carrier of U2)

K10( the carrier of U2) is set

dom f is non empty Element of K10( the carrier of U1)

K10( the carrier of U1) is set

f .: (dom f) is Element of K10( the carrier of U2)

rng f is non empty Element of K10( the carrier of U2)

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

K11( the carrier of U1, the carrier of U1) is Relation-like set

K10(K11( the carrier of U1, the carrier of U1)) is set

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

rng the charact of U1 is non empty V4() set

dom the charact of U1 is non empty Element of K10(NAT)

id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))

U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total Element of K10(K11( the carrier of U1, the carrier of U1))

ExtendRel U2 is Relation-like the carrier of U1 * -defined the carrier of U1 * -valued Element of K10(K11(( the carrier of U1 *),( the carrier of U1 *)))

K11(( the carrier of U1 *),( the carrier of U1 *)) is Relation-like set

K10(K11(( the carrier of U1 *),( the carrier of U1 *))) is set

f is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U1 . f is Relation-like Function-like homogeneous set

c

dom c

K10(( the carrier of U1 *)) is set

u1 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

u2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

[u1,u2] is set

{u1,u2} is non empty functional set

{u1} is non empty V2() functional V49(1) set

{{u1,u2},{u1}} is non empty set

c

c

[(c

{(c

{(c

{{(c

id ( the carrier of U1 *) is non empty Relation-like the carrier of U1 * -defined the carrier of U1 * -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11(( the carrier of U1 *),( the carrier of U1 *)))

rng c

K10( the carrier of U1) is set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

rng the charact of U1 is non empty V4() set

U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)

Class U2 is non empty V4() a_partition of the carrier of U1

(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2

K11(((Class U2) *),(Class U2)) is Relation-like set

K10(K11(((Class U2) *),(Class U2))) is set

f is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

arity f is V35() V36() V37() V41() V42() V47() Element of NAT

(arity f) -tuples_on (Class U2) is non empty functional FinSequence-membered FinSequenceSet of Class U2

u1 is set

dom f is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))

K10(( the carrier of U1 *)) is set

(arity f) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

{ b

{ b

u2 is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *

len u2 is V35() V36() V37() V41() V42() V47() Element of NAT

F is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

K10( the carrier of U1) is set

f . F is set

Class (U2,(f . F)) is Element of K10( the carrier of U1)

x is Element of K10( the carrier of U1)

len F is V35() V36() V37() V41() V42() V47() Element of NAT

rng f is non empty Element of K10( the carrier of U1)

y is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2

y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

f . y is set

Class (U2,(f . y)) is Element of K10( the carrier of U1)

len y is V35() V36() V37() V41() V42() V47() Element of NAT

dom F is Element of K10(NAT)

u is V35() V36() V37() V41() V42() V47() Element of NAT

F . u is set

y . u is set

[(F . u),(y . u)] is set

{(F . u),(y . u)} is non empty set

{(F . u)} is non empty V2() V49(1) set

{{(F . u),(y . u)},{(F . u)}} is non empty set

Class (U2,(F . u)) is Element of K10( the carrier of U1)

u2 . u is set

rng F is Element of K10( the carrier of U1)

Seg (arity f) is V42() V49( arity f) Element of K10(NAT)

dom y is Element of K10(NAT)

Class (U2,(y . u)) is Element of K10( the carrier of U1)

[F,y] is set

{F,y} is non empty functional set

{F} is non empty V2() functional V49(1) set

{{F,y},{F}} is non empty set

ExtendRel U2 is Relation-like the carrier of U1 * -defined the carrier of U1 * -valued Element of K10(K11(( the carrier of U1 *),( the carrier of U1 *)))

K11(( the carrier of U1 *),( the carrier of U1 *)) is Relation-like set

K10(K11(( the carrier of U1 *),( the carrier of U1 *))) is set

dom the charact of U1 is non empty Element of K10(NAT)

[(f . F),(f . y)] is set

{(f . F),(f . y)} is non empty set

{(f . F)} is non empty V2() V49(1) set

{{(f . F),(f . y)},{(f . F)}} is non empty set

u is V35() V36() V37() V41() V42() V47() set

the charact of U1 . u is Relation-like Function-like homogeneous set

u1 is Relation-like Function-like set

dom u1 is set

rng u1 is set

{ (b

union { (b

u2 is Relation-like (Class U2) * -defined Class U2 -valued Function-like Element of K10(K11(((Class U2) *),(Class U2)))

dom u2 is functional FinSequence-membered Element of K10(((Class U2) *))

K10(((Class U2) *)) is set

{ b

F is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2

len F is V35() V36() V37() V41() V42() V47() Element of NAT

x is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2

len x is V35() V36() V37() V41() V42() V47() Element of NAT

y is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *

len y is V35() V36() V37() V41() V42() V47() Element of NAT

the Relation-like NAT -defined Class U2 -valued Function-like V42() V49( arity f) FinSequence-like FinSubsequence-like Element of (arity f) -tuples_on (Class U2) is Relation-like NAT -defined Class U2 -valued Function-like V42() V49( arity f) FinSequence-like FinSubsequence-like Element of (arity f) -tuples_on (Class U2)

F is Relation-like NAT -defined Function-like V42() FinSequence-like FinSubsequence-like set

x is Relation-like NAT -defined Function-like V42() FinSequence-like FinSubsequence-like set

len F is V35() V36() V37() V41() V42() V47() Element of NAT

len x is V35() V36() V37() V41() V42() V47() Element of NAT

y is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *

len y is V35() V36() V37() V41() V42() V47() Element of NAT

y is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *

len y is V35() V36() V37() V41() V42() V47() Element of NAT

x is Relation-like NAT -defined Function-like V42() FinSequence-like FinSubsequence-like set

F is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

dom F is non empty functional FinSequence-membered with_common_domain Element of K10(((Class U2) *))

x is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2

F . x is set

y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

f . y is set

Class (U2,(f . y)) is Element of K10( the carrier of U1)

K10( the carrier of U1) is set

c

dom c

K10(((Class U2) *)) is set

u1 is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

dom u1 is non empty functional FinSequence-membered with_common_domain Element of K10(((Class U2) *))

u2 is set

c

u1 . u2 is set

F is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2

x is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

c

f . x is set

Class (U2,(f . x)) is Element of K10( the carrier of U1)

K10( the carrier of U1) is set

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)

Class U2 is non empty V4() a_partition of the carrier of U1

(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2

PFuncs (((Class U2) *),(Class U2)) is non empty functional set

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)

f is V35() V36() V37() V41() V42() V47() set

the charact of U1 . f is Relation-like Function-like homogeneous set

dom the charact of U1 is non empty Element of K10(NAT)

c

(U1,U2,c

K11(((Class U2) *),(Class U2)) is Relation-like set

K10(K11(((Class U2) *),(Class U2))) is set

u1 is Relation-like Function-like Element of PFuncs (((Class U2) *),(Class U2))

u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

f is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))

dom f is Element of K10(NAT)

c

len c

dom c

u1 is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U1 . u1 is Relation-like Function-like homogeneous set

c

u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

K11(((Class U2) *),(Class U2)) is Relation-like set

K10(K11(((Class U2) *),(Class U2))) is set

f is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))

len f is V35() V36() V37() V41() V42() V47() Element of NAT

dom f is Element of K10(NAT)

c

len c

dom c

u1 is V35() V36() V37() V41() V42() V47() set

Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)

dom the charact of U1 is non empty Element of K10(NAT)

the charact of U1 . u1 is Relation-like Function-like homogeneous set

f . u1 is Relation-like Function-like set

u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

K11(((Class U2) *),(Class U2)) is Relation-like set

K10(K11(((Class U2) *),(Class U2))) is set

c

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)

Class U2 is non empty V4() a_partition of the carrier of U1

(U1,U2) is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))

(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2

PFuncs (((Class U2) *),(Class U2)) is non empty functional set

UAStr(# (Class U2),(U1,U2) #) is non empty strict UAStr

K11(((Class U2) *),(Class U2)) is Relation-like set

K10(K11(((Class U2) *),(Class U2))) is set

dom (U1,U2) is Element of K10(NAT)

c

(U1,U2) . c

u1 is Relation-like (Class U2) * -defined Class U2 -valued Function-like Element of K10(K11(((Class U2) *),(Class U2)))

len (U1,U2) is V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len (U1,U2)) is V42() V49( len (U1,U2)) Element of K10(NAT)

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)

dom the charact of U1 is non empty Element of K10(NAT)

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

the charact of U1 . c

u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

the carrier of UAStr(# (Class U2),(U1,U2) #) is non empty set

the charact of UAStr(# (Class U2),(U1,U2) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# (Class U2),(U1,U2) #) *), the carrier of UAStr(# (Class U2),(U1,U2) #)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# (Class U2),(U1,U2) #) *), the carrier of UAStr(# (Class U2),(U1,U2) #))

the carrier of UAStr(# (Class U2),(U1,U2) #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# (Class U2),(U1,U2) #)

PFuncs (( the carrier of UAStr(# (Class U2),(U1,U2) #) *), the carrier of UAStr(# (Class U2),(U1,U2) #)) is non empty functional set

c

(U1,U2) . c

u1 is Relation-like (Class U2) * -defined Class U2 -valued Function-like Element of K10(K11(((Class U2) *),(Class U2)))

len (U1,U2) is V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len (U1,U2)) is V42() V49( len (U1,U2)) Element of K10(NAT)

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)

dom the charact of U1 is non empty Element of K10(NAT)

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

the charact of U1 . c

u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

c

(U1,U2) . c

len (U1,U2) is V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len (U1,U2)) is V42() V49( len (U1,U2)) Element of K10(NAT)

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)

dom the charact of U1 is non empty Element of K10(NAT)

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

u1 is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U1 . u1 is Relation-like Function-like homogeneous set

(U1,U2) . u1 is Relation-like Function-like set

u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

len the charact of UAStr(# (Class U2),(U1,U2) #) is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)

(U1,U2) is non empty strict V91() quasi_total non-empty UAStr

Class U2 is non empty V4() a_partition of the carrier of U1

(U1,U2) is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))

(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2

PFuncs (((Class U2) *),(Class U2)) is non empty functional set

UAStr(# (Class U2),(U1,U2) #) is non empty strict UAStr

the carrier of (U1,U2) is non empty set

K11( the carrier of U1, the carrier of (U1,U2)) is Relation-like set

K10(K11( the carrier of U1, the carrier of (U1,U2))) is set

f is Element of the carrier of U1

Class (U2,f) is Element of K10( the carrier of U1)

K10( the carrier of U1) is set

c

f is non empty Relation-like the carrier of U1 -defined the carrier of (U1,U2) -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of (U1,U2)))

c

f . c

Class (U2,c

K10( the carrier of U1) is set

f is non empty Relation-like the carrier of U1 -defined the carrier of (U1,U2) -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of (U1,U2)))

c

u1 is Element of the carrier of U1

f . u1 is Element of the carrier of (U1,U2)

Class (U2,u1) is Element of K10( the carrier of U1)

K10( the carrier of U1) is set

c

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)

(U1,U2) is non empty strict V91() quasi_total non-empty UAStr

Class U2 is non empty V4() a_partition of the carrier of U1

(U1,U2) is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))

(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2

PFuncs (((Class U2) *),(Class U2)) is non empty functional set

UAStr(# (Class U2),(U1,U2) #) is non empty strict UAStr

(U1,U2) is non empty Relation-like the carrier of U1 -defined the carrier of (U1,U2) -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of (U1,U2)))

the carrier of (U1,U2) is non empty set

K11( the carrier of U1, the carrier of (U1,U2)) is Relation-like set

K10(K11( the carrier of U1, the carrier of (U1,U2))) is set

signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)

the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set

len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT

dom (signature U1) is Element of K10(NAT)

Seg (len (signature U1)) is V42() V49( len (signature U1)) Element of K10(NAT)

len (U1,U2) is V35() V36() V37() V41() V42() V47() Element of NAT

signature (U1,U2) is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT

len (signature (U1,U2)) is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of (U1,U2) is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of (U1,U2) *), the carrier of (U1,U2)) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (U1,U2) *), the carrier of (U1,U2))

the carrier of (U1,U2) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (U1,U2)

PFuncs (( the carrier of (U1,U2) *), the carrier of (U1,U2)) is non empty functional set

len the charact of (U1,U2) is non empty V35() V36() V37() V41() V42() V47() Element of NAT

u2 is V35() V36() V37() V41() V42() V47() set

dom the charact of U1 is non empty Element of K10(NAT)

Operations U1 is non empty PFuncsDomHQN of the carrier of U1

rng the charact of U1 is non empty V4() set

the charact of U1 . u2 is Relation-like Function-like homogeneous set

dom (U1,U2) is Element of K10(NAT)

(U1,U2) . u2 is Relation-like Function-like set

F is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

(U1,U2,F) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

K11(((Class U2) *),(Class U2)) is Relation-like set

K10(K11(((Class U2) *),(Class U2))) is set

K11(( the carrier of (U1,U2) *), the carrier of (U1,U2)) is Relation-like set

K10(K11(( the carrier of (U1,U2) *), the carrier of (U1,U2))) is set

x is non empty Relation-like the carrier of (U1,U2) * -defined the carrier of (U1,U2) -valued Function-like homogeneous quasi_total Element of K10(K11(( the carrier of (U1,U2) *), the carrier of (U1,U2)))

dom x is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of (U1,U2) *))

K10(( the carrier of (U1,U2) *)) is set

y is set

dom (U1,U2,F) is non empty functional FinSequence-membered with_common_domain Element of K10(((Class U2) *))

K10(((Class U2) *)) is set

arity F is V35() V36() V37() V41() V42() V47() Element of NAT

(arity F) -tuples_on (Class U2) is non empty functional FinSequence-membered FinSequenceSet of Class U2

y is Relation-like NAT -defined the carrier of (U1,U2) -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of (U1,U2) *

{ b

arity x is V35() V36() V37() V41() V42() V47() Element of NAT

u is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *

len u is V35() V36() V37() V41() V42() V47() Element of NAT

dom (signature (U1,U2)) is Element of K10(NAT)

(signature U1) . u2 is set

(signature (U1,U2)) . u2 is set

Operations (U1,U2) is non empty PFuncsDomHQN of the carrier of (U1,U2)

rng the charact of (U1,U2) is non empty V4() set

u2 is V35() V36() V37() V41() V42() V47() Element of NAT

the charact of U1 . u2 is Relation-like Function-like homogeneous set

the charact of (U1,U2) . u2 is Relation-like Function-like homogeneous set

Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)

F is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1

dom F is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))

K10(( the carrier of U1 *)) is set

x is non empty Relation-like the carrier of (U1,U2) * -defined the carrier of (U1,U2) -valued Function-like homogeneous quasi_total Element of Operations (U1,U2)

(U1,U2,F) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))

y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1

F . y is set

(U1,U2) . (F . y) is set

(U1,U2) * y is Relation-like NAT -defined the carrier of (U1,U2) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of (U1,U2)

x . ((U1,U2) * y) is set

u is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2

len ((U1,U2) * y) is V35() V36() V37() V41() V42() V47() Element of NAT

len y is V35() V36() V37() V41() V42() V47() Element of NAT

a is V35() V36() V37() V41() V42() V47() Element of NAT

dom y is Element of K10(NAT)

dom ((U1,U2) * y) is Element of K10(NAT)

y . a is set

rng y is Element of K10( the carrier of U1)

K10( the carrier of U1) is set

Class (U2,(y . a)) is Element of K10( the carrier of U1)

b is Element of the carrier of U1

(U1,U2) . b is Element of the carrier of (U1,U2)

a is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *

a . a is set

rng F is non empty Element of K10( the carrier of U1)

arity F is V35() V36() V37() V41() V42() V47() Element of NAT

(arity F) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1

{ b

y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *

a is Element of the carrier of U1

Class (U2,a) is Element of K10( the carrier of U1)

Class (U2,(F . y)) is Element of K10( the carrier of U1)

dom (U1,U2,F) is non empty functional FinSequence-membered with_common_domain Element of K10(((Class U2) *))

(arity F) -tuples_on (Class U2) is non empty functional FinSequence-membered FinSequenceSet of Class U2

{ b

b is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *

len b is V35() V36() V37() V41() V42() V47() Element of NAT

U1 is non empty V91() quasi_total non-empty UAStr

the carrier of U1 is non empty set

U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)