let x be set ; :: thesis: for S being non void Signature
for Y being V8() ManySortedSet of the carrier of S
for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds
x is Term of S,Y

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 s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds
x is Term of S,Y

let Y be V8() ManySortedSet of the carrier of S; :: thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds
x is Term of S,Y

let X be ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds
x is Term of S,Y

let s be SortSymbol of S; :: thesis: ( x in (S -Terms (X,Y)) . s implies x is Term of S,Y )
assume x in (S -Terms (X,Y)) . s ; :: thesis: x is Term of S,Y
then x in { 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
( x = t & the_sort_of t = s & variables_in t c= X ) ;
hence x is Term of S,Y ; :: thesis: verum