:: MSUALG_1 semantic presentation

REAL is set
NAT is non empty V15() V16() V17() V22() cardinal limit_cardinal Element of K10(REAL)
K10(REAL) is set
NAT is non empty V15() V16() V17() V22() cardinal limit_cardinal set
K10(NAT) is V22() set
K10(NAT) is V22() set
2 is non empty V15() V16() V17() V21() V22() cardinal Element of NAT
K11(2,2) is Relation-like set
K11(K11(2,2),2) is Relation-like set
K10(K11(K11(2,2),2)) is set
BOOLEAN is non empty set

1 is non empty V15() V16() V17() V21() V22() cardinal Element of NAT
{0,1} is non empty set
3 is non empty V15() V16() V17() V21() V22() cardinal Element of NAT

K10(K11({},)) is set

K10(K11({},())) is set

(,{},A,z) is () ()

K11(,()) is Relation-like set
K10(K11(,())) is set

K10(K11(,)) is set

(,,z,A) is () ()
z is non empty non void V62() ()
the carrier' of z is non empty set
the carrier of z is non empty set
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
the of z is non empty Relation-like the carrier' of z -defined the carrier of z * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of z,( the carrier of z *)))
K11( the carrier' of z,( the carrier of z *)) is Relation-like set
K10(K11( the carrier' of z,( the carrier of z *))) is set
A is Element of the carrier' of z
the of z . A is Relation-like NAT -defined Function-like V22() FinSequence-like FinSubsequence-like Element of the carrier of z *
the of z is non empty Relation-like the carrier' of z -defined the carrier of z -valued Function-like total quasi_total Element of K10(K11( the carrier' of z, the carrier of z))
K11( the carrier' of z, the carrier of z) is Relation-like set
K10(K11( the carrier' of z, the carrier of z)) is set
the of z . A is Element of the carrier of z
z is 1-sorted
z is non empty V62() ()
the carrier of z is non empty set
is non empty trivial functional 1 -element set
the carrier of z --> is non empty Relation-like non-empty non empty-yielding the carrier of z -defined -valued Function-like constant total quasi_total Element of K10(K11( the carrier of z,))
is non empty trivial 1 -element set
K11( the carrier of z,) is Relation-like set
K10(K11( the carrier of z,)) is set
the carrier' of z is set
the of z is Relation-like the carrier' of z -defined the carrier of z * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of z,( the carrier of z *)))
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
K11( the carrier' of z,( the carrier of z *)) is Relation-like set
K10(K11( the carrier' of z,( the carrier of z *))) is set
A is non empty Relation-like the carrier of z -defined Function-like total set
A # is non empty Relation-like the carrier of z * -defined Function-like total set
the of z * (A #) is Relation-like the carrier' of z -defined Function-like total set
the of z is Relation-like the carrier' of z -defined the carrier of z -valued Function-like total quasi_total Element of K10(K11( the carrier' of z, the carrier of z))
K11( the carrier' of z, the carrier of z) is Relation-like set
K10(K11( the carrier' of z, the carrier of z)) is set
the of z * A is Relation-like the carrier' of z -defined Function-like total set
the Relation-like the carrier' of z -defined Function-like total Function-yielding V42() ManySortedFunction of the of z * (A #), the of z * A is Relation-like the carrier' of z -defined Function-like total Function-yielding V42() ManySortedFunction of the of z * (A #), the of z * A
(z,A, the Relation-like the carrier' of z -defined Function-like total Function-yielding V42() ManySortedFunction of the of z * (A #), the of z * A) is (z) (z)
z is set
the of (z,A, the Relation-like the carrier' of z -defined Function-like total Function-yielding V42() ManySortedFunction of the of z * (A #), the of z * A) is non empty Relation-like the carrier of z -defined Function-like total set
the of (z,A, the Relation-like the carrier' of z -defined Function-like total Function-yielding V42() ManySortedFunction of the of z * (A #), the of z * A) . z is set
z is 1-sorted
the carrier of z is set
is non empty trivial functional 1 -element set

is non empty trivial 1 -element set
K11( the carrier of z,) is Relation-like set
K10(K11( the carrier of z,)) is set

(z,A) is (z) (z)
f is set
the of (z,A) is Relation-like the carrier of z -defined Function-like total set
the of (z,A) . f is set
z is 1-sorted
A is (z) (z)
the of A is Relation-like the carrier of z -defined Function-like total set
the carrier of z is set
z is non empty V62() ()
A is (z) (z)
the of A is non empty Relation-like non-empty non empty-yielding the carrier of z -defined Function-like total set
the carrier of z is non empty set
rng the of A is non empty set
f is Element of rng the of A
z is set
the of A . z is set
the of A # is non empty Relation-like non-empty non empty-yielding the carrier of z * -defined Function-like total set
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
rng ( the of A #) is non empty set
f is Element of rng ( the of A #)
z is set
( the of A #) . z is set
z is non empty non void V62() ()
the carrier' of z is non empty set
the of z is non empty Relation-like the carrier' of z -defined the carrier of z * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of z,( the carrier of z *)))
the carrier of z is non empty set
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
K11( the carrier' of z,( the carrier of z *)) is Relation-like set
K10(K11( the carrier' of z,( the carrier of z *))) is set
f is (z)
the of f is non empty Relation-like the carrier of z -defined Function-like total set
the of f # is non empty Relation-like the carrier of z * -defined Function-like total set
the of z * ( the of f #) is non empty Relation-like the carrier' of z -defined Function-like total set
A is Element of the carrier' of z
( the of z * ( the of f #)) . A is set
rng ( the of f #) is non empty set
dom ( the of z * ( the of f #)) is non empty set
rng ( the of z * ( the of f #)) is non empty set
the of z is non empty Relation-like the carrier' of z -defined the carrier of z -valued Function-like total quasi_total Element of K10(K11( the carrier' of z, the carrier of z))
K11( the carrier' of z, the carrier of z) is Relation-like set
K10(K11( the carrier' of z, the carrier of z)) is set
the of z * the of f is non empty Relation-like the carrier' of z -defined Function-like total set
( the of z * the of f) . A is set
rng the of f is non empty set
dom ( the of z * the of f) is non empty set
rng ( the of z * the of f) is non empty set
z is non empty non void V62() ()
the carrier' of z is non empty set
f is (z)
the of f is non empty Relation-like the carrier' of z -defined Function-like total Function-yielding V42() ManySortedFunction of the of z * ( the of f #), the of z * the of f
the of z is non empty Relation-like the carrier' of z -defined the carrier of z * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of z,( the carrier of z *)))
the carrier of z is non empty set
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
K11( the carrier' of z,( the carrier of z *)) is Relation-like set
K10(K11( the carrier' of z,( the carrier of z *))) is set
the of f is non empty Relation-like the carrier of z -defined Function-like total set
the of f # is non empty Relation-like the carrier of z * -defined Function-like total set
the of z * ( the of f #) is non empty Relation-like the carrier' of z -defined Function-like total set
the of z is non empty Relation-like the carrier' of z -defined the carrier of z -valued Function-like total quasi_total Element of K10(K11( the carrier' of z, the carrier of z))
K11( the carrier' of z, the carrier of z) is Relation-like set
K10(K11( the carrier' of z, the carrier of z)) is set
the of z * the of f is non empty Relation-like the carrier' of z -defined Function-like total set
A is Element of the carrier' of z
the of f . A is Relation-like Function-like set
(z,A,f) is Element of rng ( the of f #)
rng ( the of f #) is non empty set
( the of z * ( the of f #)) . A is set
(z,A,f) is Element of rng the of f
rng the of f is non empty set
( the of z * the of f) . A is set
K11((z,A,f),(z,A,f)) is Relation-like set
K10(K11((z,A,f),(z,A,f))) is set
z is non empty non void V62() ()
the carrier' of z is non empty set
A is Element of the carrier' of z
f is (z) (z)
(z,A,f) is non empty Relation-like (z,A,f) -defined (z,A,f) -valued Function-like total quasi_total Element of K10(K11((z,A,f),(z,A,f)))
(z,A,f) is non empty Element of rng ( the of f #)
the carrier of z is non empty set
the of f is non empty Relation-like non-empty non empty-yielding the carrier of z -defined Function-like total set
the of f # is non empty Relation-like non-empty non empty-yielding the carrier of z * -defined Function-like total set
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
rng ( the of f #) is non empty set
the of z is non empty Relation-like the carrier' of z -defined the carrier of z * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of z,( the carrier of z *)))
K11( the carrier' of z,( the carrier of z *)) is Relation-like set
K10(K11( the carrier' of z,( the carrier of z *))) is set
the of z * ( the of f #) is non empty Relation-like non-empty non empty-yielding the carrier' of z -defined Function-like total set
( the of z * ( the of f #)) . A is non empty set
(z,A,f) is non empty Element of rng the of f
rng the of f is non empty set
the of z is non empty Relation-like the carrier' of z -defined the carrier of z -valued Function-like total quasi_total Element of K10(K11( the carrier' of z, the carrier of z))
K11( the carrier' of z, the carrier of z) is Relation-like set
K10(K11( the carrier' of z, the carrier of z)) is set
the of z * the of f is non empty Relation-like non-empty non empty-yielding the carrier' of z -defined Function-like total set
( the of z * the of f) . A is non empty set
K11((z,A,f),(z,A,f)) is Relation-like set
K10(K11((z,A,f),(z,A,f))) is set
the of f is non empty Relation-like the carrier' of z -defined Function-like total Function-yielding V42() ManySortedFunction of the of z * ( the of f #), the of z * the of f
the of f . A is Relation-like Function-like set
z is non empty set

K11((z *),z) is Relation-like set
K10(K11((z *),z)) is set
A is non empty Relation-like z * -defined z -valued Function-like homogeneous quasi_total Element of K10(K11((z *),z))

arity A is V15() V16() V17() V21() V22() cardinal Element of NAT
() -tuples_on z is non empty functional FinSequence-membered FinSequenceSet of z

o is set

len h is V15() V16() V17() V21() V22() cardinal Element of NAT
(len h) -tuples_on z is non empty functional FinSequence-membered FinSequenceSet of z
o is set

len z is V15() V16() V17() V21() V22() cardinal Element of NAT

len h is V15() V16() V17() V21() V22() cardinal Element of NAT
z is set
A is non empty set
K11(z,A) is Relation-like set
K10(K11(z,A)) is set
f is non empty set
K11(A,f) is Relation-like set
K10(K11(A,f)) is set
z is Relation-like z -defined A -valued Function-like Element of K10(K11(z,A))
dom z is set
K11((dom z),f) is Relation-like set
K10(K11((dom z),f)) is set
o is non empty Relation-like A -defined f -valued Function-like total quasi_total Element of K10(K11(A,f))
o * z is Relation-like z -defined f -valued Function-like Element of K10(K11(z,f))
K11(z,f) is Relation-like set
K10(K11(z,f)) is set
dom o is non empty set
rng z is set
dom (o * z) is set
rng (o * z) is set
z is non empty set

K11((z *),z) is Relation-like set
K10(K11((z *),z)) is set
A is non empty Relation-like z * -defined z -valued Function-like homogeneous quasi_total Element of K10(K11((z *),z))

arity A is V15() V16() V17() V21() V22() cardinal Element of NAT
Seg () is V22() arity A -element Element of K10(NAT)
Funcs ((Seg ()),z) is non empty functional FUNCTION_DOMAIN of Seg (),z
() -tuples_on z is non empty functional FinSequence-membered FinSequenceSet of z
z is non empty V131() quasi_total non-empty UAStr

the charact of z is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of z *), the carrier of z) -valued Function-like V22() Function-yielding V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of z *), the carrier of z)
the carrier of z is non empty set
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
PFuncs (( the carrier of z *), the carrier of z) is set
len the charact of z is non empty V15() V16() V17() V21() V22() cardinal Element of NAT
len () is V15() V16() V17() V21() V22() cardinal Element of NAT
z is non empty V62() ()
A is (z)
the of A is non empty Relation-like the carrier of z -defined Function-like total set
the carrier of z is non empty set
rng the of A is non empty set
f is Element of rng the of A
z is Element of rng the of A
o is set
the of A . o is set
h is set
the of A . h is set
is non empty trivial functional 1 -element set

A is non empty V131() quasi_total non-empty UAStr

dom () is Element of K10(NAT)
K11((dom ()),()) is Relation-like set
K10(K11((dom ()),())) is set

K11((dom ()),) is Relation-like set
K10(K11((dom ()),)) is set
{z} is non empty trivial functional 1 -element set
K11((dom ()),{z}) is Relation-like set

(,(dom ()),f,((dom ()) --> z)) is () ()
len () is V15() V16() V17() V21() V22() cardinal Element of NAT
the carrier' of (,(dom ()),f,((dom ()) --> z)) is set
Seg (len ()) is V22() len () -element Element of K10(NAT)
the non empty V131() quasi_total non-empty UAStr is non empty V131() quasi_total non-empty UAStr

dom (signature the non empty V131() quasi_total non-empty UAStr ) is Element of K10(NAT)
K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),()) is Relation-like set
K10(K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),())) is set

K11(NAT,()) is Relation-like V22() set
K10(K11(NAT,())) is V22() set
() * (signature the non empty V131() quasi_total non-empty UAStr ) is Relation-like NAT -defined * -valued Function-like Function-yielding V42() Element of K10(K11(NAT,()))
f is Relation-like dom (signature the non empty V131() quasi_total non-empty UAStr ) -defined * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),()))
(dom (signature the non empty V131() quasi_total non-empty UAStr )) --> z is Relation-like dom (signature the non empty V131() quasi_total non-empty UAStr ) -defined -valued Function-like constant total quasi_total Function-yielding V42() Element of K10(K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),))
K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),) is Relation-like set
K10(K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),)) is set
{z} is non empty trivial functional 1 -element set
K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),{z}) is Relation-like set
(,(dom (signature the non empty V131() quasi_total non-empty UAStr )),f,((dom (signature the non empty V131() quasi_total non-empty UAStr )) --> z)) is () ()
A is non empty V131() quasi_total non-empty UAStr

dom () is Element of K10(NAT)

K11(NAT,()) is Relation-like V22() set
K10(K11(NAT,())) is V22() set

K11((dom ()),NAT) is Relation-like set
K10(K11((dom ()),NAT)) is set
K11((dom ()),) is Relation-like set
K11((dom ()),()) is Relation-like set
K10(K11((dom ()),())) is set

K10(K11((dom ()),)) is set
{z} is non empty trivial functional 1 -element set
K11((dom ()),{z}) is Relation-like set
(,(dom ()),f,((dom ()) --> z)) is () ()
z is trivial V56() non void () () ()
the carrier of z is trivial V22() set
the carrier' of z is non empty set
the of z is non empty Relation-like the carrier' of z -defined the carrier of z * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of z,( the carrier of z *)))
the carrier of z * is non empty functional FinSequence-membered FinSequenceSet of the carrier of z
K11( the carrier' of z,( the carrier of z *)) is Relation-like set
K10(K11( the carrier' of z,( the carrier of z *))) is set
the of z is Relation-like the carrier' of z -defined the carrier of z -valued Function-like quasi_total Element of K10(K11( the carrier' of z, the carrier of z))
K11( the carrier' of z, the carrier of z) is Relation-like set
K10(K11( the carrier' of z, the carrier of z)) is set
o is trivial V56() non void () () ()
the carrier of o is trivial V22() set
the carrier' of o is non empty set
the of o is non empty Relation-like the carrier' of o -defined the carrier of o * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of o,( the carrier of o *)))
the carrier of o * is non empty functional FinSequence-membered FinSequenceSet of the carrier of o
K11( the carrier' of o,( the carrier of o *)) is Relation-like set
K10(K11( the carrier' of o,( the carrier of o *))) is set
the of o is Relation-like the carrier' of o -defined the carrier of o -valued Function-like quasi_total Element of K10(K11( the carrier' of o, the carrier of o))
K11( the carrier' of o, the carrier of o) is Relation-like set
K10(K11( the carrier' of o, the carrier of o)) is set
A is non empty V131() quasi_total non-empty UAStr
(A) is trivial V56() non void () () ()
the carrier of (A) is trivial V22() set
A is non empty V131() quasi_total non-empty UAStr
the carrier of A is non empty set

--> the carrier of A is non empty Relation-like non-empty non empty-yielding -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11(,{ the carrier of A}))
{ the carrier of A} is non empty trivial 1 -element set
K11(,{ the carrier of A}) is Relation-like set
K10(K11(,{ the carrier of A})) is set
(A) is non empty trivial V56() non void 1 -element V62() () () ()
the carrier of (A) is non empty trivial V22() 1 -element set
z is non empty Relation-like the carrier of (A) -defined Function-like total set
A is non empty V131() quasi_total non-empty UAStr
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V22() Function-yielding V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A is non empty set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is set
(A) is non empty trivial V56() non void 1 -element V62() () () ()
the carrier' of (A) is non empty set
the of (A) is non empty Relation-like the carrier' of (A) -defined the carrier of (A) * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of (A),( the carrier of (A) *)))
the carrier of (A) is non empty trivial V22() 1 -element set
the carrier of (A) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (A)
K11( the carrier' of (A),( the carrier of (A) *)) is Relation-like set
K10(K11( the carrier' of (A),( the carrier of (A) *))) is set
(A) is non empty Relation-like non-empty non empty-yielding the carrier of (A) -defined Function-like total set

--> the carrier of A is non empty Relation-like non-empty non empty-yielding -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11(,{ the carrier of A}))
{ the carrier of A} is non empty trivial 1 -element set
K11(,{ the carrier of A}) is Relation-like set
K10(K11(,{ the carrier of A})) is set
(A) # is non empty Relation-like non-empty non empty-yielding the carrier of (A) * -defined Function-like total set
the of (A) * ((A) #) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set
the of (A) is non empty Relation-like the carrier' of (A) -defined the carrier of (A) -valued Function-like total quasi_total Element of K10(K11( the carrier' of (A), the carrier of (A)))
K11( the carrier' of (A), the carrier of (A)) is Relation-like set
K10(K11( the carrier' of (A), the carrier of (A))) is set
the of (A) * (A) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set

dom () is Element of K10(NAT)

K11((dom ()),NAT) is Relation-like set
K10(K11((dom ()),NAT)) is set
K11((dom ()),) is Relation-like set
f is non empty set
len () is V15() V16() V17() V21() V22() cardinal Element of NAT
len the charact of A is non empty V15() V16() V17() V21() V22() cardinal Element of NAT
dom the charact of A is non empty Element of K10(NAT)

j is set

z . j is set
o . j is set
K11((z . j),(o . j)) is Relation-like set
K10(K11((z . j),(o . j))) is set
K11(( the carrier of A *), the carrier of A) is Relation-like set
K10(K11(( the carrier of A *), the carrier of A)) is set
n is V15() V16() V17() V21() V22() cardinal set

dom ((dom ()) --> 0) is set
((dom ()) --> 0) . n is Relation-like Function-like set
(A) . (((dom ()) --> 0) . n) is set
( --> the carrier of A) . 0 is set
h is non empty Relation-like the carrier of A * -defined the carrier of A -valued Function-like homogeneous quasi_total Element of K10(K11(( the carrier of A *), the carrier of A))
rng h is non empty set

() * (() * ((A) #)) is Relation-like non-empty NAT -defined Function-like set
(() * (() * ((A) #))) . n is set

() * (u #) is non empty Relation-like NAT -defined Function-like total set
() . n is set
(() * (u #)) . (() . n) is set
arity h is V15() V16() V17() V21() V22() cardinal Element of NAT
(() * (u #)) . () is set
Seg () is V22() arity h -element Element of K10(NAT)
Funcs ((Seg ()), the carrier of A) is non empty functional FUNCTION_DOMAIN of Seg (), the carrier of A
o is Element of f

dom (x . o) is set
A is non empty V131() quasi_total non-empty UAStr
(A) is non empty trivial V56() non void 1 -element V62() () () ()
(A) is non empty Relation-like non-empty non empty-yielding the carrier of (A) -defined Function-like total set
the carrier of (A) is non empty trivial V22() 1 -element set
the carrier of A is non empty set

--> the carrier of A is non empty Relation-like non-empty non empty-yielding -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11(,{ the carrier of A}))
{ the carrier of A} is non empty trivial 1 -element set
K11(,{ the carrier of A}) is Relation-like set
K10(K11(,{ the carrier of A})) is set
(A) is non empty Relation-like the carrier' of (A) -defined Function-like total Function-yielding V42() ManySortedFunction of the of (A) * ((A) #), the of (A) * (A)
the carrier' of (A) is non empty set
the of (A) is non empty Relation-like the carrier' of (A) -defined the carrier of (A) * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of (A),( the carrier of (A) *)))
the carrier of (A) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (A)
K11( the carrier' of (A),( the carrier of (A) *)) is Relation-like set
K10(K11( the carrier' of (A),( the carrier of (A) *))) is set
(A) # is non empty Relation-like non-empty non empty-yielding the carrier of (A) * -defined Function-like total set
the of (A) * ((A) #) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set
the of (A) is non empty Relation-like the carrier' of (A) -defined the carrier of (A) -valued Function-like total quasi_total Element of K10(K11( the carrier' of (A), the carrier of (A)))
K11( the carrier' of (A), the carrier of (A)) is Relation-like set
K10(K11( the carrier' of (A), the carrier of (A))) is set
the of (A) * (A) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V22() Function-yielding V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is set
((A),(A),(A)) is ((A)) ((A))
A is non empty V131() quasi_total non-empty UAStr
(A) is non empty trivial V56() non void 1 -element V62() () () ()
(A) is ((A)) ((A))
(A) is non empty Relation-like non-empty non empty-yielding the carrier of (A) -defined Function-like total set
the carrier of (A) is non empty trivial V22() 1 -element set
the carrier of A is non empty set

--> the carrier of A is non empty Relation-like non-empty non empty-yielding -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11(,{ the carrier of A}))
{ the carrier of A} is non empty trivial 1 -element set
K11(,{ the carrier of A}) is Relation-like set
K10(K11(,{ the carrier of A})) is set
(A) is non empty Relation-like the carrier' of (A) -defined Function-like total Function-yielding V42() ManySortedFunction of the of (A) * ((A) #), the of (A) * (A)
the carrier' of (A) is non empty set
the of (A) is non empty Relation-like the carrier' of (A) -defined the carrier of (A) * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of (A),( the carrier of (A) *)))
the carrier of (A) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (A)
K11( the carrier' of (A),( the carrier of (A) *)) is Relation-like set
K10(K11( the carrier' of (A),( the carrier of (A) *))) is set
(A) # is non empty Relation-like non-empty non empty-yielding the carrier of (A) * -defined Function-like total set
the of (A) * ((A) #) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set
the of (A) is non empty Relation-like the carrier' of (A) -defined the carrier of (A) -valued Function-like total quasi_total Element of K10(K11( the carrier' of (A), the carrier of (A)))
K11( the carrier' of (A), the carrier of (A)) is Relation-like set
K10(K11( the carrier' of (A), the carrier of (A))) is set
the of (A) * (A) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V22() Function-yielding V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is set
((A),(A),(A)) is ((A)) ((A))
the of (A) is non empty Relation-like the carrier of (A) -defined Function-like total set
A is non empty trivial V56() 1 -element V62() ()
f is (A)
the of f is non empty Relation-like the carrier of A -defined Function-like total set
the carrier of A is non empty trivial V22() 1 -element set
rng the of f is non empty set
the Element of rng the of f is Element of rng the of f
z is set
o is set
A is non empty trivial V56() 1 -element V62() ()
f is (A) (A)
(A,f) is set
the of f is non empty Relation-like non-empty non empty-yielding the carrier of A -defined Function-like total set
the carrier of A is non empty trivial V22() 1 -element set
rng the of f is non empty set
A is non empty trivial V56() non void 1 -element V62() () ()
the carrier' of A is non empty set
f is Element of the carrier' of A
(A,f) is Relation-like NAT -defined the carrier of A -valued Function-like V22() FinSequence-like FinSubsequence-like Element of the carrier of A *
the carrier of A is non empty trivial V22() 1 -element set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
the of A is non empty Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of A,( the carrier of A *)))
K11( the carrier' of A,( the carrier of A *)) is Relation-like set
K10(K11( the carrier' of A,( the carrier of A *))) is set
the of A . f is Relation-like NAT -defined Function-like V22() FinSequence-like FinSubsequence-like Element of the carrier of A *
len (A,f) is V15() V16() V17() V21() V22() cardinal Element of NAT
z is (A) (A)
(A,f,z) is non empty Element of rng ( the of z #)
the of z is non empty Relation-like non-empty non empty-yielding the carrier of A -defined Function-like total set
the of z # is non empty Relation-like non-empty non empty-yielding the carrier of A * -defined Function-like total set
rng ( the of z #) is non empty set
the of A * ( the of z #) is non empty Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like total set
( the of A * ( the of z #)) . f is non empty set
(A,z) is non empty set
(len (A,f)) -tuples_on (A,z) is non empty functional FinSequence-membered FinSequenceSet of (A,z)
dom the of A is non empty set
( the of z #) . ( the of A . f) is non empty set
(A,f) * the of z is Relation-like non-empty NAT -defined Function-like set
product ((A,f) * the of z) is set
rng (A,f) is set
dom the of z is non empty set
dom ((A,f) * the of z) is set
dom (A,f) is Element of K10(NAT)
h is set

dom x is set
j is V15() V16() V17() V21() V22() cardinal set
Seg j is V22() j -element Element of K10(NAT)

rng y is set
j is set
u is set
y . u is set
(A,f) . u is set
the of z . ((A,f) . u) is set
rng the of z is non empty set
x . u is set
((A,f) * the of z) . u is set
len y is V15() V16() V17() V21() V22() cardinal Element of NAT
h is set
Seg (len (A,f)) is V22() len (A,f) -element Element of K10(NAT)
Funcs ((Seg (len (A,f))),(A,z)) is non empty functional FUNCTION_DOMAIN of Seg (len (A,f)),(A,z)

dom x is set
rng x is set
y is set
(A,f) . y is set
the of z . ((A,f) . y) is set
rng the of z is non empty set
x . y is set
((A,f) * the of z) . y is set
A is non empty trivial V56() non void 1 -element V62() () ()
the carrier' of A is non empty set
f is Element of the carrier' of A
z is (A) (A)
(A,f,z) is non empty Element of rng ( the of z #)
the carrier of A is non empty trivial V22() 1 -element set
the of z is non empty Relation-like non-empty non empty-yielding the carrier of A -defined Function-like total set
the of z # is non empty Relation-like non-empty non empty-yielding the carrier of A * -defined Function-like total set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
rng ( the of z #) is non empty set
the of A is non empty Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of A,( the carrier of A *)))
K11( the carrier' of A,( the carrier of A *)) is Relation-like set
K10(K11( the carrier' of A,( the carrier of A *))) is set
the of A * ( the of z #) is non empty Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like total set
( the of A * ( the of z #)) . f is non empty set
(A,z) is non empty set
(A,z) * is non empty functional FinSequence-membered FinSequenceSet of (A,z)
(A,f) is Relation-like NAT -defined the carrier of A -valued Function-like V22() FinSequence-like FinSubsequence-like Element of the carrier of A *
the of A . f is Relation-like NAT -defined Function-like V22() FinSequence-like FinSubsequence-like Element of the carrier of A *
len (A,f) is V15() V16() V17() V21() V22() cardinal Element of NAT
(len (A,f)) -tuples_on (A,z) is non empty functional FinSequence-membered FinSequenceSet of (A,z)
A is non empty trivial V56() non void 1 -element V62() () ()
f is (A) (A)
the of f is non empty Relation-like the carrier' of A -defined Function-like total Function-yielding V42() ManySortedFunction of the of A * ( the of f #), the of A * the of f
the carrier' of A is non empty set
the of A is non empty Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of A,( the carrier of A *)))
the carrier of A is non empty trivial V22() 1 -element set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
K11( the carrier' of A,( the carrier of A *)) is Relation-like set
K10(K11( the carrier' of A,( the carrier of A *))) is set
the of f is non empty Relation-like non-empty non empty-yielding the carrier of A -defined Function-like total set
the of f # is non empty Relation-like non-empty non empty-yielding the carrier of A * -defined Function-like total set
the of A * ( the of f #) is non empty Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like total set
the of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of K10(K11( the carrier' of A, the carrier of A))
K11( the carrier' of A, the carrier of A) is Relation-like set
K10(K11( the carrier' of A, the carrier of A)) is set
the of A * the of f is non empty Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like total set
(A,f) is non empty set
(A,f) * is non empty functional FinSequence-membered FinSequenceSet of (A,f)
PFuncs (((A,f) *),(A,f)) is set
dom the of f is non empty set
z is V15() V16() V17() V21() V22() cardinal set
Seg z is V22() z -element Element of K10(NAT)
o is V15() V16() V17() V21() V22() cardinal Element of NAT
Seg o is V22() o -element Element of K10(NAT)

o is set
rng z is set
h is set
z . h is set
x is Element of the carrier' of A
the of A . x is Element of the carrier of A
the of f . ( the of A . x) is non empty set
rng the of f is non empty set
dom the of A is non empty set
( the of A * the of f) . x is non empty set
(A,x,f) is non empty Element of rng ( the of f #)
rng ( the of f #) is non empty set
( the of A * ( the of f #)) . x is non empty set
K11((A,x,f),(A,f)) is Relation-like set
K10(K11((A,x,f),(A,f))) is set
K11(((A,f) *),(A,f)) is Relation-like set
K10(K11(((A,f) *),(A,f))) is set
A is non empty trivial V56() non void 1 -element V62() () ()
f is (A) (A)
the of f is non empty Relation-like the carrier' of A -defined Function-like total Function-yielding V42() ManySortedFunction of the of A * ( the of f #), the of A * the of f
the carrier' of A is non empty set
the of A is non empty Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of A,( the carrier of A *)))
the carrier of A is non empty trivial V22() 1 -element set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
K11( the carrier' of A,( the carrier of A *)) is Relation-like set
K10(K11( the carrier' of A,( the carrier of A *))) is set
the of f is non empty Relation-like non-empty non empty-yielding the carrier of A -defined Function-like total set
the of f # is non empty Relation-like non-empty non empty-yielding the carrier of A * -defined Function-like total set
the of A * ( the of f #) is non empty Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like total set
the of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of K10(K11( the carrier' of A, the carrier of A))
K11( the carrier' of A, the carrier of A) is Relation-like set
K10(K11( the carrier' of A, the carrier of A)) is set
the of A * the of f is non empty Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like total set
(A,f) is non empty set
(A,f) * is non empty functional FinSequence-membered FinSequenceSet of (A,f)
PFuncs (((A,f) *),(A,f)) is set
A is non empty trivial V56() non void 1 -element V62() () ()
f is (A) (A)
(A,f) is non empty set
(A,f) is Relation-like NAT -defined PFuncs (((A,f) *),(A,f)) -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((A,f) *),(A,f))
(A,f) * is non empty functional FinSequence-membered FinSequenceSet of (A,f)
PFuncs (((A,f) *),(A,f)) is set
the of f is non empty Relation-like the carrier' of A -defined Function-like total Function-yielding V42() ManySortedFunction of the of A * ( the of f #), the of A * the of f
the carrier' of A is non empty set
the of A is non empty Relation-like the carrier' of A -defined the carrier of A * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of A,( the carrier of A *)))
the carrier of A is non empty trivial V22() 1 -element set
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
K11( the carrier' of A,( the carrier of A *)) is Relation-like set
K10(K11( the carrier' of A,( the carrier of A *))) is set
the of f is non empty Relation-like non-empty non empty-yielding the carrier of A -defined Function-like total set
the of f # is non empty Relation-like non-empty non empty-yielding the carrier of A * -defined Function-like total set
the of A * ( the of f #) is non empty Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like total set
the of A is non empty Relation-like the carrier' of A -defined the carrier of A -valued Function-like total quasi_total Element of K10(K11( the carrier' of A, the carrier of A))
K11( the carrier' of A, the carrier of A) is Relation-like set
K10(K11( the carrier' of A, the carrier of A)) is set
the of A * the of f is non empty Relation-like non-empty non empty-yielding the carrier' of A -defined Function-like total set
UAStr(# (A,f),(A,f) #) is non empty strict UAStr
K11(((A,f) *),(A,f)) is Relation-like set
K10(K11(((A,f) *),(A,f))) is set
z is V15() V16() V17() V21() V22() cardinal set
dom (A,f) is Element of K10(NAT)
(A,f) . z is set
o is Relation-like (A,f) * -defined (A,f) -valued Function-like Element of K10(K11(((A,f) *),(A,f)))

len x is V15() V16() V17() V21() V22() cardinal Element of NAT

len y is V15() V16() V17() V21() V22() cardinal Element of NAT
h is Element of the carrier' of A
( the of A * ( the of f #)) . h is non empty set
(A,h,f) is non empty Element of rng ( the of f #)
rng ( the of f #) is non empty set
( the of A * the of f) . h is non empty set
K11((( the of A * ( the of f #)) . h),(( the of A * the of f) . h)) is Relation-like set
K10(K11((( the of A * ( the of f #)) . h),(( the of A * the of f) . h))) is set
(A,h) is Relation-like NAT -defined the carrier of A -valued Function-like V22() FinSequence-like FinSubsequence-like Element of the carrier of A *
the of A . h is Relation-like NAT -defined Function-like V22() FinSequence-like FinSubsequence-like Element of the carrier of A *
len (A,h) is V15() V16() V17() V21() V22() cardinal Element of NAT
(len (A,h)) -tuples_on (A,f) is non empty functional FinSequence-membered FinSequenceSet of (A,f)
K11(((A,f) *),(A,f)) is Relation-like set
K10(K11(((A,f) *),(A,f))) is set
z is V15() V16() V17() V21() V22() cardinal set
dom (A,f) is Element of K10(NAT)
(A,f) . z is set
o is Relation-like (A,f) * -defined (A,f) -valued Function-like Element of K10(K11(((A,f) *),(A,f)))

len x is V15() V16() V17() V21() V22() cardinal Element of NAT
len y is V15() V16() V17() V21() V22() cardinal Element of NAT
h is Element of the carrier' of A
( the of A * ( the of f #)) . h is non empty set
(A,h,f) is non empty Element of rng ( the of f #)
rng ( the of f #) is non empty set
( the of A * the of f) . h is non empty set
K11((( the of A * ( the of f #)) . h),(( the of A * the of f) . h)) is Relation-like set
K10(K11((( the of A * ( the of f #)) . h),(( the of A * the of f) . h))) is set
(A,h) is Relation-like NAT -defined the carrier of A -valued Function-like V22() FinSequence-like FinSubsequence-like Element of the carrier of A *
the of A . h is Relation-like NAT -defined Function-like V22() FinSequence-like FinSubsequence-like Element of the carrier of A *
len (A,h) is V15() V16() V17() V21() V22() cardinal Element of NAT
(len (A,h)) -tuples_on (A,f) is non empty functional FinSequence-membered FinSequenceSet of (A,f)
z is set
dom (A,f) is set
(A,f) . z is set
dom (A,f) is Element of K10(NAT)
o is Element of the carrier' of A
(A,o,f) is non empty Relation-like (A,o,f) -defined (A,o,f) -valued Function-like total quasi_total Element of K10(K11((A,o,f),(A,o,f)))
(A,o,f) is non empty Element of rng ( the of f #)
rng ( the of f #) is non empty set
( the of A * ( the of f #)) . o is non empty set
(A,o,f) is non empty Element of rng the of f
rng the of f is non empty set
( the of A * the of f) . o is non empty set
K11((A,o,f),(A,o,f)) is Relation-like set
K10(K11((A,o,f),(A,o,f))) is set
the of f . o is Relation-like Function-like set
A is non empty strict V131() quasi_total non-empty UAStr
(A) is non empty trivial V56() non void 1 -element V62() () () ()
(A) is ((A)) ((A)) ((A))
(A) is non empty Relation-like non-empty non empty-yielding the carrier of (A) -defined Function-like total set
the carrier of (A) is non empty trivial V22() 1 -element set
the carrier of A is non empty set

--> the carrier of A is non empty Relation-like non-empty non empty-yielding -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11(,{ the carrier of A}))
{ the carrier of A} is non empty trivial 1 -element set
K11(,{ the carrier of A}) is Relation-like set
K10(K11(,{ the carrier of A})) is set
(A) is non empty Relation-like the carrier' of (A) -defined Function-like total Function-yielding V42() ManySortedFunction of the of (A) * ((A) #), the of (A) * (A)
the carrier' of (A) is non empty set
the of (A) is non empty Relation-like the carrier' of (A) -defined the carrier of (A) * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of (A),( the carrier of (A) *)))
the carrier of (A) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (A)
K11( the carrier' of (A),( the carrier of (A) *)) is Relation-like set
K10(K11( the carrier' of (A),( the carrier of (A) *))) is set
(A) # is non empty Relation-like non-empty non empty-yielding the carrier of (A) * -defined Function-like total set
the of (A) * ((A) #) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set
the of (A) is non empty Relation-like the carrier' of (A) -defined the carrier of (A) -valued Function-like total quasi_total Element of K10(K11( the carrier' of (A), the carrier of (A)))
K11( the carrier' of (A), the carrier of (A)) is Relation-like set
K10(K11( the carrier' of (A), the carrier of (A))) is set
the of (A) * (A) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set
the charact of A is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of A *), the carrier of A) -valued Function-like V22() Function-yielding V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of A *), the carrier of A)
the carrier of A * is non empty functional FinSequence-membered FinSequenceSet of the carrier of A
PFuncs (( the carrier of A *), the carrier of A) is set
((A),(A),(A)) is ((A)) ((A))
((A),(A)) is non empty strict V131() quasi_total non-empty UAStr
((A),(A)) is non empty set
((A),(A)) is Relation-like NAT -defined PFuncs ((((A),(A)) *),((A),(A))) -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((((A),(A)) *),((A),(A)))
((A),(A)) * is non empty functional FinSequence-membered FinSequenceSet of ((A),(A))
PFuncs ((((A),(A)) *),((A),(A))) is set
the of (A) is non empty Relation-like the carrier' of (A) -defined Function-like total Function-yielding V42() ManySortedFunction of the of (A) * ( the of (A) #), the of (A) * the of (A)
the of (A) is non empty Relation-like non-empty non empty-yielding the carrier of (A) -defined Function-like total set
the of (A) # is non empty Relation-like non-empty non empty-yielding the carrier of (A) * -defined Function-like total set
the of (A) * ( the of (A) #) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set
the of (A) * the of (A) is non empty Relation-like non-empty non empty-yielding the carrier' of (A) -defined Function-like total set
UAStr(# ((A),(A)),((A),(A)) #) is non empty strict UAStr
rng the of (A) is non empty set
A is non empty V131() quasi_total non-empty UAStr

dom () is Element of K10(NAT)
K11((dom ()),()) is Relation-like set
K10(K11((dom ()),())) is set

(A) is non empty trivial V56() non void 1 -element V62() () () ()

K11((dom ()),) is Relation-like set
K10(K11((dom ()),)) is set
{z} is non empty trivial functional 1 -element set
K11((dom ()),{z}) is Relation-like set
(,(dom ()),f,((dom ()) --> z)) is () ()
the carrier' of (A) is non empty set
the of (A) is non empty Relation-like the carrier' of (A) -defined the carrier of (A) * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11( the carrier' of (A),( the carrier of (A) *)))
the carrier of (A) is non empty trivial V22() 1 -element set
the carrier of (A) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (A)
K11( the carrier' of (A),( the carrier of (A) *)) is Relation-like set
K10(K11( the carrier' of (A),( the carrier of (A) *))) is set