let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis:
let X be V16() ManySortedSet of the carrier of IIG; :: thesis:
let H be ManySortedFunction of (FreeMSA X),(FreeMSA X); :: thesis:
let HH be Function-yielding Function; :: thesis:
let v be SortSymbol of IIG; :: thesis:
let p be DTree-yielding FinSequence; :: thesis:
let t be Element of the Sorts of (FreeMSA X) . v; :: thesis:
assume that
A1: v in InnerVertices IIG and
A2: t = [(action_at v), the carrier of IIG] -tree p and
A3: H is_homomorphism FreeMSA X, FreeMSA X and
A4: HH = H * (the_arity_of (action_at v)) ; :: thesis:
reconsider av = action_at v as OperSymbol of IIG ;
A5: the_result_sort_of av = v by A1, MSAFREE2:def 7;
then len p = len (the_arity_of av) by A2, MSAFREE2:13;
then A6: dom p = dom (the_arity_of av) by FINSEQ_3:31;
A7: rng (the_arity_of av) c= the carrier of IIG by FINSEQ_1:def 4;
then A8: rng (the_arity_of av) c= dom H by PARTFUN1:def 4;
then A9: dom (the_arity_of av) = dom HH by A4, RELAT_1:46;
A10: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 16;
then the Sorts of (FreeMSA X) . v = FreeSort (X,v) by MSAFREE:def 13;
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 (DTConMSA X) : ( 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 12;
reconsider HHp = HH .. p as Function ;
A12: dom HHp = dom HH by PRALG_1:def 17;
H * (the_arity_of av) is FinSequence by A8, FINSEQ_1:20;
then ex n being Nat st dom HH = Seg n by A4, FINSEQ_1:def 2;
then reconsider HHp = HHp as FinSequence by A12, FINSEQ_1:def 2;

A13: now

reconsider HH9 = HH as FinSequence by A4, A8, FINSEQ_1:20;
let x9 be set ; :: thesis:
set x = HHp . x9;
reconsider g = HH . x9 as Function ;
assume A14: x9 in dom HHp ; :: thesis:
then reconsider k = x9 as Element of NAT ;
A15: HHp . x9 = g . (p . k) by A12, A14, PRALG_1:def 17;
len HH9 = len (the_arity_of av) by A4, A8, FINSEQ_2:33;
then A16: dom HH9 = dom (the_arity_of av) by FINSEQ_3:31;
then reconsider s = (the_arity_of av) . k as SortSymbol of IIG by A12, A14, FINSEQ_2:13;
g = H . s by A4, A12, A14, A16, FUNCT_1:23;
then HHp . x9 in the Sorts of (FreeMSA X) . s by A2, A12, A5, A14, A16, A15, FUNCT_2:7, MSAFREE2:14;
hence HHp . x9 is DecoratedTree ; :: thesis:

end;

set f = the Sorts of (FreeMSA X) * (the_arity_of av);
dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;
then A17: (( the Sorts of (FreeMSA X) #) * the Arity of IIG) . av = ( the Sorts of (FreeMSA X) #) . ( the Arity of IIG . av) by FUNCT_1:23
.= ( the Sorts of (FreeMSA X) #) . (the_arity_of av) by MSUALG_1:def 6
.= product ( the Sorts of (FreeMSA X) * (the_arity_of av)) by PBOOLE:def 19 ;
reconsider HHp = HHp as DTree-yielding FinSequence by A13, TREES_3:26;
consider a being Element of TS (DTConMSA X) 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 (FreeMSA X) = the carrier of IIG by PARTFUN1:def 4;
then A22: dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) = dom (the_arity_of av) by A7, RELAT_1:46;

now

let x be set ; :: thesis:
assume A23: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; :: thesis:
then reconsider n = x as Element of NAT by A22;
(the_arity_of av) . x in rng (the_arity_of av) by A22, A23, FUNCT_1:def 5;
then reconsider s = (the_arity_of av) . x as SortSymbol of IIG by A7;
( n in dom (the_arity_of av) & ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x = the Sorts of (FreeMSA X) . s ) by A22, A23, FUNCT_1:23;
hence p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x by A2, A5, MSAFREE2:14; :: thesis:

end;

then p in (( the Sorts of (FreeMSA X) #) * the Arity of IIG) . av by A17, A22, A6, CARD_3:def 5;
then reconsider x = p as Element of Args (av,(FreeMSA X)) by MSUALG_1:def 9;
A24: a . {} = [av, the carrier of IIG] by A18, TREES_4:def 4;
reconsider Hx = H # x as Function ;

A25: now

let x9 be set ; :: thesis:
assume A26: x9 in dom HH ; :: thesis:
then reconsider n = x9 as Element of NAT by A9;
(the_arity_of av) . n in rng (the_arity_of av) by A9, A26, FUNCT_1:def 5;
then reconsider s = (the_arity_of av) . n as SortSymbol of IIG by A7;
Hx . n = (H . ((the_arity_of av) /. n)) . (p . n) by A9, A6, A26, MSUALG_3:def 8
.= (H . s) . (p . n) by A9, A26, PARTFUN1:def 8 ;
hence Hx . x9 = (HH . x9) . (p . x9) by A4, A9, A26, FUNCT_1:23; :: thesis:

end;

dom Hx = dom HH by A9, MSUALG_3:6;
then A27: HHp = H # x by A25, PRALG_1:def 17;

now

assume a = root-tree [x9,v] ; :: thesis:
then A28: a . {} = [x9,v] by TREES_4:3;
a . {} = [av, the carrier of IIG] by A18, TREES_4:def 4;
then the carrier of IIG = v by A28, ZFMISC_1:33;
hence contradiction by Lm1; :: thesis:

end;

then consider o being OperSymbol of IIG such that
A29: [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:106;
then reconsider nt = [o, the carrier of IIG] as NonTerminal of (DTConMSA X) by MSAFREE:6;
consider ts being FinSequence of TS (DTConMSA X) such that
A30: a = nt -tree ts and
A31: nt ==> roots ts by A29, DTCONSTR:10;
take HHp ; :: thesis:
thus HHp = HH .. p ; :: thesis:
A32: Sym (av,X) = [av, the carrier of IIG] by MSAFREE:def 11;

now

let x be set ; :: thesis:
reconsider g = HH . x as Function ;
assume A33: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; :: thesis:
then A34: HHp . x = g . (p . x) by A22, A9, PRALG_1:def 17;
(the_arity_of av) . x in rng (the_arity_of av) by A22, A33, FUNCT_1:def 5;
then reconsider s = (the_arity_of av) . x as SortSymbol of IIG by A7;
A35: the_result_sort_of av = v by A1, MSAFREE2:def 7;
( ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x = the Sorts of (FreeMSA X) . s & g = H . s ) by A4, A22, A33, FUNCT_1:23;
hence HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x by A2, A22, A33, A35, A34, FUNCT_2:7, MSAFREE2:14; :: thesis:

end;

then A36: HHp in (((FreeSort X) #) * the Arity of IIG) . av by A12, A17, A22, A9, A10, CARD_3:def 5;
then reconsider HHp9 = HHp as FinSequence of TS (DTConMSA X) by MSAFREE:8;
A37: Sym (av,X) ==> roots HHp9 by A36, MSAFREE:10;
reconsider p9 = p as FinSequence of TS (DTConMSA X) by A18, A30, TREES_4:15;
ts = p by A18, A30, TREES_4:15;
then A38: (DenOp (av,X)) . p9 = t by A2, A29, A24, A31, A32, MSAFREE:def 14;
Den (av,(FreeMSA X)) = (FreeOper X) . av by A10, MSUALG_1:def 11
.= DenOp (av,X) by MSAFREE:def 15 ;
hence (H . v) . t = (DenOp (av,X)) . HHp by A3, A5, A38, A27, MSUALG_3:def 9
.= [(action_at v), the carrier of IIG] -tree HHp by A32, A37, MSAFREE:def 14 ;
:: thesis: