for IIG being non empty non void Circuit-like monotonic ManySortedSign
for X being V2() ManySortedSet of the carrier of IIG
for H being ManySortedFunction of (FreeMSA X),(FreeMSA X)
for HH being Function-yielding Function
for v being SortSymbol of IIG
for p being DTree-yielding FinSequence
for t being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices IIG & t = [(action_at v), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )