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

0 is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V15() V16() V17() V19() V20() V21() V22() cardinal {} -element with_common_domain Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

{} is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V15() V16() V17() V19() V20() V21() V22() cardinal {} -element with_common_domain Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered set

the empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V15() V16() V17() V19() V20() V21() V22() cardinal {} -element with_common_domain Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered set is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V15() V16() V17() V19() V20() V21() V22() cardinal {} -element with_common_domain Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered 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

{{}} is non empty trivial functional 1 -element set

K11({},{{}}) is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V15() V16() V17() V19() V20() V21() V22() cardinal {} -element with_common_domain Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered set

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

{} --> {} is empty trivial Relation-like non-empty empty-yielding {} -defined {{}} -valued Function-like one-to-one constant functional total V15() V16() V17() V19() V20() V21() V22() cardinal {} -element with_common_domain quasi_total Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of K10(K11({},{{}}))

{{}} * is non empty functional FinSequence-membered FinSequenceSet of {{}}

K11({},({{}} *)) is empty trivial Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V15() V16() V17() V19() V20() V21() V22() cardinal {} -element with_common_domain Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered set

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

A is empty trivial Relation-like non-empty empty-yielding {} -defined {{}} * -valued Function-like one-to-one constant functional total V15() V16() V17() V19() V20() V21() V22() cardinal {} -element with_common_domain quasi_total Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of K10(K11({},({{}} *)))

z is empty trivial Relation-like non-empty empty-yielding {} -defined {{}} -valued Function-like one-to-one constant functional total V15() V16() V17() V19() V20() V21() V22() cardinal {} -element with_common_domain quasi_total Function-yielding V42() FinSequence-like FinSubsequence-like FinSequence-membered Element of K10(K11({},{{}}))

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

{{}} is non empty trivial functional 1 -element set

{{}} * is non empty functional FinSequence-membered FinSequenceSet of {{}}

K11({{}},({{}} *)) is Relation-like set

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

{{}} --> {} is non empty Relation-like {{}} -defined {{}} -valued Function-like constant total quasi_total Function-yielding V42() Element of K10(K11({{}},{{}}))

K11({{}},{{}}) is Relation-like set

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

z is non empty Relation-like {{}} -defined {{}} * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11({{}},({{}} *)))

A is non empty Relation-like {{}} -defined {{}} -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11({{}},{{}}))

({{}},{{}},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

{0} is non empty trivial functional 1 -element set

the carrier of z --> {0} is non empty Relation-like non-empty non empty-yielding the carrier of z -defined {{0}} -valued Function-like constant total quasi_total Element of K10(K11( the carrier of z,{{0}}))

{{0}} is non empty trivial 1 -element set

K11( the carrier of z,{{0}}) is Relation-like set

K10(K11( the carrier of z,{{0}})) 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

{0} is non empty trivial functional 1 -element set

the carrier of z --> {0} is Relation-like non-empty the carrier of z -defined {{0}} -valued Function-like constant total quasi_total Element of K10(K11( the carrier of z,{{0}}))

{{0}} is non empty trivial 1 -element set

K11( the carrier of z,{{0}}) is Relation-like set

K10(K11( the carrier of z,{{0}})) is set

A is Relation-like the carrier of z -defined Function-like total 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

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

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

dom A is non empty functional with_common_domain FinSequence-membered set

arity A is V15() V16() V17() V21() V22() cardinal Element of NAT

(arity A) -tuples_on z is non empty functional FinSequence-membered FinSequenceSet of z

the Relation-like NAT -defined Function-like V22() FinSequence-like FinSubsequence-like Element of dom A is Relation-like NAT -defined Function-like V22() FinSequence-like FinSubsequence-like Element of dom A

o is set

h is Relation-like NAT -defined z -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of z

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

z is Relation-like NAT -defined z -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of z

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

h is Relation-like NAT -defined z -valued Function-like V22() arity A -element FinSequence-like FinSubsequence-like Element of (arity A) -tuples_on z

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

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

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

dom A is non empty functional with_common_domain FinSequence-membered set

arity A is V15() V16() V17() V21() V22() cardinal Element of NAT

Seg (arity A) is V22() arity A -element Element of K10(NAT)

Funcs ((Seg (arity A)),z) is non empty functional FUNCTION_DOMAIN of Seg (arity A),z

(arity A) -tuples_on z is non empty functional FinSequence-membered FinSequenceSet of z

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

signature z is Relation-like NAT -defined NAT -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of NAT

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 (signature z) 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

{0} is non empty trivial functional 1 -element set

{0} * is non empty functional FinSequence-membered FinSequenceSet of {0}

z is Relation-like Function-like Element of {0}

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

signature A is Relation-like NAT -defined NAT -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of NAT

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

K11((dom (signature A)),({0} *)) is Relation-like set

K10(K11((dom (signature A)),({0} *))) is set

(dom (signature A)) --> z is Relation-like dom (signature A) -defined {0} -valued Function-like constant total quasi_total Function-yielding V42() Element of K10(K11((dom (signature A)),{0}))

K11((dom (signature A)),{0}) is Relation-like set

K10(K11((dom (signature A)),{0})) is set

{z} is non empty trivial functional 1 -element set

K11((dom (signature A)),{z}) is Relation-like set

f is Relation-like dom (signature A) -defined {0} * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11((dom (signature A)),({0} *)))

({0},(dom (signature A)),f,((dom (signature A)) --> z)) is () ()

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

the carrier' of ({0},(dom (signature A)),f,((dom (signature A)) --> z)) is set

Seg (len (signature A)) is V22() len (signature A) -element Element of K10(NAT)

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

signature the non empty V131() quasi_total non-empty UAStr is Relation-like NAT -defined NAT -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of NAT

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 )),({0} *)) is Relation-like set

K10(K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),({0} *))) is set

*--> 0 is non empty Relation-like NAT -defined {0} * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11(NAT,({0} *)))

K11(NAT,({0} *)) is Relation-like V22() set

K10(K11(NAT,({0} *))) is V22() set

(*--> 0) * (signature the non empty V131() quasi_total non-empty UAStr ) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V42() Element of K10(K11(NAT,({0} *)))

f is Relation-like dom (signature the non empty V131() quasi_total non-empty UAStr ) -defined {0} * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),({0} *)))

(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 {0} -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 )),{0}))

K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),{0}) is Relation-like set

K10(K11((dom (signature the non empty V131() quasi_total non-empty UAStr )),{0})) 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

({0},(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

signature A is Relation-like NAT -defined NAT -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of NAT

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

*--> 0 is non empty Relation-like NAT -defined {0} * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11(NAT,({0} *)))

K11(NAT,({0} *)) is Relation-like V22() set

K10(K11(NAT,({0} *))) is V22() set

(*--> 0) * (signature A) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V42() Element of K10(K11(NAT,({0} *)))

(dom (signature A)) --> 0 is Relation-like dom (signature A) -defined NAT -valued Function-like constant total quasi_total Function-yielding V42() Element of K10(K11((dom (signature A)),NAT))

K11((dom (signature A)),NAT) is Relation-like set

K10(K11((dom (signature A)),NAT)) is set

K11((dom (signature A)),{0}) is Relation-like set

K11((dom (signature A)),({0} *)) is Relation-like set

K10(K11((dom (signature A)),({0} *))) is set

f is Relation-like dom (signature A) -defined {0} * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11((dom (signature A)),({0} *)))

(dom (signature A)) --> z is Relation-like dom (signature A) -defined {0} -valued Function-like constant total quasi_total Function-yielding V42() Element of K10(K11((dom (signature A)),{0}))

K10(K11((dom (signature A)),{0})) is set

{z} is non empty trivial functional 1 -element set

K11((dom (signature A)),{z}) is Relation-like set

({0},(dom (signature A)),f,((dom (signature A)) --> 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

0 .--> the carrier of A is Relation-like NAT -defined {0} -defined Function-like one-to-one set

{0} --> the carrier of A is non empty Relation-like non-empty non empty-yielding {0} -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11({0},{ the carrier of A}))

{ the carrier of A} is non empty trivial 1 -element set

K11({0},{ the carrier of A}) is Relation-like set

K10(K11({0},{ 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

0 .--> the carrier of A is Relation-like NAT -defined {0} -defined Function-like one-to-one set

{0} --> the carrier of A is non empty Relation-like non-empty non empty-yielding {0} -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11({0},{ the carrier of A}))

{ the carrier of A} is non empty trivial 1 -element set

K11({0},{ the carrier of A}) is Relation-like set

K10(K11({0},{ 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

signature A is Relation-like NAT -defined NAT -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of NAT

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

(dom (signature A)) --> 0 is Relation-like dom (signature A) -defined NAT -valued Function-like constant total quasi_total Function-yielding V42() Element of K10(K11((dom (signature A)),NAT))

K11((dom (signature A)),NAT) is Relation-like set

K10(K11((dom (signature A)),NAT)) is set

K11((dom (signature A)),{0}) is Relation-like set

f is non empty set

len (signature A) 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)

(*--> 0) * (signature A) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V42() Element of K10(K11(NAT,({0} *)))

h is non empty Relation-like f -defined Function-like total set

x is non empty Relation-like f -defined Function-like total Function-yielding V42() set

z is non empty Relation-like f -defined Function-like total set

o is non empty Relation-like f -defined Function-like total set

j is set

x . j is Relation-like Function-like 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

x . n is Relation-like Function-like set

dom ((dom (signature A)) --> 0) is set

((dom (signature A)) --> 0) . n is Relation-like Function-like set

(A) . (((dom (signature A)) --> 0) . n) is set

({0} --> 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

(*--> 0) * ((A) #) is Relation-like non-empty NAT -defined Function-like set

(signature A) * ((*--> 0) * ((A) #)) is Relation-like non-empty NAT -defined Function-like set

((signature A) * ((*--> 0) * ((A) #))) . n is set

u is non empty Relation-like {0} -defined Function-like total set

u # is non empty Relation-like {0} * -defined Function-like total set

(*--> 0) * (u #) is non empty Relation-like NAT -defined Function-like total set

(signature A) . n is set

((*--> 0) * (u #)) . ((signature A) . n) is set

arity h is V15() V16() V17() V21() V22() cardinal Element of NAT

((*--> 0) * (u #)) . (arity h) is set

Seg (arity h) is V22() arity h -element Element of K10(NAT)

Funcs ((Seg (arity h)), the carrier of A) is non empty functional FUNCTION_DOMAIN of Seg (arity h), the carrier of A

o is Element of f

x . o is Relation-like Function-like set

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

0 .--> the carrier of A is Relation-like NAT -defined {0} -defined Function-like one-to-one set

{0} --> the carrier of A is non empty Relation-like non-empty non empty-yielding {0} -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11({0},{ the carrier of A}))

{ the carrier of A} is non empty trivial 1 -element set

K11({0},{ the carrier of A}) is Relation-like set

K10(K11({0},{ 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

0 .--> the carrier of A is Relation-like NAT -defined {0} -defined Function-like one-to-one set

{0} --> the carrier of A is non empty Relation-like non-empty non empty-yielding {0} -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11({0},{ the carrier of A}))

{ the carrier of A} is non empty trivial 1 -element set

K11({0},{ the carrier of A}) is Relation-like set

K10(K11({0},{ 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

x is Relation-like Function-like set

dom x is set

j is V15() V16() V17() V21() V22() cardinal set

Seg j is V22() j -element Element of K10(NAT)

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

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)

x is Relation-like Function-like set

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)

z is Relation-like NAT -defined Function-like V22() FinSequence-like FinSubsequence-like set

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

x is Relation-like NAT -defined (A,f) -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of (A,f)

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

dom o is functional FinSequence-membered set

y is Relation-like NAT -defined (A,f) -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of (A,f)

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

dom o is functional FinSequence-membered set

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

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

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

0 .--> the carrier of A is Relation-like NAT -defined {0} -defined Function-like one-to-one set

{0} --> the carrier of A is non empty Relation-like non-empty non empty-yielding {0} -defined { the carrier of A} -valued Function-like constant total quasi_total Element of K10(K11({0},{ the carrier of A}))

{ the carrier of A} is non empty trivial 1 -element set

K11({0},{ the carrier of A}) is Relation-like set

K10(K11({0},{ 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

signature A is Relation-like NAT -defined NAT -valued Function-like V22() FinSequence-like FinSubsequence-like FinSequence of NAT

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

K11((dom (signature A)),({0} *)) is Relation-like set

K10(K11((dom (signature A)),({0} *))) is set

(*--> 0) * (signature A) is Relation-like NAT -defined {0} * -valued Function-like Function-yielding V42() Element of K10(K11(NAT,({0} *)))

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

f is Relation-like dom (signature A) -defined {0} * -valued Function-like total quasi_total Function-yielding V42() Element of K10(K11((dom (signature A)),({0} *)))

z is Relation-like Function-like Element of {0}

(dom (signature A)) --> z is Relation-like dom (signature A) -defined {0} -valued Function-like constant total quasi_total Function-yielding V42() Element of K10(K11((dom (signature A)),{0}))

K11((dom (signature A)),{0}) is Relation-like set

K10(K11((dom (signature A)),{0})) is set

{z} is non empty trivial functional 1 -element set

K11((dom (signature A)),{z}) is Relation-like set

({0},(dom (signature A)),f,((dom (signature A)) --> 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