let a be object ; for S being 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 being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom t)
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 being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom 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 being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom t)
let X be V5() ManySortedSet of the carrier of S; for x being Element of X . s
for t being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom t)
let x be Element of X . s; for t being Element of (Free (S,X)) st t . a = [x,s] holds
a in Leaves (dom t)
let t be Element of (Free (S,X)); ( t . a = [x,s] implies a in Leaves (dom t) )
assume Z0:
t . a = [x,s]
; a in Leaves (dom t)
then reconsider q = a as Element of dom t by FUNCT_1:def 2;
reconsider v = t | q as Element of (Free (S,X)) by MSAFREE4:44;
{} in (dom t) | q
by TREES_1:22;
then A2:
v . {} = t . (q ^ (<*> NAT))
by TREES_2:def 10;