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