let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for h being Endomorphism of Free (S,X)
for t, t1 being Element of (Free (S,X))
for xi being Node of t st t1 = t | xi holds
(h . t) | xi = h . t1
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for h being Endomorphism of Free (S,X)
for t, t1 being Element of (Free (S,X))
for xi being Node of t st t1 = t | xi holds
(h . t) | xi = h . t1
let h be Endomorphism of Free (S,X); :: thesis: for t, t1 being Element of (Free (S,X))
for xi being Node of t st t1 = t | xi holds
(h . t) | xi = h . t1
let t, t1 be Element of (Free (S,X)); :: thesis: for xi being Node of t st t1 = t | xi holds
(h . t) | xi = h . t1
let xi be Node of t; :: thesis: ( t1 = t | xi implies (h . t) | xi = h . t1 )
defpred S₁[ Element of (Free (S,X))] means for xi being Node of $1
for t1 being Element of (Free (S,X)) st t1 = $1 | xi holds
( (h . $1) | xi = h . t1 & xi in dom (h . $1) );
A1: for s being SortSymbol of S
for x being Element of X . s holds S₁[x -term ]

proof

let s be SortSymbol of S; :: thesis: for x being Element of X . s holds S₁[x -term ]
let x be Element of X . s; :: thesis: S₁[x -term ]
let xi be Node of (x -term); :: thesis: for t1 being Element of (Free (S,X)) st t1 = (x -term) | xi holds
( (h . (x -term)) | xi = h . t1 & xi in dom (h . (x -term)) )
dom (x -term) = {{}} by TREES_1:29;
then A2: xi = {} ;
let t1 be Element of (Free (S,X)); :: thesis: ( t1 = (x -term) | xi implies ( (h . (x -term)) | xi = h . t1 & xi in dom (h . (x -term)) ) )
assume t1 = (x -term) | xi ; :: thesis: ( (h . (x -term)) | xi = h . t1 & xi in dom (h . (x -term)) )
then t1 = x -term by A2, TREES_9:1;
hence (h . (x -term)) | xi = h . t1 by A2, TREES_9:1; :: thesis: xi in dom (h . (x -term))
thus xi in dom (h . (x -term)) by A2, TREES_1:22; :: thesis: verum

end;

A3: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]

proof

let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) holds
S₁[o -term p]
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ( for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ) implies S₁[o -term p] )
assume A4: for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ; :: thesis: S₁[o -term p]
let xi be Node of (o -term p); :: thesis: for t1 being Element of (Free (S,X)) st t1 = (o -term p) | xi holds
( (h . (o -term p)) | xi = h . t1 & xi in dom (h . (o -term p)) )
let t1 be Element of (Free (S,X)); :: thesis: ( t1 = (o -term p) | xi implies ( (h . (o -term p)) | xi = h . t1 & xi in dom (h . (o -term p)) ) )
assume A5: t1 = (o -term p) | xi ; :: thesis: ( (h . (o -term p)) | xi = h . t1 & xi in dom (h . (o -term p)) )

per cases ( xi = {} or ex n being Nat ex t being DecoratedTree ex q being Node of t st
( n < len p & t = p . (n + 1) & xi = <*n*> ^ q ) ) by TREES_4:11;

suppose A6: xi = {} ; :: thesis: ( (h . (o -term p)) | xi = h . t1 & xi in dom (h . (o -term p)) )

hence (h . (o -term p)) | xi = h . (o -term p) by TREES_9:1
.= h . t1 by A5, A6, TREES_9:1 ;
:: thesis: xi in dom (h . (o -term p))
thus xi in dom (h . (o -term p)) by A6, TREES_1:22; :: thesis: verum

end;

suppose ex n being Nat ex t being DecoratedTree ex q being Node of t st
( n < len p & t = p . (n + 1) & xi = <*n*> ^ q ) ; :: thesis: ( (h . (o -term p)) | xi = h . t1 & xi in dom (h . (o -term p)) )

then consider n being Nat, t being DecoratedTree, q being Node of t such that
A6: ( n < len p & t = p . (n + 1) & xi = <*n*> ^ q ) ;
A8: t1 = ((o -term p) | <*n*>) | q by A5, A6, TREES_9:3;
( 1 <= n + 1 & n + 1 <= len p ) by A6, NAT_1:12, NAT_1:13;
then A10: n + 1 in dom p by FINSEQ_3:25;
then reconsider t = t as Element of (Free (S,X)) by A6, FUNCT_1:102;
A9: t = (o -term p) | <*n*> by A6, TREES_4:def 4;
t in rng p by A6, A10, FUNCT_1:def 3;
then A12: ( (h . t) | q = h . t1 & q in dom (h . t) ) by A8, A9, A4;
the_sort_of (o -term p) = the_result_sort_of o by Th8;
then ( h . (o -term p) = (h . (the_result_sort_of o)) . (o -term p) & o -term p = (Den (o,(Free (S,X)))) . p ) by ABBR, MSAFREE4:13;
then A13: h . (o -term p) = (Den (o,(Free (S,X)))) . (h # p) by MSUALG_6:def 2, MSUALG_3:def 7
.= o -term (h # p) by MSAFREE4:13 ;
( dom (h # p) = dom (the_arity_of o) & dom (the_arity_of o) = dom p ) by MSUALG_6:2;
then A16: len (h # p) = len p by FINSEQ_3:29;
then A14: (h # p) . (n + 1) = (o -term (h # p)) | <*n*> by A6, TREES_4:def 4;
( (h # p) . (n + 1) = (h . ((the_arity_of o) /. (n + 1))) . t & t = p /. (n + 1) ) by A6, A10, MSUALG_3:def 6, PARTFUN1:def 6;
then A15: (h # p) . (n + 1) = (h . (the_sort_of t)) . t by A10, Th4A
.= h . t by ABBR ;
then <*n*> ^ q in dom (o -term (h # p)) by A6, A12, A16, TREES_4:11;
hence ( (h . (o -term p)) | xi = h . t1 & xi in dom (h . (o -term p)) ) by A6, A12, A13, A14, A15, TREES_9:3; :: thesis: verum

end;

end;

end;

S₁[t] from MSAFREE5:sch 2(A1, A3);
hence ( t1 = t | xi implies (h . t) | xi = h . t1 ) ; :: thesis: verum