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)) st t is x -omitting holds
(t,[x,s]) <- t1 = t
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)) st t is x -omitting holds
(t,[x,s]) <- t1 = t
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)) st t is x -omitting holds
(t,[x,s]) <- t1 = t
let x be 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 t, t1 be Element of (Free (S,X)); ( t is x -omitting implies (t,[x,s]) <- t1 = t )
assume A1:
Coim (t,[x,s]) = {}
; MSAFREE5:def 21 (t,[x,s]) <- t1 = t
reconsider dt = dom t as set ;
AA:
dom ((t,[x,s]) <- t1) = dt
now for a being object st a in dom t holds
((t,[x,s]) <- t1) . a = t . alet a be
object ;
( a in dom t implies ((t,[x,s]) <- t1) . a = t . a )assume
a in dom t
;
((t,[x,s]) <- t1) . a = t . athen 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;
verum end;
hence
(t,[x,s]) <- t1 = t
by AA, FUNCT_1:2; verum