let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis:
let X be V5() ManySortedSet of ; :: 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 ;
reconsider HHp = HH .. p as Function ;
A5: dom HHp = dom HH by PRALG_1:def 17;
A6: rng (the_arity_of av) c= the carrier of IIG by FINSEQ_1:def 4;
then A7: rng (the_arity_of av) c= dom H by PARTFUN1:def 4;
then H * (the_arity_of av) is FinSequence by FINSEQ_1:20;
then consider n being Nat such that
A8: dom HH = Seg n by A4, FINSEQ_1:def 2;
reconsider HHp = HHp as FinSequence by A5, A8, FINSEQ_1:def 2;
A9: the_result_sort_of av = v by A1, MSAFREE2:def 7;

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

end;

then reconsider HHp = HHp as DTree-yielding FinSequence by TREES_3:26;
take HHp ; :: thesis:
thus HHp = HH .. p ; :: thesis:
dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;
then A13: ((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 ;
set f = the Sorts of (FreeMSA X) * (the_arity_of av);
A14: dom the Sorts of (FreeMSA X) = the carrier of IIG by PARTFUN1:def 4;
then A15: ( dom (the Sorts of (FreeMSA X) * (the_arity_of av)) = dom (the_arity_of av) & dom (the_arity_of av) = dom HH ) by A4, A6, A7, RELAT_1:46;
len p = len (the_arity_of av) by A2, A9, MSAFREE2:13;
then A16: dom p = dom (the_arity_of av) by FINSEQ_3:31;

let x be set ; :: thesis:
assume A17: x in dom (the Sorts of (FreeMSA X) * (the_arity_of av)) ; :: thesis:
then reconsider n = x as Element of NAT by A15;
A18: n in dom (the_arity_of av) by A6, A14, A17, RELAT_1:46;
(the_arity_of av) . x in rng (the_arity_of av) by A15, A17, FUNCT_1:def 5;
then reconsider s = (the_arity_of av) . x as SortSymbol of IIG by A6;
(the Sorts of (FreeMSA X) * (the_arity_of av)) . x = the Sorts of (FreeMSA X) . s by A15, A17, FUNCT_1:23;
hence p . x in (the Sorts of (FreeMSA X) * (the_arity_of av)) . x by A2, A9, A18, MSAFREE2:14; :: thesis:

end;

then p in ((the Sorts of (FreeMSA X) # ) * the Arity of IIG) . av by A13, A15, A16, CARD_3:def 5;
then reconsider x = p as Element of Args av,(FreeMSA X) by MSUALG_1:def 9;
A19: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 16;
then A20: Den av,(FreeMSA X) = (FreeOper X) . av by MSUALG_1:def 11
.= DenOp av,X by MSAFREE:def 15 ;
the Sorts of (FreeMSA X) . v = FreeSort X,v by A19, MSAFREE:def 13;
then [av,the carrier of IIG] -tree p in FreeSort X,v by A2;
then [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;
then consider a being Element of TS (DTConMSA X) such that
A21: a = [av,the carrier of IIG] -tree p and
A22: ( 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 ) ) ;
consider x' being set such that
A23: ( ( 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 A22;

assume a = root-tree [x',v] ; :: thesis:
then ( a . {} = [x',v] & a . {} = [av,the carrier of IIG] ) by A21, TREES_4:3, TREES_4:def 4;
then the carrier of IIG = v by ZFMISC_1:33;
hence contradiction by Lm1; :: thesis:

end;

then consider o being OperSymbol of IIG such that
A24: [o,the carrier of IIG] = a . {} and
the_result_sort_of o = v by A23;
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;
A25: a . {} = [av,the carrier of IIG] by A21, TREES_4:def 4;
consider ts being FinSequence of TS (DTConMSA X) such that
A26: a = nt -tree ts and
A27: nt ==> roots ts by A24, DTCONSTR:10;
A28: ts = p by A21, A26, TREES_4:15;
reconsider p' = p as FinSequence of TS (DTConMSA X) by A21, A26, TREES_4:15;
A29: Sym av,X = [av,the carrier of IIG] by MSAFREE:def 11;
then A30: (DenOp av,X) . p' = t by A2, A24, A25, A27, A28, MSAFREE:def 14;
reconsider Hx = H # x as Function ;
A31: dom Hx = dom HH by A15, MSUALG_3:6;

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

end;

then A33: HHp = H # x by A31, PRALG_1:def 17;

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

end;

then A39: HHp in (((FreeSort X) # ) * the Arity of IIG) . av by A5, A13, A15, A19, CARD_3:def 5;
then reconsider HHp' = HHp as FinSequence of TS (DTConMSA X) by MSAFREE:8;
A40: Sym av,X ==> roots HHp' by A39, MSAFREE:10;
thus (H . v) . t = (DenOp av,X) . HHp by A3, A9, A20, A30, A33, MSUALG_3:def 9
.= [(action_at v),the carrier of IIG] -tree HHp by A29, A40, MSAFREE:def 14 ; :: thesis: