:: UNIALG_1 semantic presentation

REAL is set

NAT is non empty V26() V27() V28() V33() V38() V39() V62() V63() Element of K19(REAL)

K19(REAL) is set

NAT is non empty V26() V27() V28() V33() V38() V39() V62() V63() set

K19(NAT) is V33() set

K19(NAT) is V33() set

K187() is non empty set

K116() is Function-like functional empty ext-real non positive non negative V26() V27() V28() V30() V31() V32() V33() V38() V40( {} ) FinSequence-membered V60() V62() Element of NAT

{} is Function-like functional empty ext-real non positive non negative V26() V27() V28() V30() V31() V32() V33() V38() V40( {} ) FinSequence-membered V60() V62() set

1 is non empty ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

{K116(),1} is non empty set

2 is non empty ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

3 is non empty ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

the non empty set is non empty set

the non empty set * is functional non empty FinSequence-membered M8( the non empty set )

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

the Relation-like NAT -defined PFuncs (( the non empty set *), the non empty set ) -valued Function-like Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs (( the non empty set *), the non empty set ) is Relation-like NAT -defined PFuncs (( the non empty set *), the non empty set ) -valued Function-like Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs (( the non empty set *), the non empty set )

( the non empty set , the Relation-like NAT -defined PFuncs (( the non empty set *), the non empty set ) -valued Function-like Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs (( the non empty set *), the non empty set )) is () ()

the carrier of ( the non empty set , the Relation-like NAT -defined PFuncs (( the non empty set *), the non empty set ) -valued Function-like Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs (( the non empty set *), the non empty set )) is set

U0 is non empty set

U0 * is functional non empty FinSequence-membered M8(U0)

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

x is Relation-like NAT -defined PFuncs ((U0 *),U0) -valued Function-like Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs ((U0 *),U0)

(U0,x) is () ()

the non empty set is non empty set

the Element of the non empty set is Element of the non empty set

the non empty set * is functional non empty FinSequence-membered M8( the non empty set )

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

<*> the non empty set is Relation-like NAT -defined the non empty set -valued Function-like one-to-one constant functional empty Function-yielding V22() ext-real non positive non negative V26() V27() V28() V30() V31() V32() V33() V38() V40( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V59() V60() V62() FinSequence of the non empty set

(<*> the non empty set ) .--> the Element of the non empty set is Relation-like {(<*> the non empty set )} -defined the non empty set -valued Function-like one-to-one set

{(<*> the non empty set )} is functional non empty V12() V40(1) V60() set

{(<*> the non empty set )} --> the Element of the non empty set is Relation-like {(<*> the non empty set )} -defined the non empty set -valued { the Element of the non empty set } -valued Function-like constant non empty total V18({(<*> the non empty set )},{ the Element of the non empty set }) Element of K19(K20({(<*> the non empty set )},{ the Element of the non empty set }))

{ the Element of the non empty set } is non empty V12() V40(1) set

K20({(<*> the non empty set )},{ the Element of the non empty set }) is set

K19(K20({(<*> the non empty set )},{ the Element of the non empty set })) is set

y is Relation-like Function-like Element of PFuncs (( the non empty set *), the non empty set )

<*y*> is Relation-like NAT -defined PFuncs (( the non empty set *), the non empty set ) -valued Function-like constant non empty V12() Function-yielding V22() V33() V40(1) FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs (( the non empty set *), the non empty set )

( the non empty set ,<*y*>) is non empty () ()

the of ( the non empty set ,<*y*>) is Relation-like NAT -defined PFuncs (( the carrier of ( the non empty set ,<*y*>) *), the carrier of ( the non empty set ,<*y*>)) -valued Function-like Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs (( the carrier of ( the non empty set ,<*y*>) *), the carrier of ( the non empty set ,<*y*>))

the carrier of ( the non empty set ,<*y*>) is non empty set

the carrier of ( the non empty set ,<*y*>) * is functional non empty FinSequence-membered M8( the carrier of ( the non empty set ,<*y*>))

PFuncs (( the carrier of ( the non empty set ,<*y*>) *), the carrier of ( the non empty set ,<*y*>)) is functional non empty set

U0 is () ()

the carrier of U0 is set

the of U0 is Relation-like NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 * is functional non empty FinSequence-membered M8( the carrier of U0)

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

U0 is () ()

the carrier of U0 is set

the of U0 is Relation-like NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 * is functional non empty FinSequence-membered M8( the carrier of U0)

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

U0 is () ()

the of U0 is Relation-like NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 is set

the carrier of U0 * is functional non empty FinSequence-membered M8( the carrier of U0)

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

U0 is ext-real V26() V27() V28() V32() V33() V38() V62() set

x is non empty () () ()

the of x is Relation-like non-empty NAT -defined PFuncs (( the carrier of x *), the carrier of x) -valued Function-like non empty Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() homogeneous FinSequence of PFuncs (( the carrier of x *), the carrier of x)

the carrier of x is non empty set

the carrier of x * is functional non empty FinSequence-membered M8( the carrier of x)

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

dom the of x is V62() Element of K19(NAT)

the of x . U0 is Relation-like Function-like homogeneous set

K20(( the carrier of x *), the carrier of x) is set

K19(K20(( the carrier of x *), the carrier of x)) is set

rng the of x is set

U0 is non empty () () ()

the of U0 is Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like non empty Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() homogeneous FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 is non empty set

the carrier of U0 * is functional non empty FinSequence-membered M8( the carrier of U0)

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

len the of U0 is non empty ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

K20(( the carrier of U0 *), the carrier of U0) is set

K19(K20(( the carrier of U0 *), the carrier of U0)) is set

x is ext-real V26() V27() V28() V32() V33() V38() V62() set

Seg (len the of U0) is non empty V33() V40( len the of U0) V62() Element of K19(NAT)

dom the of U0 is V62() Element of K19(NAT)

the of U0 . x is Relation-like Function-like homogeneous set

y is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous Element of K19(K20(( the carrier of U0 *), the carrier of U0))

arity y is ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

m is ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

h is ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

c

arity c

x is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V62() FinSequence of NAT

dom x is V62() Element of K19(NAT)

len x is ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

y is ext-real V26() V27() V28() V32() V33() V38() V62() set

the of U0 . y is Relation-like Function-like homogeneous set

x . y is set

m is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous Element of K19(K20(( the carrier of U0 *), the carrier of U0))

arity m is ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

x is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V62() FinSequence of NAT

len x is ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

dom x is V62() Element of K19(NAT)

y is Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like V62() FinSequence of NAT

len y is ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

dom y is V62() Element of K19(NAT)

m is ext-real V26() V27() V28() V32() V33() V38() V62() set

Seg (len x) is V33() V40( len x) V62() Element of K19(NAT)

dom the of U0 is V62() Element of K19(NAT)

the of U0 . m is Relation-like Function-like homogeneous set

x . m is set

h is Relation-like the carrier of U0 * -defined the carrier of U0 -valued Function-like non empty homogeneous Element of K19(K20(( the carrier of U0 *), the carrier of U0))

arity h is ext-real V26() V27() V28() V32() V33() V38() V62() Element of NAT

y . m is set

U0 is non empty () () () ()

the of U0 is Relation-like non-empty NAT -defined PFuncs (( the carrier of U0 *), the carrier of U0) -valued Function-like non empty Function-yielding V22() V33() FinSequence-like FinSubsequence-like V62() homogeneous quasi_total FinSequence of PFuncs (( the carrier of U0 *), the carrier of U0)

the carrier of U0 is non empty set

the carrier of U0 * is functional non empty FinSequence-membered M8( the carrier of U0)

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