let S be non empty non void ManySortedSign ; :: thesis: for Y being infinite-yielding ManySortedSet of the carrier of S
for v, v1 being Element of (Free (S,Y))
for h being Endomorphism of Free (S,Y)
for g being one-to-one FinSequence of dom v st rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom v c= dom v1 & v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) & ( for i being Nat st i in dom g holds
(h . v) | (g /. i) = v1 | (g /. i) ) holds
h . v = v1
let Y be infinite-yielding ManySortedSet of the carrier of S; :: thesis: for v, v1 being Element of (Free (S,Y))
for h being Endomorphism of Free (S,Y)
for g being one-to-one FinSequence of dom v st rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom v c= dom v1 & v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) & ( for i being Nat st i in dom g holds
(h . v) | (g /. i) = v1 | (g /. i) ) holds
h . v = v1
let v, v1 be Element of (Free (S,Y)); :: thesis: for h being Endomorphism of Free (S,Y)
for g being one-to-one FinSequence of dom v st rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom v c= dom v1 & v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) & ( for i being Nat st i in dom g holds
(h . v) | (g /. i) = v1 | (g /. i) ) holds
h . v = v1
let h be Endomorphism of Free (S,Y); :: thesis: for g being one-to-one FinSequence of dom v st rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom v c= dom v1 & v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) & ( for i being Nat st i in dom g holds
(h . v) | (g /. i) = v1 | (g /. i) ) holds
h . v = v1
let g be one-to-one FinSequence of dom v; :: thesis: ( rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom v c= dom v1 & v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) & ( for i being Nat st i in dom g holds
(h . v) | (g /. i) = v1 | (g /. i) ) implies h . v = v1 )
assume Z0: rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } ; :: thesis: ( not dom v c= dom v1 or not v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) or ex i being Nat st
( i in dom g & not (h . v) | (g /. i) = v1 | (g /. i) ) or h . v = v1 )
assume Z1: dom v c= dom v1 ; :: thesis: ( not v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) or ex i being Nat st
( i in dom g & not (h . v) | (g /. i) = v1 | (g /. i) ) or h . v = v1 )
assume v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) ; :: thesis: ( ex i being Nat st
( i in dom g & not (h . v) | (g /. i) = v1 | (g /. i) ) or h . v = v1 )
then A5: (h . v) | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) by Z0, Th135;
assume Z3: for i being Nat st i in dom g holds
(h . v) | (g /. i) = v1 | (g /. i) ; :: thesis: h . v = v1
h . v c= v1

proof

let a be object ; :: according to RELAT_1:def 3 :: thesis: for b₁ being object holds
( not [a,b₁] in h . v or [a,b₁] in v1 )
let b be object ; :: thesis: ( not [a,b] in h . v or [a,b] in v1 )
assume [a,b] in h . v ; :: thesis: [a,b] in v1
then A1: ( a in dom (h . v) & b = (h . v) . a ) by FUNCT_1:1;

per cases then ( a in (dom v) \ (rng g) or ex nu being Element of dom v st
( nu in rng g & ex mu being Node of ((h . v) | nu) st a = nu ^ mu ) ) by Z0, Th137;

suppose a in (dom v) \ (rng g) ; :: thesis: [a,b] in v1

then A2: ( ((h . v) | ((dom v) \ (rng g))) . a = (h . v) . a & a in dom v & (v1 | ((dom v) \ (rng g))) . a = v1 . a ) by FUNCT_1:49;
thus [a,b] in v1 by Z1, A5, A1, A2, FUNCT_1:1; :: thesis: verum

end;

suppose ex nu being Element of dom v st
( nu in rng g & ex mu being Node of ((h . v) | nu) st a = nu ^ mu ) ; :: thesis: [a,b] in v1

then consider nu being Element of dom v, mu being Node of ((h . v) | nu) such that
A3: ( nu in rng g & a = nu ^ mu ) ;
consider i being object such that
A6: ( i in dom g & nu = g . i ) by A3, FUNCT_1:def 3;
reconsider i = i as Nat by A6;
nu = g /. i by A6, PARTFUN1:def 6;
then A7: (h . v) | nu = v1 | nu by A6, Z3;
A8: ( nu in dom v & dom v c= dom (h . v) ) by Th135;
( mu in dom ((h . v) | nu) & dom ((h . v) | nu) = (dom (h . v)) | nu & dom (v1 | nu) = (dom v1) | nu ) by TREES_2:def 10;
then ( b = ((h . v) | nu) . mu & ((h . v) | nu) . mu = v1 . a & a in dom v1 ) by Z1, A7, A1, A3, A8, TREES_1:def 6, TREES_2:def 10;
hence [a,b] in v1 by FUNCT_1:1; :: thesis: verum

end;

end;

end;

hence h . v = v1 by Th136; :: thesis: verum