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

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