let S be non empty non void ManySortedSign ; 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; 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)); 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); 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; ( 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] }
; ( 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
; ( 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))
; ( 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)
; h . v = v1
h . v c= v1
proof
let a be
object ;
RELAT_1:def 3 for b1 being object holds
( not [a,b1] in h . v or [a,b1] in v1 )let b be
object ;
( not [a,b] in h . v or [a,b] in v1 )
assume
[a,b] in h . v
;
[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
ex
nu being
Element of
dom v st
(
nu in rng g & ex
mu being
Node of
((h . v) | nu) st
a = nu ^ mu )
;
[a,b] in v1then 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;
verum end;
end;
hence
h . v = v1
by Th136; verum