let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] holds
dom t c= dom (t with-replacement (xi,t1))
let s be SortSymbol of S; for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] holds
dom t c= dom (t with-replacement (xi,t1))
let X be V5() ManySortedSet of the carrier of S; for x being Element of X . s
for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] holds
dom t c= dom (t with-replacement (xi,t1))
let x be Element of X . s; for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] holds
dom t c= dom (t with-replacement (xi,t1))
let t, t1 be Element of (Free (S,X)); for xi being Element of dom t st t . xi = [x,s] holds
dom t c= dom (t with-replacement (xi,t1))
let xi be Element of dom t; ( t . xi = [x,s] implies dom t c= dom (t with-replacement (xi,t1)) )
assume Z0:
t . xi = [x,s]
; dom t c= dom (t with-replacement (xi,t1))
let a be object ; TARSKI:def 3 ( not a in dom t or a in dom (t with-replacement (xi,t1)) )
assume
a in dom t
; a in dom (t with-replacement (xi,t1))
then reconsider q = a as Element of dom t ;
xi in Leaves (dom t)
by Z0, Lem13;
then
not xi c< q
by TREES_1:def 5;
then
q in (dom t) with-replacement (xi,(dom t1))
by TREES_1:def 9;
hence
a in dom (t with-replacement (xi,t1))
by TREES_2:def 11; verum