let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty 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 non-empty 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:22;
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