theorem
for
S being non
empty non
void ManySortedSign for
Y being
infinite-yielding ManySortedSet of the
carrier of
S for
v being
Element of
(Free (S,Y)) for
h being
Endomorphism of
Free (
S,
Y)
for
f being
vf-sequence of
v st
f <> {} holds
ex
B being non
empty FinSequence of the
carrier of
S ex
V1 being
b6 -sorts FinSequence of
Union Y st
(
dom B = dom f &
B = pr2 f &
V1 = pr1 f & ex
D being
b6 -sorts FinSequence of
(Free (S,Y)) ex
V2 being
b6 -sorts b7 -omitting b8 -omitting FinSequence of
Union Y st
( ( for
i being
Element of
dom B holds
D . i = h . ((V1 . i) -term) ) & ex
F being
b9 -context-sequence FinSequence of
(Free (S,Y)) st
(
F is
V1,
V2,
D -consequent-context-sequence &
(F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v &
h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )