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