theorem :: MSAFREE5:147

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 b₆ -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b₆ -sorts FinSequence of (Free (S,Y)) ex V2 being b₆ -sorts b₇ -omitting b₈ -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b₉ -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)))) ) ) )