let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x, x1 being Element of X . s
for t being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] holds
dom t = dom (t with-replacement (xi,(x1 -term)))
let s be SortSymbol of S; :: thesis: for X being V5() ManySortedSet of the carrier of S
for x, x1 being Element of X . s
for t being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] holds
dom t = dom (t with-replacement (xi,(x1 -term)))
let X be V5() ManySortedSet of the carrier of S; :: thesis: for x, x1 being Element of X . s
for t being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] holds
dom t = dom (t with-replacement (xi,(x1 -term)))
let x, x1 be Element of X . s; :: thesis: for t being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] holds
dom t = dom (t with-replacement (xi,(x1 -term)))
let t be Element of (Free (S,X)); :: thesis: for xi being Element of dom t st t . xi = [x,s] holds
dom t = dom (t with-replacement (xi,(x1 -term)))
set t1 = x1 -term ;
let xi be Element of dom t; :: thesis: ( t . xi = [x,s] implies dom t = dom (t with-replacement (xi,(x1 -term))) )
assume t . xi = [x,s] ; :: thesis: dom t = dom (t with-replacement (xi,(x1 -term)))
then A0: dom t c= dom (t with-replacement (xi,(x1 -term))) by Lem11;
dom (t with-replacement (xi,(x1 -term))) c= dom t
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (t with-replacement (xi,(x1 -term))) or a in dom t )
assume a in dom (t with-replacement (xi,(x1 -term))) ; :: thesis: a in dom t
then reconsider q = a as Element of dom (t with-replacement (xi,(x1 -term))) ;
dom (t with-replacement (xi,(x1 -term))) = (dom t) with-replacement (xi,(dom (x1 -term))) by TREES_2:def 11;
per cases then ( q in dom t or ex r being FinSequence of NAT st
( r in dom (x1 -term) & q = xi ^ r ) ) by TREES_1:def 9;
suppose ex r being FinSequence of NAT st
( r in dom (x1 -term) & q = xi ^ r ) ; :: thesis: a in dom t
then consider r being FinSequence of NAT such that
A1: ( r in dom (x1 -term) & q = xi ^ r ) ;
r in {{}} by A1, TREES_1:29;
then r = {} ;
hence a in dom t by A1; :: thesis: verum
end;
end;
end;
hence dom t = dom (t with-replacement (xi,(x1 -term))) by A0, XBOOLE_0:def 10; :: thesis: verum