let S be non void Signature; :: thesis: for Y being V5() ManySortedSet of
for X being ManySortedSet of
for t being Term of S,Y
for s being SortSymbol of S st t in (S -Terms X,Y) . s holds
( the_sort_of t = s & variables_in t c= X )
let Y be V5() ManySortedSet of ; :: thesis: for X being ManySortedSet of
for t being Term of S,Y
for s being SortSymbol of S st t in (S -Terms X,Y) . s holds
( the_sort_of t = s & variables_in t c= X )
let X be ManySortedSet of ; :: thesis: for t being Term of S,Y
for s being SortSymbol of S st t in (S -Terms X,Y) . s holds
( the_sort_of t = s & variables_in t c= X )
let q be Term of S,Y; :: thesis: for s being SortSymbol of S st q in (S -Terms X,Y) . s holds
( the_sort_of q = s & variables_in q c= X )
let s be SortSymbol of S; :: thesis: ( q in (S -Terms X,Y) . s implies ( the_sort_of q = s & variables_in q c= X ) )
assume A1: q in (S -Terms X,Y) . s ; :: thesis: ( the_sort_of q = s & variables_in q c= X )
(S -Terms X,Y) . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } by Def6;
then ex t being Term of S,Y st
( q = t & the_sort_of t = s & variables_in t c= X ) by A1;
hence ( the_sort_of q = s & variables_in q c= X ) ; :: thesis: verum