let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for t, t1 being Element of (Free (S,X)) st t is x -omitting holds
(t,[x,s]) <- t1 = t
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for t, t1 being Element of (Free (S,X)) st t is x -omitting holds
(t,[x,s]) <- t1 = t
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for t, t1 being Element of (Free (S,X)) st t is x -omitting holds
(t,[x,s]) <- t1 = t
let x be Element of X . s; :: thesis: for t, t1 being Element of (Free (S,X)) st t is x -omitting holds
(t,[x,s]) <- t1 = t
let t, t1 be Element of (Free (S,X)); :: thesis: ( t is x -omitting implies (t,[x,s]) <- t1 = t )
assume A1: Coim (t,[x,s]) = {} ; :: according to MSAFREE5:def 21 :: thesis: (t,[x,s]) <- t1 = t
reconsider dt = dom t as set ;
AA: dom ((t,[x,s]) <- t1) = dt

proof

thus dom ((t,[x,s]) <- t1) c= dt :: according to XBOOLE_0:def 10 :: thesis: dt c= dom ((t,[x,s]) <- t1)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom ((t,[x,s]) <- t1) or a in dt )
assume a in dom ((t,[x,s]) <- t1) ; :: thesis: a in dt
then reconsider r = a as Node of ((t,[x,s]) <- t1) ;

per cases ( r in dom t or ex q being Node of t ex p being Node of t1 st
( q in Leaves (dom t) & t . q = [x,s] & r = q ^ p ) ) by TREES_4:def 7;

suppose r in dom t ; :: thesis: a in dt

hence a in dt ; :: thesis: verum

end;

suppose ex q being Node of t ex p being Node of t1 st
( q in Leaves (dom t) & t . q = [x,s] & r = q ^ p ) ; :: thesis: a in dt

then consider q being Node of t, p being Node of t1 such that
A2: ( q in Leaves (dom t) & t . q = [x,s] & r = q ^ p ) ;
[x,s] in {[x,s]} by TARSKI:def 1;
hence a in dt by A1, A2, FUNCT_1:def 7; :: thesis: verum

end;

end;

end;

thus dt c= dom ((t,[x,s]) <- t1) by TREES_4:def 7; :: thesis: verum

end;

now :: thesis: for a being object st a in dom t holds
((t,[x,s]) <- t1) . a = t . a

let a be object ; :: thesis: ( a in dom t implies ((t,[x,s]) <- t1) . a = t . a )
assume a in dom t ; :: thesis: ((t,[x,s]) <- t1) . a = t . a
then reconsider r = a as Node of t ;
[x,s] in {[x,s]} by TARSKI:def 1;
then t . r <> [x,s] by A1, FUNCT_1:def 7;
hence ((t,[x,s]) <- t1) . a = t . a by TREES_4:def 7; :: thesis: verum

end;

hence (t,[x,s]) <- t1 = t by AA, FUNCT_1:2; :: thesis: verum