let x be set ; :: thesis: for S being non void Signature
for Y being V5() ManySortedSet of
for X being ManySortedSet of the carrier of S
for s being SortSymbol of st x in (S -Terms X,Y) . s holds
x is Term of the carrier of (DTConMSA Y),
let S be non void Signature; :: thesis: for Y being V5() ManySortedSet of
for X being ManySortedSet of the carrier of S
for s being SortSymbol of st x in (S -Terms X,Y) . s holds
x is Term of the carrier of (DTConMSA Y),
let Y be V5() ManySortedSet of ; :: thesis: for X being ManySortedSet of the carrier of S
for s being SortSymbol of st x in (S -Terms X,Y) . s holds
x is Term of the carrier of (DTConMSA Y),
let X be ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of st x in (S -Terms X,Y) . s holds
x is Term of the carrier of (DTConMSA Y),
let s be SortSymbol of ; :: thesis: ( x in (S -Terms X,Y) . s implies x is Term of the carrier of (DTConMSA Y), )
assume x in (S -Terms X,Y) . s ; :: thesis: x is Term of the carrier of (DTConMSA Y),
then x in { t where t is Term of the carrier of (DTConMSA Y), : ( the_sort_of t = s & variables_in t c= X ) } by Def6;
then ex t being Term of the carrier of (DTConMSA Y), st
( x = t & the_sort_of t = s & variables_in t c= X ) ;
hence x is Term of the carrier of (DTConMSA Y), ; :: thesis: verum