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 being Element of (Free (S,X))
for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
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 being Element of (Free (S,X))
for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
let X be V5() ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for t being Element of (Free (S,X))
for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
let x be Element of X . s; :: thesis: for t being Element of (Free (S,X))
for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
let t be Element of (Free (S,X)); :: thesis: for xi being Node of t st t . xi = [x,s] holds
t | xi = x -term
let xi be Node of t; :: thesis: ( t . xi = [x,s] implies t | xi = x -term )
assume Z0: t . xi = [x,s] ; :: thesis: t | xi = x -term
reconsider tx = t | xi as Element of (Free (S,X)) by MSAFREE4:44;