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