let S be non empty non void ManySortedSign ; :: thesis: for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V holds
( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [:the carrier' of S,{the carrier of S}:] )
let V be V16() ManySortedSet of the carrier of S; :: thesis: for t being Term of S,V holds
( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [:the carrier' of S,{the carrier of S}:] )
let t be Term of S,V; :: thesis: ( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [:the carrier' of S,{the carrier of S}:] )
set G = DTConMSA V;
A1: the carrier of (DTConMSA V) = (Terminals (DTConMSA V)) \/ (NonTerminals (DTConMSA V)) by LANG1:1;
reconsider e = {} as Node of t by TREES_1:47;
NonTerminals (DTConMSA V) = [:the carrier' of S,{the carrier of S}:] by MSAFREE:6;
then ( t . e in Terminals (DTConMSA V) or t . e in [:the carrier' of S,{the carrier of S}:] ) by A1, XBOOLE_0:def 3;
hence ( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [:the carrier' of S,{the carrier of S}:] ) by Lm3; :: thesis: verum