let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for h being Endomorphism of Free (S,X) holds
( dom t c= dom (h . t) & ( for I being set st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds
t | ((dom t) \ I) = (h . t) | ((dom t) \ I) ) )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X))
for h being Endomorphism of Free (S,X) holds
( dom t c= dom (h . t) & ( for I being set st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds
t | ((dom t) \ I) = (h . t) | ((dom t) \ I) ) )
let t be Element of (Free (S,X)); :: thesis: for h being Endomorphism of Free (S,X) holds
( dom t c= dom (h . t) & ( for I being set st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds
t | ((dom t) \ I) = (h . t) | ((dom t) \ I) ) )
let h be Endomorphism of Free (S,X); :: thesis: ( dom t c= dom (h . t) & ( for I being set st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds
t | ((dom t) \ I) = (h . t) | ((dom t) \ I) ) )
defpred S₁[ Element of (Free (S,X))] means ( dom $1 c= dom (h . $1) & ( for I being set st I = { xi where xi is Element of dom $1 : ex s being SortSymbol of S ex x being Element of X . s st $1 . xi = [x,s] } holds
$1 | ((dom $1) \ I) = (h . $1) | ((dom $1) \ I) ) );
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 ]
{} in dom (h . (x -term)) by TREES_1:22;
then {{}} c= dom (h . (x -term)) ;
hence dom (x -term) c= dom (h . (x -term)) by TREES_1:29; :: thesis: for I being set st I = { xi where xi is Element of dom (x -term) : ex s being SortSymbol of S ex x being Element of X . s st (x -term) . xi = [x,s] } holds
(x -term) | ((dom (x -term)) \ I) = (h . (x -term)) | ((dom (x -term)) \ I)
let I be set ; :: thesis: ( I = { xi where xi is Element of dom (x -term) : ex s being SortSymbol of S ex x being Element of X . s st (x -term) . xi = [x,s] } implies (x -term) | ((dom (x -term)) \ I) = (h . (x -term)) | ((dom (x -term)) \ I) )
assume A2: I = { xi where xi is Node of (x -term) : ex s being SortSymbol of S ex x1 being Element of X . s st (x -term) . xi = [x1,s] } ; :: thesis: (x -term) | ((dom (x -term)) \ I) = (h . (x -term)) | ((dom (x -term)) \ I)
( {} in dom (x -term) & (x -term) . {} = [x,s] ) by TREES_1:22, TREES_4:3;
then {} in I by A2;
then {{}} c= I ;
then dom (x -term) c= I by TREES_1:29;
then ( (x -term) | ((dom (x -term)) \ I) = {} & (h . (x -term)) | ((dom (x -term)) \ I) = {} ) ;
hence (x -term) | ((dom (x -term)) \ I) = (h . (x -term)) | ((dom (x -term)) \ I) ; :: 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 Z0: for t being Element of (Free (S,X)) st t in rng p holds
S₁[t] ; :: thesis: S₁[o -term p]
the_sort_of (o -term p) = the_result_sort_of o by Th8;
then A6: h . (o -term p) = (h . (the_result_sort_of o)) . (o -term p) by ABBR
.= (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . p) by MSAFREE4:13
.= (Den (o,(Free (S,X)))) . (h # p) by MSUALG_6:def 2, MSUALG_3:def 7
.= o -term (h # p) by MSAFREE4:13 ;
thus B3: dom (o -term p) c= dom (h . (o -term p)) :: thesis: for I being set st I = { xi where xi is Element of dom (o -term p) : ex s being SortSymbol of S ex x being Element of X . s st (o -term p) . xi = [x,s] } holds
(o -term p) | ((dom (o -term p)) \ I) = (h . (o -term p)) | ((dom (o -term p)) \ I)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (o -term p) or a in dom (h . (o -term p)) )
assume a in dom (o -term p) ; :: thesis: a in dom (h . (o -term p))

per cases then ( a = {} or ex i being Nat ex T being DecoratedTree ex r being Node of T st
( i < len p & T = p . (i + 1) & a = <*i*> ^ r ) ) by TREES_4:11;

suppose a = {} ; :: thesis: a in dom (h . (o -term p))

hence a in dom (h . (o -term p)) by TREES_1:22; :: thesis: verum

end;

suppose ex i being Nat ex T being DecoratedTree ex r being Node of T st
( i < len p & T = p . (i + 1) & a = <*i*> ^ r ) ; :: thesis: a in dom (h . (o -term p))

then consider i being Nat, T being DecoratedTree, r being Node of T such that
A7: ( i < len p & T = p . (i + 1) & a = <*i*> ^ r ) ;
( 1 <= i + 1 & i + 1 <= len p ) by A7, NAT_1:12, NAT_1:13;
then A8: i + 1 in dom p by FINSEQ_3:25;
then reconsider T = T as Element of (Free (S,X)) by A7, FUNCT_1:102;
T in rng p by A7, A8, FUNCT_1:def 3;
then dom T c= dom (h . T) by Z0;
then A9: r in dom (h . T) ;
A10: (h # p) . (i + 1) = (h . ((the_arity_of o) /. (i + 1))) . T by A7, A8, MSUALG_3:def 6
.= (h . ((the_arity_of o) /. (i + 1))) . (p /. (i + 1)) by A7, A8, PARTFUN1:def 6
.= (h . (the_sort_of (p /. (i + 1)))) . (p /. (i + 1)) by A8, Th4A
.= h . (p /. (i + 1)) by ABBR
.= h . T by A7, A8, PARTFUN1:def 6 ;
( dom (h # p) = dom (the_arity_of o) & dom (the_arity_of o) = dom p ) by MSUALG_6:2;
then len (h # p) = len p by FINSEQ_3:29;
hence a in dom (h . (o -term p)) by A7, A9, A10, A6, TREES_4:11; :: thesis: verum

end;

end;

end;

let I be set ; :: thesis: ( I = { xi where xi is Element of dom (o -term p) : ex s being SortSymbol of S ex x being Element of X . s st (o -term p) . xi = [x,s] } implies (o -term p) | ((dom (o -term p)) \ I) = (h . (o -term p)) | ((dom (o -term p)) \ I) )
assume A4: I = { xi where xi is Node of (o -term p) : ex s being SortSymbol of S ex x being Element of X . s st (o -term p) . xi = [x,s] } ; :: thesis: (o -term p) | ((dom (o -term p)) \ I) = (h . (o -term p)) | ((dom (o -term p)) \ I)
B2: (dom (o -term p)) \ I c= dom (h . (o -term p)) by B3;
thus dom ((o -term p) | ((dom (o -term p)) \ I)) = dom ((h . (o -term p)) | ((dom (o -term p)) \ I)) by B2, RELAT_1:62; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in proj1 ((o -term p) | ((dom (o -term p)) \ I)) or ((o -term p) | ((dom (o -term p)) \ I)) . b₁ = ((h . (o -term p)) | ((dom (o -term p)) \ I)) . b₁ )
let q be object ; :: thesis: ( not q in proj1 ((o -term p) | ((dom (o -term p)) \ I)) or ((o -term p) | ((dom (o -term p)) \ I)) . q = ((h . (o -term p)) | ((dom (o -term p)) \ I)) . q )
assume BB: q in dom ((o -term p) | ((dom (o -term p)) \ I)) ; :: thesis: ((o -term p) | ((dom (o -term p)) \ I)) . q = ((h . (o -term p)) | ((dom (o -term p)) \ I)) . q
reconsider q = q as Node of (o -term p) by BB;
B6: ( ((o -term p) | ((dom (o -term p)) \ I)) . q = (o -term p) . q & ((h . (o -term p)) | ((dom (o -term p)) \ I)) . q = (h . (o -term p)) . q ) by BB, FUNCT_1:49;

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

suppose q = {} ; :: thesis: ((o -term p) | ((dom (o -term p)) \ I)) . q = ((h . (o -term p)) | ((dom (o -term p)) \ I)) . q

then ( (o -term p) . q = [o, the carrier of S] & [o, the carrier of S] = (o -term (h # p)) . q ) by TREES_4:def 4;
hence ((o -term p) | ((dom (o -term p)) \ I)) . q = ((h . (o -term p)) | ((dom (o -term p)) \ I)) . q by A6, B6; :: thesis: verum

end;

suppose ex i being Nat ex T being DecoratedTree ex r being Node of T st
( i < len p & T = p . (i + 1) & q = <*i*> ^ r ) ; :: thesis: ((o -term p) | ((dom (o -term p)) \ I)) . q = ((h . (o -term p)) | ((dom (o -term p)) \ I)) . q

then consider i being Nat, T being DecoratedTree, r being Node of T such that
A7: ( i < len p & T = p . (i + 1) & q = <*i*> ^ r ) ;
( 1 <= i + 1 & i + 1 <= len p ) by A7, NAT_1:12, NAT_1:13;
then A8: i + 1 in dom p by FINSEQ_3:25;
then reconsider T = T as Element of (Free (S,X)) by A7, FUNCT_1:102;
set II = { xi where xi is Node of T : ex s being SortSymbol of S ex x being Element of X . s st T . xi = [x,s] } ;
T in rng p by A7, A8, FUNCT_1:def 3;
then B9: ( dom T c= dom (h . T) & T | ((dom T) \ { xi where xi is Node of T : ex s being SortSymbol of S ex x being Element of X . s st T . xi = [x,s] } ) = (h . T) | ((dom T) \ { xi where xi is Node of T : ex s being SortSymbol of S ex x being Element of X . s st T . xi = [x,s] } ) ) by Z0;
B8: (o -term p) . q = T . r by A7, TREES_4:12;
r nin { xi where xi is Node of T : ex s being SortSymbol of S ex x being Element of X . s st T . xi = [x,s] }

proof

assume r in { xi where xi is Node of T : ex s being SortSymbol of S ex x being Element of X . s st T . xi = [x,s] } ; :: thesis: contradiction
then consider xi being Node of T such that
B7: ( r = xi & ex s being SortSymbol of S ex x being Element of X . s st T . xi = [x,s] ) ;
q in I by A4, B8, B7;
hence contradiction by BB, XBOOLE_0:def 5; :: thesis: verum

end;

then r in (dom T) \ { xi where xi is Node of T : ex s being SortSymbol of S ex x being Element of X . s st T . xi = [x,s] } by XBOOLE_0:def 5;
then A11: ( T . r = (T | ((dom T) \ { xi where xi is Node of T : ex s being SortSymbol of S ex x being Element of X . s st T . xi = [x,s] } )) . r & (T | ((dom T) \ { xi where xi is Node of T : ex s being SortSymbol of S ex x being Element of X . s st T . xi = [x,s] } )) . r = (h . T) . r ) by B9, FUNCT_1:49;
A10: (h # p) . (i + 1) = (h . ((the_arity_of o) /. (i + 1))) . T by A7, A8, MSUALG_3:def 6
.= (h . ((the_arity_of o) /. (i + 1))) . (p /. (i + 1)) by A7, A8, PARTFUN1:def 6
.= (h . (the_sort_of (p /. (i + 1)))) . (p /. (i + 1)) by A8, Th4A
.= h . (p /. (i + 1)) by ABBR
.= h . T by A7, A8, PARTFUN1:def 6 ;
( dom (h # p) = dom (the_arity_of o) & dom (the_arity_of o) = dom p ) by MSUALG_6:2;
then ( len (h # p) = len p & r in dom (h . T) ) by B9, FINSEQ_3:29;
hence ((o -term p) | ((dom (o -term p)) \ I)) . q = ((h . (o -term p)) | ((dom (o -term p)) \ I)) . q by B6, B8, A6, A7, A10, A11, TREES_4:12; :: thesis: verum

end;

end;

end;

thus S₁[t] from MSAFREE5:sch 2(A1, A3); :: thesis: verum