let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis:
let X be non-empty 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:10;
then A6: dom p = dom (the_arity_of av) by FINSEQ_3:29;
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 2;
then A9: dom (the_arity_of av) = dom HH by A4, RELAT_1:27;
A10: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 14;
then the Sorts of (FreeMSA X) . 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 (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 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 * (the_arity_of av) is FinSequence by A8, FINSEQ_1:16;
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 :: thesis:

reconsider HH9 = HH as FinSequence by A4, A8, FINSEQ_1:16;
let x9 be object ; :: 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 A14, PRALG_1:def 19;
len HH9 = len (the_arity_of av) by A4, A8, FINSEQ_2:29;
then A16: dom HH9 = dom (the_arity_of av) by FINSEQ_3:29;
then reconsider s = (the_arity_of av) . k as SortSymbol of IIG by A12, A14, FINSEQ_2:11;
g = H . s by A4, A12, A14, A16, FUNCT_1:13;
then HHp . x9 in the Sorts of (FreeMSA X) . s by A2, A12, A5, A14, A16, A15, FUNCT_2:5, MSAFREE2:11;
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:13
.= ( the Sorts of (FreeMSA X) #) . (the_arity_of av) by MSUALG_1:def 1
.= product ( the Sorts of (FreeMSA X) * (the_arity_of av)) by FINSEQ_2:def 5 ;
reconsider HHp = HHp as DTree-yielding FinSequence by A13, TREES_3:24;
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 2;
then A21: dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) = dom (the_arity_of av) by A7, RELAT_1:27;

now :: thesis:

let x be object ; :: thesis:
assume A22: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; :: thesis:
then reconsider n = x as Element of NAT by A21;
(the_arity_of av) . x in rng (the_arity_of av) by A21, A22, FUNCT_1:def 3;
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 A21, A22, FUNCT_1:13;
hence p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x by A2, A5, MSAFREE2:11; :: thesis:

end;

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

A24: now :: thesis:

let x9 be set ; :: thesis:
assume A25: 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, A25, FUNCT_1:def 3;
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, A25, MSUALG_3:def 6
.= (H . s) . (p . n) by A9, A25, PARTFUN1:def 6 ;
hence Hx . x9 = (HH . x9) . (p . x9) by A4, A9, A25, FUNCT_1:13; :: thesis:

end;

AA: dom Hx = dom HH by A9, MSUALG_3:6
.= (dom HH) /\ (dom p) by A12, PRALG_1:def 19 ;
A26: HHp = Hx by PRALG_1:def 19, AA, A24, A6, A9;

now :: thesis:

assume a = root-tree [x9,v] ; :: thesis:
then A27: 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 A27, XTUPLE_0:1;
hence contradiction by Lm1; :: thesis:

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

now :: thesis:

let x be object ; :: thesis:
reconsider g = HH . x as Function ;
assume A32: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; :: thesis:
dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) c= dom (the_arity_of av) by RELAT_1:25;
then A33: HHp . x = g . (p . x) by A32, A9, A12, PRALG_1:def 19;
(the_arity_of av) . x in rng (the_arity_of av) by A21, A32, FUNCT_1:def 3;
then reconsider s = (the_arity_of av) . x as SortSymbol of IIG by A7;
A34: 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, A21, A32, FUNCT_1:13;
hence HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x by A2, A21, A32, A34, A33, FUNCT_2:5, MSAFREE2:11; :: thesis:

end;

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