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 being Element of X . s
for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t1 = t with-replacement (xi,(x -term)) & t is x -omitting holds
t1 is context of x
let s be SortSymbol of S; :: thesis: 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 t1 = t with-replacement (xi,(x -term)) & t is x -omitting holds
t1 is context of x
let X be V5() ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t1 = t with-replacement (xi,(x -term)) & t is x -omitting holds
t1 is context of x
let x be Element of X . s; :: thesis: for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t1 = t with-replacement (xi,(x -term)) & t is x -omitting holds
t1 is context of x
let t, t1 be Element of (Free (S,X)); :: thesis: for xi being Element of dom t st t1 = t with-replacement (xi,(x -term)) & t is x -omitting holds
t1 is context of x
let xi be Element of dom t; :: thesis: ( t1 = t with-replacement (xi,(x -term)) & t is x -omitting implies t1 is context of x )
assume Z1: t1 = t with-replacement (xi,(x -term)) ; :: thesis: ( not t is x -omitting or t1 is context of x )
assume Z2: t is x -omitting ; :: thesis: t1 is context of x
Coim (t1,[x,s]) = {xi}
proof
thus Coim (t1,[x,s]) c= {xi} :: according to XBOOLE_0:def 10 :: thesis: {xi} c= Coim (t1,[x,s])
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Coim (t1,[x,s]) or a in {xi} )
assume A0: a in Coim (t1,[x,s]) ; :: thesis: a in {xi}
then A1: ( a in dom t1 & t1 . a in {[x,s]} ) by FUNCT_1:def 7;
reconsider nu = a as Element of dom t1 by A0, FUNCT_1:def 7;
nu in dom t1 ;
then A5: ( xi in dom t & nu in (dom t) with-replacement (xi,(dom (x -term))) ) by Z1, TREES_2:def 11;
per cases then ( ( t1 . nu = t . nu & not xi is_a_prefix_of nu ) or ex r being FinSequence of NAT st
( r in dom (x -term) & nu = xi ^ r & t1 . nu = (x -term) . r ) ) by Z1, TREES_2:def 11;
suppose A3: ( t1 . nu = t . nu & not xi is_a_prefix_of nu ) ; :: thesis: a in {xi}
then for r being FinSequence of NAT holds
( not r in dom (x -term) or not nu = xi ^ r ) by TREES_1:1;
then ( [x,s] in {[x,s]} & nu in dom t ) by A5, TARSKI:def 1, TREES_1:def 9;
hence a in {xi} by Z2, A3, A1, FUNCT_1:def 7; :: thesis: verum
end;
suppose ex r being FinSequence of NAT st
( r in dom (x -term) & nu = xi ^ r & t1 . nu = (x -term) . r ) ; :: thesis: a in {xi}
then consider r being FinSequence of NAT such that
A6: ( r in dom (x -term) & nu = xi ^ r & t1 . nu = (x -term) . r ) ;
r in {{}} by A6, TREES_1:29;
then r = {} ;
hence a in {xi} by A6, TARSKI:def 1; :: thesis: verum
end;
end;
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {xi} or a in Coim (t1,[x,s]) )
assume a in {xi} ; :: thesis: a in Coim (t1,[x,s])
then A7: a = xi by TARSKI:def 1;
A9: ( xi in (dom t) with-replacement (xi,(dom (x -term))) & (dom t) with-replacement (xi,(dom (x -term))) = dom t1 ) by Z1, TREES_1:def 9, TREES_2:def 11;
then consider r being FinSequence of NAT such that
A8: ( r in dom (x -term) & xi = xi ^ r & t1 . xi = (x -term) . r ) by Z1, TREES_2:def 11;
r = {} by A8, FINSEQ_1:87;
then ( t1 . xi = [x,s] & [x,s] in {[x,s]} ) by A8, TARSKI:def 1, TREES_4:3;
hence a in Coim (t1,[x,s]) by A7, A9, FUNCT_1:def 7; :: thesis: verum
end;
then card (Coim (t1,[x,s])) = 1 by CARD_1:30;
hence t1 is context of x by CONTEXT; :: thesis: verum