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)) st the_sort_of t = s holds
(x -term) -sub t = t
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)) st the_sort_of t = s holds
(x -term) -sub t = t
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)) st the_sort_of t = s holds
(x -term) -sub t = t
let x be Element of X . s; :: thesis: for t being Element of (Free (S,X)) st the_sort_of t = s holds
(x -term) -sub t = t
let t be Element of (Free (S,X)); :: thesis: ( the_sort_of t = s implies (x -term) -sub t = t )
assume the_sort_of t = s ; :: thesis: (x -term) -sub t = t
hence (x -term) -sub t = ((x -term),[x,s]) <- t by SUB
.= t ;
:: thesis: verum