:: ALG_1 semantic presentation

NAT is non empty V35() V36() V37() V42() V47() V48() Element of K10(REAL)
REAL is set
K10(REAL) is set
NAT is non empty V35() V36() V37() V42() V47() V48() set
K10(NAT) is V42() set
K10(NAT) is V42() set
K219() is non empty set
K133() is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain Element of NAT
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set
the empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain set
1 is non empty set
{K133(),1} is non empty set
2 is non empty set
3 is non empty set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
K10( the carrier of U1) is set
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
U2 is non empty Element of K10( the carrier of U1)
Opers (U1,U2) is Relation-like NAT -defined PFuncs ((U2 *),U2) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((U2 *),U2)
U2 * is non empty functional FinSequence-membered FinSequenceSet of U2
PFuncs ((U2 *),U2) is non empty functional set
dom (Opers (U1,U2)) is Element of K10(NAT)
dom the charact of U1 is non empty Element of K10(NAT)
f is V35() V36() V37() V41() V42() V47() set
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
the charact of U1 . f is Relation-like Function-like homogeneous set
(Opers (U1,U2)) . f is Relation-like Function-like set
c₄ is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
c₄ /. U2 is non empty Relation-like U2 * -defined U2 -valued Function-like homogeneous quasi_total Element of K10(K11((U2 *),U2))
K11((U2 *),U2) is Relation-like set
K10(K11((U2 *),U2)) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
<*> the carrier of U1 is empty Relation-like non-empty empty-yielding NAT -defined the carrier of U1 -valued Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of the carrier of U1
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
f * (<*> the carrier of U1) is empty Relation-like non-empty empty-yielding NAT -defined the carrier of U2 -valued Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of the carrier of U2
<*> the carrier of U2 is empty Relation-like non-empty empty-yielding NAT -defined the carrier of U2 -valued Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() V42() V47() V49( {} ) FinSequence-like FinSubsequence-like FinSequence-membered with_common_domain FinSequence of the carrier of U2
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))
K11( the carrier of U1, the carrier of U1) is Relation-like set
K10(K11( the carrier of U1, the carrier of U1)) is set
U2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
(id the carrier of U1) * U2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
dom ((id the carrier of U1) * U2) is Element of K10(NAT)
dom U2 is Element of K10(NAT)
c₄ is V35() V36() V37() V41() V42() V47() set
U2 . c₄ is set
u1 is Element of the carrier of U1
(id the carrier of U1) . u1 is Element of the carrier of U1
((id the carrier of U1) * U2) . c₄ is set
len ((id the carrier of U1) * U2) is V35() V36() V37() V41() V42() V47() Element of NAT
len U2 is V35() V36() V37() V41() V42() V47() Element of NAT
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty V91() quasi_total non-empty UAStr
the carrier of f is non empty set
K11( the carrier of U2, the carrier of f) is Relation-like set
K10(K11( the carrier of U2, the carrier of f)) is set
c₄ is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
u1 is non empty Relation-like the carrier of U2 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of f))
u1 * c₄ is non empty Relation-like the carrier of U1 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of f))
K11( the carrier of U1, the carrier of f) is Relation-like set
K10(K11( the carrier of U1, the carrier of f)) is set
u2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
c₄ * u2 is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
u1 * (c₄ * u2) is Relation-like NAT -defined the carrier of f -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of f
(u1 * c₄) * u2 is Relation-like NAT -defined the carrier of f -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of f
dom u2 is Element of K10(NAT)
len u2 is V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len u2) is V42() V49( len u2) Element of K10(NAT)
dom (u1 * (c₄ * u2)) is Element of K10(NAT)
dom (c₄ * u2) is Element of K10(NAT)
len ((u1 * c₄) * u2) is V35() V36() V37() V41() V42() V47() Element of NAT
dom ((u1 * c₄) * u2) is Element of K10(NAT)
F is V35() V36() V37() V41() V42() V47() set
(u1 * (c₄ * u2)) . F is set
(c₄ * u2) . F is set
u1 . ((c₄ * u2) . F) is set
u2 . F is set
c₄ . (u2 . F) is set
u1 . (c₄ . (u2 . F)) is set
(u1 * c₄) . (u2 . F) is set
((u1 * c₄) * u2) . F is set
len (u1 * (c₄ * u2)) is V35() V36() V37() V41() V42() V47() Element of NAT
len (c₄ * u2) is V35() V36() V37() V41() V42() V47() Element of NAT
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))
K11( the carrier of U1, the carrier of U1) is Relation-like set
K10(K11( the carrier of U1, the carrier of U1)) is set
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
dom the charact of U1 is non empty Element of K10(NAT)
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
U2 is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 . U2 is Relation-like Function-like homogeneous set
f is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
c₄ is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
dom f is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))
K10(( the carrier of U1 *)) is set
u2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
f . u2 is set
(id the carrier of U1) . (f . u2) is set
(id the carrier of U1) * u2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
c₄ . ((id the carrier of U1) * u2) is set
rng f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
F is Element of the carrier of U1
(id the carrier of U1) . F is Element of the carrier of U1
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty V91() quasi_total non-empty UAStr
the carrier of f is non empty set
K11( the carrier of U2, the carrier of f) is Relation-like set
K10(K11( the carrier of U2, the carrier of f)) is set
c₄ is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
u1 is non empty Relation-like the carrier of U2 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of f))
u1 * c₄ is non empty Relation-like the carrier of U1 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of f))
K11( the carrier of U1, the carrier of f) is Relation-like set
K10(K11( the carrier of U1, the carrier of f)) is set
signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
signature U2 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
signature f is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
dom the charact of U1 is non empty Element of K10(NAT)
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
the carrier of f * is non empty functional FinSequence-membered FinSequenceSet of the carrier of f
Operations f is non empty PFuncsDomHQN of the carrier of f
the charact of f is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of f *), the carrier of f) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of f *), the carrier of f)
PFuncs (( the carrier of f *), the carrier of f) is non empty functional set
rng the charact of f is non empty V4() set
y is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 . y is Relation-like Function-like homogeneous set
the charact of f . y is Relation-like Function-like homogeneous set
y is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
dom y is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))
K10(( the carrier of U1 *)) is set
u is non empty Relation-like the carrier of f * -defined the carrier of f -valued Function-like homogeneous quasi_total Element of Operations f
a is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
y . a is set
(u1 * c₄) . (y . a) is set
(u1 * c₄) * a is Relation-like NAT -defined the carrier of f -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of f
u . ((u1 * c₄) * a) is set
the carrier of U2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2
c₄ * a is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
rng y is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
arity y is V35() V36() V37() V41() V42() V47() Element of NAT
(arity y) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 * : len b₁ = arity y } is set
len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
len (signature U2) is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U2 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U2 *), the carrier of U2) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U2 *), the carrier of U2)
PFuncs (( the carrier of U2 *), the carrier of U2) is non empty functional set
len the charact of U2 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
dom the charact of U2 is non empty Element of K10(NAT)
Seg (len the charact of U2) is non empty V42() V49( len the charact of U2) Element of K10(NAT)
Operations U2 is non empty PFuncsDomHQN of the carrier of U2
rng the charact of U2 is non empty V4() set
the charact of U2 . y is Relation-like Function-like homogeneous set
dom (signature U1) is Element of K10(NAT)
Seg (len (signature U1)) is V42() V49( len (signature U1)) Element of K10(NAT)
(signature U2) . y is set
b is non empty Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like homogeneous quasi_total Element of Operations U2
arity b is V35() V36() V37() V41() V42() V47() Element of NAT
(signature U1) . y is set
len (c₄ * a) is V35() V36() V37() V41() V42() V47() Element of NAT
b is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
len b is V35() V36() V37() V41() V42() V47() Element of NAT
dom b is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U2 *))
K10(( the carrier of U2 *)) is set
(arity b) -tuples_on the carrier of U2 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2
a is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U2 *
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U2 * : len b₁ = arity b } is set
b . (c₄ * a) is set
u1 . (b . (c₄ * a)) is set
u1 * (c₄ * a) is Relation-like NAT -defined the carrier of f -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of f
u . (u1 * (c₄ * a)) is set
c₄ . (y . a) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
rng f is non empty Element of K10( the carrier of U2)
K10( the carrier of U2) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
dom f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
rng f is non empty Element of K10( the carrier of U2)
K10( the carrier of U2) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
K11( the carrier of U2, the carrier of U1) is Relation-like set
K10(K11( the carrier of U2, the carrier of U1)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
f " is Relation-like Function-like set
c₄ is non empty Relation-like the carrier of U2 -defined the carrier of U1 -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of U1))
signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
signature U2 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
dom the charact of U1 is non empty Element of K10(NAT)
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
dom (signature U2) is Element of K10(NAT)
len (signature U2) is V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len (signature U2)) is V42() V49( len (signature U2)) Element of K10(NAT)
the charact of U2 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U2 *), the carrier of U2) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U2 *), the carrier of U2)
the carrier of U2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2
PFuncs (( the carrier of U2 *), the carrier of U2) is non empty functional set
len the charact of U2 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
dom the charact of U2 is non empty Element of K10(NAT)
Seg (len the charact of U2) is non empty V42() V49( len the charact of U2) Element of K10(NAT)
rng f is non empty Element of K10( the carrier of U2)
K10( the carrier of U2) is set
u1 is V35() V36() V37() V41() V42() V47() Element of NAT
Operations U2 is non empty PFuncsDomHQN of the carrier of U2
rng the charact of U2 is non empty V4() set
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
u2 is non empty Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like homogeneous quasi_total Element of Operations U2
the charact of U2 . u1 is Relation-like Function-like homogeneous set
F is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
the charact of U1 . u1 is Relation-like Function-like homogeneous set
x is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
dom x is Element of K10(NAT)
len x is V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len x) is V42() V49( len x) Element of K10(NAT)
y is V35() V36() V37() V41() V42() V47() set
x . y is set
dom f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
y is set
f . y is set
u is Element of the carrier of U1
f . u is set
y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
dom y is Element of K10(NAT)
f * y is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
dom (f * y) is Element of K10(NAT)
y is V35() V36() V37() V41() V42() V47() set
x . y is set
y . y is set
f . (y . y) is set
(f * y) . y is set
len y is V35() V36() V37() V41() V42() V47() Element of NAT
dom u2 is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U2 *))
K10(( the carrier of U2 *)) is set
arity u2 is V35() V36() V37() V41() V42() V47() Element of NAT
(arity u2) -tuples_on the carrier of U2 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U2 * : len b₁ = arity u2 } is set
c₄ * f is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U1))
K11( the carrier of U1, the carrier of U1) is Relation-like set
K10(K11( the carrier of U1, the carrier of U1)) is set
dom f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
id (dom f) is non empty Relation-like dom f -defined dom f -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11((dom f),(dom f)))
K11((dom f),(dom f)) is Relation-like set
K10(K11((dom f),(dom f))) is set
id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))
c₄ * x is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
(id the carrier of U1) * y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
(signature U1) . u1 is set
arity F is V35() V36() V37() V41() V42() V47() Element of NAT
(signature U2) . u1 is set
y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 * : len b₁ = arity F } is set
u is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U2 *
len u is V35() V36() V37() V41() V42() V47() Element of NAT
(arity F) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
dom F is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))
K10(( the carrier of U1 *)) is set
u2 . x is set
c₄ . (u2 . x) is set
F . y is set
f . (F . y) is set
c₄ . (f . (F . y)) is set
(id the carrier of U1) . (F . y) is set
F . (c₄ * x) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
K11( the carrier of U2, the carrier of U1) is Relation-like set
K10(K11( the carrier of U2, the carrier of U1)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
f " is Relation-like Function-like set
c₄ is non empty Relation-like the carrier of U2 -defined the carrier of U1 -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of U1))
rng c₄ is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
dom f is non empty Element of K10( the carrier of U1)
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty V91() quasi_total non-empty UAStr
the carrier of f is non empty set
K11( the carrier of U2, the carrier of f) is Relation-like set
K10(K11( the carrier of U2, the carrier of f)) is set
c₄ is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
u1 is non empty Relation-like the carrier of U2 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of f))
u1 * c₄ is non empty Relation-like the carrier of U1 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of f))
K11( the carrier of U1, the carrier of f) is Relation-like set
K10(K11( the carrier of U1, the carrier of f)) is set
dom u1 is non empty Element of K10( the carrier of U2)
K10( the carrier of U2) is set
rng c₄ is non empty Element of K10( the carrier of U2)
rng (u1 * c₄) is non empty Element of K10( the carrier of f)
K10( the carrier of f) is set
rng u1 is non empty Element of K10( the carrier of f)
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))
K11( the carrier of U1, the carrier of U1) is Relation-like set
K10(K11( the carrier of U1, the carrier of U1)) is set
rng (id the carrier of U1) is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
U1 is non empty V91() quasi_total non-empty UAStr
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
f " is Relation-like Function-like set
rng (f ") is set
dom f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
dom (f ") is set
rng f is non empty Element of K10( the carrier of U2)
K10( the carrier of U2) is set
K11( the carrier of U2, the carrier of U1) is Relation-like set
K10(K11( the carrier of U2, the carrier of U1)) is set
c₄ is non empty Relation-like the carrier of U2 -defined the carrier of U1 -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of U1))
U1 is non empty V91() quasi_total non-empty UAStr
U2 is non empty V91() quasi_total non-empty UAStr
f is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
c₄ is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
the carrier of f is non empty set
K11( the carrier of U2, the carrier of f) is Relation-like set
K10(K11( the carrier of U2, the carrier of f)) is set
u1 is non empty Relation-like the carrier of U2 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U2, the carrier of f))
u1 * c₄ is non empty Relation-like the carrier of U1 -defined the carrier of f -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of f))
K11( the carrier of U1, the carrier of f) is Relation-like set
K10(K11( the carrier of U1, the carrier of f)) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
f .: the carrier of U1 is Element of K10( the carrier of U2)
K10( the carrier of U2) is set
dom f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
c₄ is non empty Element of K10( the carrier of U2)
UniAlgSetClosed c₄ is non empty strict V91() quasi_total non-empty SubAlgebra of U2
u1 is non empty strict V91() quasi_total non-empty SubAlgebra of U2
the carrier of u1 is non empty set
the carrier of U2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2
Operations U2 is non empty PFuncsDomHQN of the carrier of U2
the charact of U2 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U2 *), the carrier of U2) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U2 *), the carrier of U2)
PFuncs (( the carrier of U2 *), the carrier of U2) is non empty functional set
rng the charact of U2 is non empty V4() set
u2 is non empty Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like homogeneous quasi_total Element of Operations U2
dom the charact of U2 is non empty Element of K10(NAT)
F is V35() V36() V37() V41() V42() V47() set
the charact of U2 . F is Relation-like Function-like homogeneous set
x is Relation-like NAT -defined c₄ -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of c₄
len x is V35() V36() V37() V41() V42() V47() Element of NAT
arity u2 is V35() V36() V37() V41() V42() V47() Element of NAT
u2 . x is set
dom x is Element of K10(NAT)
y is set
x . y is set
y is V35() V36() V37() V41() V42() V47() Element of NAT
x . y is set
u is set
f . u is set
y is Relation-like Function-like set
dom y is set
rng y is set
Seg (len x) is V42() V49( len x) Element of K10(NAT)
y is Relation-like NAT -defined Function-like V42() FinSequence-like FinSubsequence-like set
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
u is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
a is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
len a is V35() V36() V37() V41() V42() V47() Element of NAT
signature U2 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature U2) is Element of K10(NAT)
len (signature U2) is V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len (signature U2)) is V42() V49( len (signature U2)) Element of K10(NAT)
signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
dom (signature U1) is Element of K10(NAT)
len the charact of U2 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len the charact of U2) is non empty V42() V49( len the charact of U2) Element of K10(NAT)
(signature U2) . F is set
f * a is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
len (f * a) is V35() V36() V37() V41() V42() V47() Element of NAT
dom (f * a) is Element of K10(NAT)
Seg (len (f * a)) is V42() V49( len (f * a)) Element of K10(NAT)
Seg (len a) is V42() V49( len a) Element of K10(NAT)
a is V35() V36() V37() V41() V42() V47() set
a . a is set
f . (a . a) is set
x . a is set
(f * a) . a is set
len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len (signature U1)) is V42() V49( len (signature U1)) Element of K10(NAT)
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
dom the charact of U1 is non empty Element of K10(NAT)
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
the charact of U1 . F is Relation-like Function-like homogeneous set
(signature U1) . F is set
a is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
arity a is V35() V36() V37() V41() V42() V47() Element of NAT
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 * : len b₁ = arity a } is set
(arity a) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
dom a is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))
K10(( the carrier of U1 *)) is set
a . a is set
rng a is non empty Element of K10( the carrier of U1)
f . (a . a) is set
u2 . (f * a) is set
Opers (U2,c₄) is Relation-like NAT -defined PFuncs ((c₄ *),c₄) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((c₄ *),c₄)
c₄ * is non empty functional FinSequence-membered FinSequenceSet of c₄
PFuncs ((c₄ *),c₄) is non empty functional set
UAStr(# c₄,(Opers (U2,c₄)) #) is non empty strict UAStr
c₄ is non empty strict V91() quasi_total non-empty SubAlgebra of U2
the carrier of c₄ is non empty set
u1 is non empty strict V91() quasi_total non-empty SubAlgebra of U2
the carrier of u1 is non empty set
the charact of c₄ is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of c₄ *), the carrier of c₄) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of c₄ *), the carrier of c₄)
the carrier of c₄ * is non empty functional FinSequence-membered FinSequenceSet of the carrier of c₄
PFuncs (( the carrier of c₄ *), the carrier of c₄) is non empty functional set
u2 is non empty Element of K10( the carrier of U2)
Opers (U2,u2) is Relation-like NAT -defined PFuncs ((u2 *),u2) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((u2 *),u2)
u2 * is non empty functional FinSequence-membered FinSequenceSet of u2
PFuncs ((u2 *),u2) is non empty functional set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
rng f is non empty Element of K10( the carrier of U2)
K10( the carrier of U2) is set
(U1,U2,f) is non empty strict V91() quasi_total non-empty SubAlgebra of U2
the carrier of (U1,U2,f) is non empty set
dom f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
f .: the carrier of U1 is Element of K10( the carrier of U2)
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty strict V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
(U1,U2,f) is non empty strict V91() quasi_total non-empty SubAlgebra of U2
K10( the carrier of U2) is set
the carrier of (U1,U2,f) is non empty set
rng f is non empty Element of K10( the carrier of U2)
dom f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
f .: (dom f) is Element of K10( the carrier of U2)
f .: the carrier of U1 is Element of K10( the carrier of U2)
the charact of (U1,U2,f) is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of (U1,U2,f) *), the carrier of (U1,U2,f)) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (U1,U2,f) *), the carrier of (U1,U2,f))
the carrier of (U1,U2,f) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (U1,U2,f)
PFuncs (( the carrier of (U1,U2,f) *), the carrier of (U1,U2,f)) is non empty functional set
c₄ is non empty Element of K10( the carrier of U2)
Opers (U2,c₄) is Relation-like NAT -defined PFuncs ((c₄ *),c₄) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs ((c₄ *),c₄)
c₄ * is non empty functional FinSequence-membered FinSequenceSet of c₄
PFuncs ((c₄ *),c₄) is non empty functional set
f .: the carrier of U1 is Element of K10( the carrier of U2)
K10( the carrier of U2) is set
dom f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
f .: (dom f) is Element of K10( the carrier of U2)
rng f is non empty Element of K10( the carrier of U2)
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
K11( the carrier of U1, the carrier of U1) is Relation-like set
K10(K11( the carrier of U1, the carrier of U1)) is set
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
rng the charact of U1 is non empty V4() set
dom the charact of U1 is non empty Element of K10(NAT)
id the carrier of U1 is non empty Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11( the carrier of U1, the carrier of U1))
U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total Element of K10(K11( the carrier of U1, the carrier of U1))
ExtendRel U2 is Relation-like the carrier of U1 * -defined the carrier of U1 * -valued Element of K10(K11(( the carrier of U1 *),( the carrier of U1 *)))
K11(( the carrier of U1 *),( the carrier of U1 *)) is Relation-like set
K10(K11(( the carrier of U1 *),( the carrier of U1 *))) is set
f is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 . f is Relation-like Function-like homogeneous set
c₄ is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
dom c₄ is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))
K10(( the carrier of U1 *)) is set
u1 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
u2 is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
[u1,u2] is set
{u1,u2} is non empty functional set
{u1} is non empty V2() functional V49(1) set
{{u1,u2},{u1}} is non empty set
c₄ . u1 is set
c₄ . u2 is set
[(c₄ . u1),(c₄ . u2)] is set
{(c₄ . u1),(c₄ . u2)} is non empty set
{(c₄ . u1)} is non empty V2() V49(1) set
{{(c₄ . u1),(c₄ . u2)},{(c₄ . u1)}} is non empty set
id ( the carrier of U1 *) is non empty Relation-like the carrier of U1 * -defined the carrier of U1 * -valued reflexive symmetric antisymmetric transitive Function-like one-to-one total quasi_total onto bijective Element of K10(K11(( the carrier of U1 *),( the carrier of U1 *)))
rng c₄ is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
rng the charact of U1 is non empty V4() set
U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
Class U2 is non empty V4() a_partition of the carrier of U1
(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2
K11(((Class U2) *),(Class U2)) is Relation-like set
K10(K11(((Class U2) *),(Class U2))) is set
f is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
arity f is V35() V36() V37() V41() V42() V47() Element of NAT
(arity f) -tuples_on (Class U2) is non empty functional FinSequence-membered FinSequenceSet of Class U2
u1 is set
dom f is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))
K10(( the carrier of U1 *)) is set
(arity f) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 * : len b₁ = arity f } is set
{ b₁ where b₁ is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) * : len b₁ = arity f } is set
u2 is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *
len u2 is V35() V36() V37() V41() V42() V47() Element of NAT
F is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
K10( the carrier of U1) is set
f . F is set
Class (U2,(f . F)) is Element of K10( the carrier of U1)
x is Element of K10( the carrier of U1)
len F is V35() V36() V37() V41() V42() V47() Element of NAT
rng f is non empty Element of K10( the carrier of U1)
y is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2
y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
f . y is set
Class (U2,(f . y)) is Element of K10( the carrier of U1)
len y is V35() V36() V37() V41() V42() V47() Element of NAT
dom F is Element of K10(NAT)
u is V35() V36() V37() V41() V42() V47() Element of NAT
F . u is set
y . u is set
[(F . u),(y . u)] is set
{(F . u),(y . u)} is non empty set
{(F . u)} is non empty V2() V49(1) set
{{(F . u),(y . u)},{(F . u)}} is non empty set
Class (U2,(F . u)) is Element of K10( the carrier of U1)
u2 . u is set
rng F is Element of K10( the carrier of U1)
Seg (arity f) is V42() V49( arity f) Element of K10(NAT)
dom y is Element of K10(NAT)
Class (U2,(y . u)) is Element of K10( the carrier of U1)
[F,y] is set
{F,y} is non empty functional set
{F} is non empty V2() functional V49(1) set
{{F,y},{F}} is non empty set
ExtendRel U2 is Relation-like the carrier of U1 * -defined the carrier of U1 * -valued Element of K10(K11(( the carrier of U1 *),( the carrier of U1 *)))
K11(( the carrier of U1 *),( the carrier of U1 *)) is Relation-like set
K10(K11(( the carrier of U1 *),( the carrier of U1 *))) is set
dom the charact of U1 is non empty Element of K10(NAT)
[(f . F),(f . y)] is set
{(f . F),(f . y)} is non empty set
{(f . F)} is non empty V2() V49(1) set
{{(f . F),(f . y)},{(f . F)}} is non empty set
u is V35() V36() V37() V41() V42() V47() set
the charact of U1 . u is Relation-like Function-like homogeneous set
u1 is Relation-like Function-like set
dom u1 is set
rng u1 is set
{ (b₁ -tuples_on (Class U2)) where b₁ is V35() V36() V37() V41() V42() V47() Element of NAT : verum } is set
union { (b₁ -tuples_on (Class U2)) where b₁ is V35() V36() V37() V41() V42() V47() Element of NAT : verum } is set
u2 is Relation-like (Class U2) * -defined Class U2 -valued Function-like Element of K10(K11(((Class U2) *),(Class U2)))
dom u2 is functional FinSequence-membered Element of K10(((Class U2) *))
K10(((Class U2) *)) is set
{ b₁ where b₁ is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) * : len b₁ = arity f } is set
F is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2
len F is V35() V36() V37() V41() V42() V47() Element of NAT
x is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2
len x is V35() V36() V37() V41() V42() V47() Element of NAT
y is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *
len y is V35() V36() V37() V41() V42() V47() Element of NAT
the Relation-like NAT -defined Class U2 -valued Function-like V42() V49( arity f) FinSequence-like FinSubsequence-like Element of (arity f) -tuples_on (Class U2) is Relation-like NAT -defined Class U2 -valued Function-like V42() V49( arity f) FinSequence-like FinSubsequence-like Element of (arity f) -tuples_on (Class U2)
F is Relation-like NAT -defined Function-like V42() FinSequence-like FinSubsequence-like set
x is Relation-like NAT -defined Function-like V42() FinSequence-like FinSubsequence-like set
len F is V35() V36() V37() V41() V42() V47() Element of NAT
len x is V35() V36() V37() V41() V42() V47() Element of NAT
y is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *
len y is V35() V36() V37() V41() V42() V47() Element of NAT
y is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *
len y is V35() V36() V37() V41() V42() V47() Element of NAT
x is Relation-like NAT -defined Function-like V42() FinSequence-like FinSubsequence-like set
F is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
dom F is non empty functional FinSequence-membered with_common_domain Element of K10(((Class U2) *))
x is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2
F . x is set
y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
f . y is set
Class (U2,(f . y)) is Element of K10( the carrier of U1)
K10( the carrier of U1) is set
c₄ is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
dom c₄ is non empty functional FinSequence-membered with_common_domain Element of K10(((Class U2) *))
K10(((Class U2) *)) is set
u1 is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
dom u1 is non empty functional FinSequence-membered with_common_domain Element of K10(((Class U2) *))
u2 is set
c₄ . u2 is set
u1 . u2 is set
F is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2
x is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
c₄ . F is set
f . x is set
Class (U2,(f . x)) is Element of K10( the carrier of U1)
K10( the carrier of U1) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
Class U2 is non empty V4() a_partition of the carrier of U1
(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2
PFuncs (((Class U2) *),(Class U2)) is non empty functional set
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
f is V35() V36() V37() V41() V42() V47() set
the charact of U1 . f is Relation-like Function-like homogeneous set
dom the charact of U1 is non empty Element of K10(NAT)
c₄ is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,U2,c₄) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
K11(((Class U2) *),(Class U2)) is Relation-like set
K10(K11(((Class U2) *),(Class U2))) is set
u1 is Relation-like Function-like Element of PFuncs (((Class U2) *),(Class U2))
u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
f is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))
dom f is Element of K10(NAT)
c₄ is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))
len c₄ is V35() V36() V37() V41() V42() V47() Element of NAT
dom c₄ is Element of K10(NAT)
u1 is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 . u1 is Relation-like Function-like homogeneous set
c₄ . u1 is Relation-like Function-like set
u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
K11(((Class U2) *),(Class U2)) is Relation-like set
K10(K11(((Class U2) *),(Class U2))) is set
f is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))
len f is V35() V36() V37() V41() V42() V47() Element of NAT
dom f is Element of K10(NAT)
c₄ is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))
len c₄ is V35() V36() V37() V41() V42() V47() Element of NAT
dom c₄ is Element of K10(NAT)
u1 is V35() V36() V37() V41() V42() V47() set
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
dom the charact of U1 is non empty Element of K10(NAT)
the charact of U1 . u1 is Relation-like Function-like homogeneous set
f . u1 is Relation-like Function-like set
u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
K11(((Class U2) *),(Class U2)) is Relation-like set
K10(K11(((Class U2) *),(Class U2))) is set
c₄ . u1 is Relation-like Function-like set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
Class U2 is non empty V4() a_partition of the carrier of U1
(U1,U2) is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))
(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2
PFuncs (((Class U2) *),(Class U2)) is non empty functional set
UAStr(# (Class U2),(U1,U2) #) is non empty strict UAStr
K11(((Class U2) *),(Class U2)) is Relation-like set
K10(K11(((Class U2) *),(Class U2))) is set
dom (U1,U2) is Element of K10(NAT)
c₄ is V35() V36() V37() V41() V42() V47() set
(U1,U2) . c₄ is Relation-like Function-like set
u1 is Relation-like (Class U2) * -defined Class U2 -valued Function-like Element of K10(K11(((Class U2) *),(Class U2)))
len (U1,U2) is V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len (U1,U2)) is V42() V49( len (U1,U2)) Element of K10(NAT)
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
dom the charact of U1 is non empty Element of K10(NAT)
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
the charact of U1 . c₄ is Relation-like Function-like homogeneous set
u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
the carrier of UAStr(# (Class U2),(U1,U2) #) is non empty set
the charact of UAStr(# (Class U2),(U1,U2) #) is Relation-like NAT -defined PFuncs (( the carrier of UAStr(# (Class U2),(U1,U2) #) *), the carrier of UAStr(# (Class U2),(U1,U2) #)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (( the carrier of UAStr(# (Class U2),(U1,U2) #) *), the carrier of UAStr(# (Class U2),(U1,U2) #))
the carrier of UAStr(# (Class U2),(U1,U2) #) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of UAStr(# (Class U2),(U1,U2) #)
PFuncs (( the carrier of UAStr(# (Class U2),(U1,U2) #) *), the carrier of UAStr(# (Class U2),(U1,U2) #)) is non empty functional set
c₄ is V35() V36() V37() V41() V42() V47() set
(U1,U2) . c₄ is Relation-like Function-like set
u1 is Relation-like (Class U2) * -defined Class U2 -valued Function-like Element of K10(K11(((Class U2) *),(Class U2)))
len (U1,U2) is V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len (U1,U2)) is V42() V49( len (U1,U2)) Element of K10(NAT)
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
dom the charact of U1 is non empty Element of K10(NAT)
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
the charact of U1 . c₄ is Relation-like Function-like homogeneous set
u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
c₄ is set
(U1,U2) . c₄ is Relation-like Function-like set
len (U1,U2) is V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len (U1,U2)) is V42() V49( len (U1,U2)) Element of K10(NAT)
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
dom the charact of U1 is non empty Element of K10(NAT)
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
u1 is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 . u1 is Relation-like Function-like homogeneous set
(U1,U2) . u1 is Relation-like Function-like set
u2 is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,U2,u2) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
len the charact of UAStr(# (Class U2),(U1,U2) #) is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
(U1,U2) is non empty strict V91() quasi_total non-empty UAStr
Class U2 is non empty V4() a_partition of the carrier of U1
(U1,U2) is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))
(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2
PFuncs (((Class U2) *),(Class U2)) is non empty functional set
UAStr(# (Class U2),(U1,U2) #) is non empty strict UAStr
the carrier of (U1,U2) is non empty set
K11( the carrier of U1, the carrier of (U1,U2)) is Relation-like set
K10(K11( the carrier of U1, the carrier of (U1,U2))) is set
f is Element of the carrier of U1
Class (U2,f) is Element of K10( the carrier of U1)
K10( the carrier of U1) is set
c₄ is Element of the carrier of (U1,U2)
f is non empty Relation-like the carrier of U1 -defined the carrier of (U1,U2) -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of (U1,U2)))
c₄ is Element of the carrier of U1
f . c₄ is Element of the carrier of (U1,U2)
Class (U2,c₄) is Element of K10( the carrier of U1)
K10( the carrier of U1) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of (U1,U2) -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of (U1,U2)))
c₄ is non empty Relation-like the carrier of U1 -defined the carrier of (U1,U2) -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of (U1,U2)))
u1 is Element of the carrier of U1
f . u1 is Element of the carrier of (U1,U2)
Class (U2,u1) is Element of K10( the carrier of U1)
K10( the carrier of U1) is set
c₄ . u1 is Element of the carrier of (U1,U2)
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
(U1,U2) is non empty strict V91() quasi_total non-empty UAStr
Class U2 is non empty V4() a_partition of the carrier of U1
(U1,U2) is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))
(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2
PFuncs (((Class U2) *),(Class U2)) is non empty functional set
UAStr(# (Class U2),(U1,U2) #) is non empty strict UAStr
(U1,U2) is non empty Relation-like the carrier of U1 -defined the carrier of (U1,U2) -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of (U1,U2)))
the carrier of (U1,U2) is non empty set
K11( the carrier of U1, the carrier of (U1,U2)) is Relation-like set
K10(K11( the carrier of U1, the carrier of (U1,U2))) is set
signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
dom (signature U1) is Element of K10(NAT)
Seg (len (signature U1)) is V42() V49( len (signature U1)) Element of K10(NAT)
len (U1,U2) is V35() V36() V37() V41() V42() V47() Element of NAT
signature (U1,U2) is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
len (signature (U1,U2)) is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of (U1,U2) is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of (U1,U2) *), the carrier of (U1,U2)) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (U1,U2) *), the carrier of (U1,U2))
the carrier of (U1,U2) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (U1,U2)
PFuncs (( the carrier of (U1,U2) *), the carrier of (U1,U2)) is non empty functional set
len the charact of (U1,U2) is non empty V35() V36() V37() V41() V42() V47() Element of NAT
u2 is V35() V36() V37() V41() V42() V47() set
dom the charact of U1 is non empty Element of K10(NAT)
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
the charact of U1 . u2 is Relation-like Function-like homogeneous set
dom (U1,U2) is Element of K10(NAT)
(U1,U2) . u2 is Relation-like Function-like set
F is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
(U1,U2,F) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
K11(((Class U2) *),(Class U2)) is Relation-like set
K10(K11(((Class U2) *),(Class U2))) is set
K11(( the carrier of (U1,U2) *), the carrier of (U1,U2)) is Relation-like set
K10(K11(( the carrier of (U1,U2) *), the carrier of (U1,U2))) is set
x is non empty Relation-like the carrier of (U1,U2) * -defined the carrier of (U1,U2) -valued Function-like homogeneous quasi_total Element of K10(K11(( the carrier of (U1,U2) *), the carrier of (U1,U2)))
dom x is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of (U1,U2) *))
K10(( the carrier of (U1,U2) *)) is set
y is set
dom (U1,U2,F) is non empty functional FinSequence-membered with_common_domain Element of K10(((Class U2) *))
K10(((Class U2) *)) is set
arity F is V35() V36() V37() V41() V42() V47() Element of NAT
(arity F) -tuples_on (Class U2) is non empty functional FinSequence-membered FinSequenceSet of Class U2
y is Relation-like NAT -defined the carrier of (U1,U2) -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of (U1,U2) *
{ b₁ where b₁ is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) * : len b₁ = arity F } is set
arity x is V35() V36() V37() V41() V42() V47() Element of NAT
u is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *
len u is V35() V36() V37() V41() V42() V47() Element of NAT
dom (signature (U1,U2)) is Element of K10(NAT)
(signature U1) . u2 is set
(signature (U1,U2)) . u2 is set
Operations (U1,U2) is non empty PFuncsDomHQN of the carrier of (U1,U2)
rng the charact of (U1,U2) is non empty V4() set
u2 is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 . u2 is Relation-like Function-like homogeneous set
the charact of (U1,U2) . u2 is Relation-like Function-like homogeneous set
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
F is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
dom F is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))
K10(( the carrier of U1 *)) is set
x is non empty Relation-like the carrier of (U1,U2) * -defined the carrier of (U1,U2) -valued Function-like homogeneous quasi_total Element of Operations (U1,U2)
(U1,U2,F) is non empty Relation-like (Class U2) * -defined Class U2 -valued Function-like homogeneous quasi_total Element of K10(K11(((Class U2) *),(Class U2)))
y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
F . y is set
(U1,U2) . (F . y) is set
(U1,U2) * y is Relation-like NAT -defined the carrier of (U1,U2) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of (U1,U2)
x . ((U1,U2) * y) is set
u is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class U2
len ((U1,U2) * y) is V35() V36() V37() V41() V42() V47() Element of NAT
len y is V35() V36() V37() V41() V42() V47() Element of NAT
a is V35() V36() V37() V41() V42() V47() Element of NAT
dom y is Element of K10(NAT)
dom ((U1,U2) * y) is Element of K10(NAT)
y . a is set
rng y is Element of K10( the carrier of U1)
K10( the carrier of U1) is set
Class (U2,(y . a)) is Element of K10( the carrier of U1)
b is Element of the carrier of U1
(U1,U2) . b is Element of the carrier of (U1,U2)
a is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) *
a . a is set
rng F is non empty Element of K10( the carrier of U1)
arity F is V35() V36() V37() V41() V42() V47() Element of NAT
(arity F) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 * : len b₁ = arity F } is set
y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
a is Element of the carrier of U1
Class (U2,a) is Element of K10( the carrier of U1)
Class (U2,(F . y)) is Element of K10( the carrier of U1)
dom (U1,U2,F) is non empty functional FinSequence-membered with_common_domain Element of K10(((Class U2) *))
(arity F) -tuples_on (Class U2) is non empty functional FinSequence-membered FinSequenceSet of Class U2
{ b₁ where b₁ is Relation-like NAT -defined Class U2 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class U2) * : len b₁ = arity F } is set
b is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
len b is V35() V36() V37() V41() V42() V47() Element of NAT
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
(U1,U2) is non empty strict V91() quasi_total non-empty UAStr
Class U2 is non empty V4() a_partition of the carrier of U1
(U1,U2) is Relation-like NAT -defined PFuncs (((Class U2) *),(Class U2)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class U2) *),(Class U2))
(Class U2) * is non empty functional FinSequence-membered FinSequenceSet of Class U2
PFuncs (((Class U2) *),(Class U2)) is non empty functional set
UAStr(# (Class U2),(U1,U2) #) is non empty strict UAStr
(U1,U2) is non empty Relation-like the carrier of U1 -defined the carrier of (U1,U2) -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of (U1,U2)))
the carrier of (U1,U2) is non empty set
K11( the carrier of U1, the carrier of (U1,U2)) is Relation-like set
K10(K11( the carrier of U1, the carrier of (U1,U2))) is set
rng (U1,U2) is non empty Element of K10( the carrier of (U1,U2))
K10( the carrier of (U1,U2)) is set
F is set
K10( the carrier of U1) is set
x is Element of K10( the carrier of U1)
y is set
Class (U2,y) is Element of K10( the carrier of U1)
dom (U1,U2) is non empty Element of K10( the carrier of U1)
y is Element of the carrier of U1
(U1,U2) . y is Element of the carrier of (U1,U2)
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
K11( the carrier of U1, the carrier of U1) is Relation-like set
K10(K11( the carrier of U1, the carrier of U1)) is set
u1 is Relation-like the carrier of U1 -defined the carrier of U1 -valued Element of K10(K11( the carrier of U1, the carrier of U1))
u2 is set
[u2,u2] is set
{u2,u2} is non empty set
{u2} is non empty V2() V49(1) set
{{u2,u2},{u2}} is non empty set
F is Element of the carrier of U1
f . F is Element of the carrier of U2
dom u1 is Element of K10( the carrier of U1)
K10( the carrier of U1) is set
field u1 is set
u2 is set
F is set
x is set
[u2,F] is set
{u2,F} is non empty set
{u2} is non empty V2() V49(1) set
{{u2,F},{u2}} is non empty set
[F,x] is set
{F,x} is non empty set
{F} is non empty V2() V49(1) set
{{F,x},{F}} is non empty set
[u2,x] is set
{u2,x} is non empty set
{{u2,x},{u2}} is non empty set
y is Element of the carrier of U1
f . y is Element of the carrier of U2
y is Element of the carrier of U1
f . y is Element of the carrier of U2
u is Element of the carrier of U1
f . u is Element of the carrier of U2
u2 is set
F is set
[u2,F] is set
{u2,F} is non empty set
{u2} is non empty V2() V49(1) set
{{u2,F},{u2}} is non empty set
[F,u2] is set
{F,u2} is non empty set
{F} is non empty V2() V49(1) set
{{F,u2},{F}} is non empty set
x is Element of the carrier of U1
f . x is Element of the carrier of U2
y is Element of the carrier of U1
f . y is Element of the carrier of U2
signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
signature U2 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
rng the charact of U1 is non empty V4() set
F is V35() V36() V37() V41() V42() V47() Element of NAT
dom the charact of U1 is non empty Element of K10(NAT)
x is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
the charact of U1 . F is Relation-like Function-like homogeneous set
len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
len (signature U2) is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U2 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U2 *), the carrier of U2) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U2 *), the carrier of U2)
the carrier of U2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2
PFuncs (( the carrier of U2 *), the carrier of U2) is non empty functional set
len the charact of U2 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
dom the charact of U2 is non empty Element of K10(NAT)
Operations U2 is non empty PFuncsDomHQN of the carrier of U2
rng the charact of U2 is non empty V4() set
the charact of U2 . F is Relation-like Function-like homogeneous set
y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
dom x is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))
K10(( the carrier of U1 *)) is set
u is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
[y,u] is set
{y,u} is non empty functional set
{y} is non empty V2() functional V49(1) set
{{y,u},{y}} is non empty set
u2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total Element of K10(K11( the carrier of U1, the carrier of U1))
ExtendRel u2 is Relation-like the carrier of U1 * -defined the carrier of U1 * -valued Element of K10(K11(( the carrier of U1 *),( the carrier of U1 *)))
K11(( the carrier of U1 *),( the carrier of U1 *)) is Relation-like set
K10(K11(( the carrier of U1 *),( the carrier of U1 *))) is set
x . y is set
rng x is non empty Element of K10( the carrier of U1)
x . u is set
len y is V35() V36() V37() V41() V42() V47() Element of NAT
len u is V35() V36() V37() V41() V42() V47() Element of NAT
f * u is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
len (f * u) is V35() V36() V37() V41() V42() V47() Element of NAT
dom (f * u) is Element of K10(NAT)
Seg (len y) is V42() V49( len y) Element of K10(NAT)
f * y is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
len (f * y) is V35() V36() V37() V41() V42() V47() Element of NAT
b is V35() V36() V37() V41() V42() V47() set
dom u is Element of K10(NAT)
u . b is set
rng u is Element of K10( the carrier of U1)
dom y is Element of K10(NAT)
y . b is set
rng y is Element of K10( the carrier of U1)
[(y . b),(u . b)] is set
{(y . b),(u . b)} is non empty set
{(y . b)} is non empty V2() V49(1) set
{{(y . b),(u . b)},{(y . b)}} is non empty set
b is Element of the carrier of U1
f . b is Element of the carrier of U2
y is Element of the carrier of U1
f . y is Element of the carrier of U2
(f * u) . b is set
dom (f * y) is Element of K10(NAT)
(f * y) . b is set
f . (x . y) is set
y is non empty Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like homogeneous quasi_total Element of Operations U2
y . (f * y) is set
f . (x . u) is set
y . (f * u) is set
a is Element of the carrier of U1
f . a is Element of the carrier of U2
a is Element of the carrier of U1
f . a is Element of the carrier of U2
[(x . y),(x . u)] is set
{(x . y),(x . u)} is non empty set
{(x . y)} is non empty V2() V49(1) set
{{(x . y),(x . u)},{(x . y)}} is non empty set
F is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
x is Element of the carrier of U1
y is Element of the carrier of U1
[x,y] is set
{x,y} is non empty set
{x} is non empty V2() V49(1) set
{{x,y},{x}} is non empty set
f . x is Element of the carrier of U2
f . y is Element of the carrier of U2
u1 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
u2 is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
F is set
x is set
[F,x] is set
{F,x} is non empty set
{F} is non empty V2() V49(1) set
{{F,x},{F}} is non empty set
y is Element of the carrier of U1
f . y is Element of the carrier of U2
y is Element of the carrier of U1
f . y is Element of the carrier of U2
y is Element of the carrier of U1
f . y is Element of the carrier of U2
y is Element of the carrier of U1
f . y is Element of the carrier of U2
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
(U1,U2,f) is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
(U1,(U1,U2,f)) is non empty strict V91() quasi_total non-empty UAStr
Class (U1,U2,f) is non empty V4() a_partition of the carrier of U1
(U1,(U1,U2,f)) is Relation-like NAT -defined PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f))) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f)))
(Class (U1,U2,f)) * is non empty functional FinSequence-membered FinSequenceSet of Class (U1,U2,f)
PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f))) is non empty functional set
UAStr(# (Class (U1,U2,f)),(U1,(U1,U2,f)) #) is non empty strict UAStr
the carrier of (U1,(U1,U2,f)) is non empty set
K11( the carrier of (U1,(U1,U2,f)), the carrier of U2) is Relation-like set
K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2)) is set
x is set
K10( the carrier of U1) is set
y is Element of K10( the carrier of U1)
y is set
Class ((U1,U2,f),y) is Element of K10( the carrier of U1)
u is Element of the carrier of U1
f . u is Element of the carrier of U2
a is Element of the carrier of U2
a is Element of the carrier of U1
Class ((U1,U2,f),a) is Element of K10( the carrier of U1)
f . a is Element of the carrier of U2
Class ((U1,U2,f),u) is Element of K10( the carrier of U1)
[a,u] is set
{a,u} is non empty set
{a} is non empty V2() V49(1) set
{{a,u},{a}} is non empty set
x is Relation-like Function-like set
dom x is set
rng x is set
y is non empty Relation-like the carrier of (U1,(U1,U2,f)) -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2))
y is Element of the carrier of U1
Class ((U1,U2,f),y) is Element of K10( the carrier of U1)
K10( the carrier of U1) is set
y . (Class ((U1,U2,f),y)) is set
f . y is Element of the carrier of U2
F is non empty Relation-like the carrier of (U1,(U1,U2,f)) -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2))
x is non empty Relation-like the carrier of (U1,(U1,U2,f)) -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2))
y is Element of the carrier of (U1,(U1,U2,f))
F . y is set
x . y is set
K10( the carrier of U1) is set
y is Element of K10( the carrier of U1)
u is set
Class ((U1,U2,f),u) is Element of K10( the carrier of U1)
F . y is Element of the carrier of U2
f . u is set
x . y is Element of the carrier of U2
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
(U1,U2,f) is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
(U1,(U1,U2,f)) is non empty strict V91() quasi_total non-empty UAStr
Class (U1,U2,f) is non empty V4() a_partition of the carrier of U1
(U1,(U1,U2,f)) is Relation-like NAT -defined PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f))) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f)))
(Class (U1,U2,f)) * is non empty functional FinSequence-membered FinSequenceSet of Class (U1,U2,f)
PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f))) is non empty functional set
UAStr(# (Class (U1,U2,f)),(U1,(U1,U2,f)) #) is non empty strict UAStr
(U1,U2,f) is non empty Relation-like the carrier of (U1,(U1,U2,f)) -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2))
the carrier of (U1,(U1,U2,f)) is non empty set
K11( the carrier of (U1,(U1,U2,f)), the carrier of U2) is Relation-like set
K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2)) is set
(U1,(U1,U2,f)) is non empty Relation-like the carrier of U1 -defined the carrier of (U1,(U1,U2,f)) -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of (U1,(U1,U2,f))))
K11( the carrier of U1, the carrier of (U1,(U1,U2,f))) is Relation-like set
K10(K11( the carrier of U1, the carrier of (U1,(U1,U2,f)))) is set
signature U1 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
signature (U1,(U1,U2,f)) is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
signature U2 is Relation-like NAT -defined NAT -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of NAT
the charact of (U1,(U1,U2,f)) is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of (U1,(U1,U2,f)) *), the carrier of (U1,(U1,U2,f))) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of (U1,(U1,U2,f)) *), the carrier of (U1,(U1,U2,f)))
the carrier of (U1,(U1,U2,f)) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (U1,(U1,U2,f))
PFuncs (( the carrier of (U1,(U1,U2,f)) *), the carrier of (U1,(U1,U2,f))) is non empty functional set
dom the charact of (U1,(U1,U2,f)) is non empty Element of K10(NAT)
Operations (U1,(U1,U2,f)) is non empty PFuncsDomHQN of the carrier of (U1,(U1,U2,f))
rng the charact of (U1,(U1,U2,f)) is non empty V4() set
the carrier of U2 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U2
Operations U2 is non empty PFuncsDomHQN of the carrier of U2
the charact of U2 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U2 *), the carrier of U2) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U2 *), the carrier of U2)
PFuncs (( the carrier of U2 *), the carrier of U2) is non empty functional set
rng the charact of U2 is non empty V4() set
x is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of (U1,(U1,U2,f)) . x is Relation-like Function-like homogeneous set
the charact of U2 . x is Relation-like Function-like homogeneous set
len (signature U1) is V35() V36() V37() V41() V42() V47() Element of NAT
the charact of U1 is non empty Relation-like non-empty NAT -defined PFuncs (( the carrier of U1 *), the carrier of U1) -valued Function-like V33() V42() FinSequence-like FinSubsequence-like homogeneous quasi_total FinSequence of PFuncs (( the carrier of U1 *), the carrier of U1)
the carrier of U1 * is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
PFuncs (( the carrier of U1 *), the carrier of U1) is non empty functional set
len the charact of U1 is non empty V35() V36() V37() V41() V42() V47() Element of NAT
len (signature (U1,(U1,U2,f))) is V35() V36() V37() V41() V42() V47() Element of NAT
len the charact of (U1,(U1,U2,f)) is non empty V35() V36() V37() V41() V42() V47() Element of NAT
Seg (len the charact of (U1,(U1,U2,f))) is non empty V42() V49( len the charact of (U1,(U1,U2,f))) Element of K10(NAT)
dom the charact of U1 is non empty Element of K10(NAT)
Seg (len the charact of U1) is non empty V42() V49( len the charact of U1) Element of K10(NAT)
Operations U1 is non empty PFuncsDomHQN of the carrier of U1
rng the charact of U1 is non empty V4() set
the charact of U1 . x is Relation-like Function-like homogeneous set
y is non empty Relation-like the carrier of U1 * -defined the carrier of U1 -valued Function-like homogeneous quasi_total Element of Operations U1
dom y is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of U1 *))
K10(( the carrier of U1 *)) is set
arity y is V35() V36() V37() V41() V42() V47() Element of NAT
(arity y) -tuples_on the carrier of U1 is non empty functional FinSequence-membered FinSequenceSet of the carrier of U1
{ b₁ where b₁ is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 * : len b₁ = arity y } is set
y is non empty Relation-like the carrier of (U1,(U1,U2,f)) * -defined the carrier of (U1,(U1,U2,f)) -valued Function-like homogeneous quasi_total Element of Operations (U1,(U1,U2,f))
dom y is non empty functional FinSequence-membered with_common_domain Element of K10(( the carrier of (U1,(U1,U2,f)) *))
K10(( the carrier of (U1,(U1,U2,f)) *)) is set
u is non empty Relation-like the carrier of U2 * -defined the carrier of U2 -valued Function-like homogeneous quasi_total Element of Operations U2
a is Relation-like NAT -defined the carrier of (U1,(U1,U2,f)) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of (U1,(U1,U2,f))
y . a is set
(U1,U2,f) . (y . a) is set
(U1,U2,f) * a is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
u . ((U1,U2,f) * a) is set
a is Relation-like NAT -defined Class (U1,U2,f) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of Class (U1,U2,f)
b is Relation-like NAT -defined Class (U1,U2,f) -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class (U1,U2,f)) *
b is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U1
len b is V35() V36() V37() V41() V42() V47() Element of NAT
y is Relation-like NAT -defined the carrier of U1 -valued Function-like V42() FinSequence-like FinSubsequence-like Element of the carrier of U1 *
len y is V35() V36() V37() V41() V42() V47() Element of NAT
len ((U1,U2,f) * a) is V35() V36() V37() V41() V42() V47() Element of NAT
f * y is Relation-like NAT -defined the carrier of U2 -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of the carrier of U2
len (f * y) is V35() V36() V37() V41() V42() V47() Element of NAT
o1y is V35() V36() V37() V41() V42() V47() set
Seg (len y) is V42() V49( len y) Element of K10(NAT)
dom ((U1,U2,f) * a) is Element of K10(NAT)
dom (f * y) is Element of K10(NAT)
dom y is Element of K10(NAT)
y . o1y is set
b . o1y is set
Class ((U1,U2,f),(y . o1y)) is Element of K10( the carrier of U1)
K10( the carrier of U1) is set
((U1,U2,f) * a) . o1y is set
ym is Element of the carrier of U1
Class ((U1,U2,f),ym) is Element of K10( the carrier of U1)
(U1,U2,f) . (Class ((U1,U2,f),ym)) is set
f . (y . o1y) is set
(f * y) . o1y is set
u . (f * y) is set
(U1,(U1,U2,f),y) is non empty Relation-like (Class (U1,U2,f)) * -defined Class (U1,U2,f) -valued Function-like homogeneous quasi_total Element of K10(K11(((Class (U1,U2,f)) *),(Class (U1,U2,f))))
K11(((Class (U1,U2,f)) *),(Class (U1,U2,f))) is Relation-like set
K10(K11(((Class (U1,U2,f)) *),(Class (U1,U2,f)))) is set
(arity y) -tuples_on (Class (U1,U2,f)) is non empty functional FinSequence-membered FinSequenceSet of Class (U1,U2,f)
{ b₁ where b₁ is Relation-like NAT -defined Class (U1,U2,f) -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class (U1,U2,f)) * : len b₁ = arity y } is set
o1y is Relation-like NAT -defined Class (U1,U2,f) -valued Function-like V42() FinSequence-like FinSubsequence-like Element of (Class (U1,U2,f)) *
len o1y is V35() V36() V37() V41() V42() V47() Element of NAT
y . y is set
rng y is non empty Element of K10( the carrier of U1)
o1y is Element of the carrier of U1
Class ((U1,U2,f),o1y) is Element of K10( the carrier of U1)
(U1,U2,f) . (Class ((U1,U2,f),o1y)) is set
f . (y . y) is set
dom (U1,U2,f) is non empty Element of K10( the carrier of (U1,(U1,U2,f)))
K10( the carrier of (U1,(U1,U2,f))) is set
x is set
dom (U1,U2,f) is non empty set
(U1,U2,f) . x is set
y is set
(U1,U2,f) . y is set
K10( the carrier of U1) is set
y is Element of K10( the carrier of U1)
a is set
Class ((U1,U2,f),a) is Element of K10( the carrier of U1)
u is Element of K10( the carrier of U1)
b is set
Class ((U1,U2,f),b) is Element of K10( the carrier of U1)
(U1,U2,f) . u is set
b is Element of the carrier of U1
f . b is Element of the carrier of U2
(U1,U2,f) . y is set
a is Element of the carrier of U1
f . a is Element of the carrier of U2
[a,b] is set
{a,b} is non empty set
{a} is non empty V2() V49(1) set
{{a,b},{a}} is non empty set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
(U1,U2,f) is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
(U1,(U1,U2,f)) is non empty strict V91() quasi_total non-empty UAStr
Class (U1,U2,f) is non empty V4() a_partition of the carrier of U1
(U1,(U1,U2,f)) is Relation-like NAT -defined PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f))) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f)))
(Class (U1,U2,f)) * is non empty functional FinSequence-membered FinSequenceSet of Class (U1,U2,f)
PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f))) is non empty functional set
UAStr(# (Class (U1,U2,f)),(U1,(U1,U2,f)) #) is non empty strict UAStr
(U1,U2,f) is non empty Relation-like the carrier of (U1,(U1,U2,f)) -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2))
the carrier of (U1,(U1,U2,f)) is non empty set
K11( the carrier of (U1,(U1,U2,f)), the carrier of U2) is Relation-like set
K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2)) is set
rng f is non empty Element of K10( the carrier of U2)
K10( the carrier of U2) is set
rng (U1,U2,f) is non empty Element of K10( the carrier of U2)
x is set
dom f is non empty Element of K10( the carrier of U1)
K10( the carrier of U1) is set
y is set
f . y is set
y is Element of the carrier of U1
Class ((U1,U2,f),y) is Element of K10( the carrier of U1)
dom (U1,U2,f) is non empty Element of K10( the carrier of (U1,(U1,U2,f)))
K10( the carrier of (U1,(U1,U2,f))) is set
(U1,U2,f) . (Class ((U1,U2,f),y)) is set
U1 is non empty V91() quasi_total non-empty UAStr
the carrier of U1 is non empty set
U2 is non empty V91() quasi_total non-empty UAStr
the carrier of U2 is non empty set
K11( the carrier of U1, the carrier of U2) is Relation-like set
K10(K11( the carrier of U1, the carrier of U2)) is set
f is non empty Relation-like the carrier of U1 -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of U1, the carrier of U2))
(U1,U2,f) is Relation-like the carrier of U1 -defined the carrier of U1 -valued reflexive symmetric transitive total quasi_total (U1)
(U1,(U1,U2,f)) is non empty strict V91() quasi_total non-empty UAStr
Class (U1,U2,f) is non empty V4() a_partition of the carrier of U1
(U1,(U1,U2,f)) is Relation-like NAT -defined PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f))) -valued Function-like V42() FinSequence-like FinSubsequence-like FinSequence of PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f)))
(Class (U1,U2,f)) * is non empty functional FinSequence-membered FinSequenceSet of Class (U1,U2,f)
PFuncs (((Class (U1,U2,f)) *),(Class (U1,U2,f))) is non empty functional set
UAStr(# (Class (U1,U2,f)),(U1,(U1,U2,f)) #) is non empty strict UAStr
(U1,U2,f) is non empty Relation-like the carrier of (U1,(U1,U2,f)) -defined the carrier of U2 -valued Function-like total quasi_total Element of K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2))
the carrier of (U1,(U1,U2,f)) is non empty set
K11( the carrier of (U1,(U1,U2,f)), the carrier of U2) is Relation-like set
K10(K11( the carrier of (U1,(U1,U2,f)), the carrier of U2)) is set