theorem
Th34
:
:: MONOID_1:34
for
x
being
set
for
A
being non
empty
set
for
p
being
FinSequence
of
A
holds
dom
(
{
x
}
|`
(
p
^
<*
x
*>
)
)
=
(
dom
(
{
x
}
|`
p
)
)
\/
{
(
(
len
p
)
+
1
)
}