let x be set ; 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; 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; 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; 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; ( x in (S -Terms (X,Y)) . s implies x is Term of S,Y )
assume
x in (S -Terms (X,Y)) . s
; 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
; verum