let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for X being V2() ManySortedSet of the carrier of IIG
for H being ManySortedFunction of (),()
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 () . v st v in InnerVertices IIG & t = [(), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * () holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(), the carrier of IIG] -tree HHp )

let X be V2() ManySortedSet of the carrier of IIG; :: thesis: for H being ManySortedFunction of (),()
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 () . v st v in InnerVertices IIG & t = [(), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * () holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(), the carrier of IIG] -tree HHp )

let H be ManySortedFunction of (),(); :: thesis: 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 () . v st v in InnerVertices IIG & t = [(), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * () holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(), the carrier of IIG] -tree HHp )

let HH be Function-yielding Function; :: thesis: for v being SortSymbol of IIG
for p being DTree-yielding FinSequence
for t being Element of the Sorts of () . v st v in InnerVertices IIG & t = [(), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * () holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(), the carrier of IIG] -tree HHp )

let v be SortSymbol of IIG; :: thesis: for p being DTree-yielding FinSequence
for t being Element of the Sorts of () . v st v in InnerVertices IIG & t = [(), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * () holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(), the carrier of IIG] -tree HHp )

let p be DTree-yielding FinSequence; :: thesis: for t being Element of the Sorts of () . v st v in InnerVertices IIG & t = [(), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * () holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(), the carrier of IIG] -tree HHp )

let t be Element of the Sorts of () . v; :: thesis: ( v in InnerVertices IIG & t = [(), the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * () implies ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(), the carrier of IIG] -tree HHp ) )

assume that
A1: v in InnerVertices IIG and
A2: t = [(), the carrier of IIG] -tree p and
A3: H is_homomorphism FreeMSA X, FreeMSA X and
A4: HH = H * () ; :: thesis: ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(), the carrier of IIG] -tree HHp )

reconsider av = action_at v as OperSymbol of IIG ;
A5: the_result_sort_of av = v by ;
then len p = len () by ;
then A6: dom p = dom () by FINSEQ_3:29;
A7: rng () c= the carrier of IIG by FINSEQ_1:def 4;
then A8: rng () c= dom H by PARTFUN1:def 2;
then A9: dom () = dom HH by ;
A10: FreeMSA X = MSAlgebra(# (),() #) by MSAFREE:def 14;
then the Sorts of () . v = FreeSort (X,v) by MSAFREE:def 11;
then [av, the carrier of IIG] -tree p in FreeSort (X,v) by A2;
then A11: [av, the carrier of IIG] -tree p in { a where a is Element of TS () : ( ex x being set st
( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) )
}
by MSAFREE:def 10;
reconsider HHp = HH .. p as Function ;
A12: dom HHp = (dom HH) /\ (dom p) by PRALG_1:def 19
.= dom HH by A6, A9 ;
H * () is FinSequence by ;
then ex n being Nat st dom HH = Seg n by ;
then reconsider HHp = HHp as FinSequence by ;
A13: now :: thesis: for x9 being object st x9 in dom HHp holds
HHp . x9 is DecoratedTree
reconsider HH9 = HH as FinSequence by ;
let x9 be object ; :: thesis: ( x9 in dom HHp implies HHp . x9 is DecoratedTree )
set x = HHp . x9;
reconsider g = HH . x9 as Function ;
assume A14: x9 in dom HHp ; :: thesis: HHp . x9 is DecoratedTree
then reconsider k = x9 as Element of NAT ;
A15: HHp . x9 = g . (p . k) by ;
len HH9 = len () by ;
then A16: dom HH9 = dom () by FINSEQ_3:29;
then reconsider s = () . k as SortSymbol of IIG by ;
g = H . s by ;
then HHp . x9 in the Sorts of () . s by ;
hence HHp . x9 is DecoratedTree ; :: thesis: verum
end;
set f = the Sorts of () * ();
dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;
then A17: (( the Sorts of () #) * the Arity of IIG) . av = ( the Sorts of () #) . ( the Arity of IIG . av) by FUNCT_1:13
.= ( the Sorts of () #) . () by MSUALG_1:def 1
.= product ( the Sorts of () * ()) by FINSEQ_2:def 5 ;
reconsider HHp = HHp as DTree-yielding FinSequence by ;
consider a being Element of TS () such that
A18: a = [av, the carrier of IIG] -tree p and
A19: ( ex x being set st
( x in X . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) by A11;
consider x9 being set such that
A20: ( ( x9 in X . v & a = root-tree [x9,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) by A19;
dom the Sorts of () = the carrier of IIG by PARTFUN1:def 2;
then A21: dom ( the Sorts of () * ()) = dom () by ;
now :: thesis: for x being object st x in dom ( the Sorts of () * ()) holds
p . x in ( the Sorts of () * ()) . x
let x be object ; :: thesis: ( x in dom ( the Sorts of () * ()) implies p . x in ( the Sorts of () * ()) . x )
assume A22: x in dom ( the Sorts of () * ()) ; :: thesis: p . x in ( the Sorts of () * ()) . x
then reconsider n = x as Element of NAT by A21;
(the_arity_of av) . x in rng () by ;
then reconsider s = () . x as SortSymbol of IIG by A7;
( n in dom () & ( the Sorts of () * ()) . x = the Sorts of () . s ) by ;
hence p . x in ( the Sorts of () * ()) . x by ; :: thesis: verum
end;
then p in (( the Sorts of () #) * the Arity of IIG) . av by ;
then reconsider x = p as Element of Args (av,()) by MSUALG_1:def 4;
A23: a . {} = [av, the carrier of IIG] by ;
reconsider Hx = H # x as Function ;
A24: now :: thesis: for x9 being set st x9 in dom HH holds
Hx . x9 = (HH . x9) . (p . x9)
let x9 be set ; :: thesis: ( x9 in dom HH implies Hx . x9 = (HH . x9) . (p . x9) )
assume A25: x9 in dom HH ; :: thesis: Hx . x9 = (HH . x9) . (p . x9)
then reconsider n = x9 as Element of NAT by A9;
(the_arity_of av) . n in rng () by ;
then reconsider s = () . n as SortSymbol of IIG by A7;
Hx . n = (H . (() /. n)) . (p . n) by
.= (H . s) . (p . n) by ;
hence Hx . x9 = (HH . x9) . (p . x9) by ; :: thesis: verum
end;
AA: dom Hx = dom HH by
.= (dom HH) /\ (dom p) by ;
A26: HHp = Hx by ;
now :: thesis: not a = root-tree [x9,v]
assume a = root-tree [x9,v] ; :: thesis: contradiction
then A27: a . {} = [x9,v] by TREES_4:3;
a . {} = [av, the carrier of IIG] by ;
then the carrier of IIG = v by ;
hence contradiction by Lm1; :: thesis: verum
end;
then consider o being OperSymbol of IIG such that
A28: [o, the carrier of IIG] = a . {} and
the_result_sort_of o = v by A20;
the carrier of IIG in { the carrier of IIG} by TARSKI:def 1;
then [o, the carrier of IIG] in [: the carrier' of IIG,{ the carrier of IIG}:] by ZFMISC_1:87;
then reconsider nt = [o, the carrier of IIG] as NonTerminal of () by MSAFREE:6;
consider ts being FinSequence of TS () such that
A29: a = nt -tree ts and
A30: nt ==> roots ts by ;
take HHp ; :: thesis: ( HHp = HH .. p & (H . v) . t = [(), the carrier of IIG] -tree HHp )
thus HHp = HH .. p ; :: thesis: (H . v) . t = [(), the carrier of IIG] -tree HHp
A31: Sym (av,X) = [av, the carrier of IIG] by MSAFREE:def 9;
now :: thesis: for x being object st x in dom ( the Sorts of () * ()) holds
HHp . x in ( the Sorts of () * ()) . x
let x be object ; :: thesis: ( x in dom ( the Sorts of () * ()) implies HHp . x in ( the Sorts of () * ()) . x )
reconsider g = HH . x as Function ;
assume A32: x in dom ( the Sorts of () * ()) ; :: thesis: HHp . x in ( the Sorts of () * ()) . x
dom ( the Sorts of () * ()) c= dom () by RELAT_1:25;
then A33: HHp . x = g . (p . x) by ;
(the_arity_of av) . x in rng () by ;
then reconsider s = () . x as SortSymbol of IIG by A7;
A34: the_result_sort_of av = v by ;
( ( the Sorts of () * ()) . x = the Sorts of () . s & g = H . s ) by ;
hence HHp . x in ( the Sorts of () * ()) . x by ; :: thesis: verum
end;
then A35: HHp in ((() #) * the Arity of IIG) . av by ;
then reconsider HHp9 = HHp as FinSequence of TS () by MSAFREE:8;
A36: Sym (av,X) ==> roots HHp9 by ;
reconsider p9 = p as FinSequence of TS () by ;
ts = p by ;
then A37: (DenOp (av,X)) . p9 = t by ;
Den (av,()) = () . av by
.= DenOp (av,X) by MSAFREE:def 13 ;
hence (H . v) . t = (DenOp (av,X)) . HHp by
.= [(), the carrier of IIG] -tree HHp by ;
:: thesis: verum