let S be non void Signature; :: thesis: for Y being V8() 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 V8() 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

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 V8() 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