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 (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 )

let X be V2() ManySortedSet of the carrier of IIG; :: thesis: 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 )

let H be ManySortedFunction of (FreeMSA X),(FreeMSA X); :: 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 (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 )

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 (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 )

let v be SortSymbol of IIG; :: thesis: 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 )

let p be DTree-yielding FinSequence; :: thesis: 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 )

let t be Element of the Sorts of (FreeMSA X) . v; :: thesis: ( 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)) implies ex HHp being DTree-yielding FinSequence st

( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp ) )

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: ex HHp being DTree-yielding FinSequence st

( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )

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;

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;

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 ;

.= (dom HH) /\ (dom p) by A12, PRALG_1:def 19 ;

A26: HHp = Hx by PRALG_1:def 19, AA, A24, A6, A9;

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: ( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )

thus HHp = HH .. p ; :: thesis: (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp

A31: Sym (av,X) = [av, the carrier of IIG] by MSAFREE:def 9;

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: verum

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 )

let X be V2() ManySortedSet of the carrier of IIG; :: thesis: 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 )

let H be ManySortedFunction of (FreeMSA X),(FreeMSA X); :: 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 (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 )

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 (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 )

let v be SortSymbol of IIG; :: thesis: 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 )

let p be DTree-yielding FinSequence; :: thesis: 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 )

let t be Element of the Sorts of (FreeMSA X) . v; :: thesis: ( 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)) implies ex HHp being DTree-yielding FinSequence st

( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp ) )

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: ex HHp being DTree-yielding FinSequence st

( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )

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: for x9 being object st x9 in dom HHp holds

HHp . x9 is DecoratedTree

set f = the Sorts of (FreeMSA X) * (the_arity_of av);HHp . x9 is DecoratedTree

reconsider HH9 = HH as FinSequence by A4, A8, FINSEQ_1:16;

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 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: verum

end;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 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: verum

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: for x being object st x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) holds

p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x

then
p in (( the Sorts of (FreeMSA X) #) * the Arity of IIG) . av
by A17, A21, A6, CARD_3:def 5;p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x

let x be object ; :: thesis: ( x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) implies p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x )

assume A22: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; :: thesis: p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x

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: verum

end;assume A22: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; :: thesis: p . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x

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: verum

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: for x9 being set st x9 in dom HH holds

Hx . x9 = (HH . x9) . (p . x9)

AA: dom Hx =
dom HH
by A9, MSUALG_3:6
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 (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: verum

end;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 (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: verum

.= (dom HH) /\ (dom p) by A12, PRALG_1:def 19 ;

A26: HHp = Hx by PRALG_1:def 19, AA, A24, A6, A9;

now :: thesis: not a = root-tree [x9,v]

then consider o being OperSymbol of IIG such that assume
a = root-tree [x9,v]
; :: thesis: contradiction

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: verum

end;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: verum

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: ( HHp = HH .. p & (H . v) . t = [(action_at v), the carrier of IIG] -tree HHp )

thus HHp = HH .. p ; :: thesis: (H . v) . t = [(action_at v), 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 (FreeMSA X) * (the_arity_of av)) holds

HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x

then A35:
HHp in (((FreeSort X) #) * the Arity of IIG) . av
by A12, A17, A21, A9, A10, CARD_3:def 5;HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x

let x be object ; :: thesis: ( x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) implies HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x )

reconsider g = HH . x as Function ;

assume A32: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; :: thesis: HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x

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: verum

end;reconsider g = HH . x as Function ;

assume A32: x in dom ( the Sorts of (FreeMSA X) * (the_arity_of av)) ; :: thesis: HHp . x in ( the Sorts of (FreeMSA X) * (the_arity_of av)) . x

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: verum

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: verum