let S be non void Signature; :: thesis: for Y being non-empty ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
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 non-empty ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S
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 the carrier of S; :: 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 Def5;
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