let S be non empty non void ManySortedSign ; for V being V2() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V holds
( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or 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 V2() ManySortedSet of the carrier of S; for A being MSAlgebra over S
for t being c-Term of A,V holds
( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or 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 A be MSAlgebra over S; for t being c-Term of A,V holds
( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or 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 c-Term of A,V; ( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or 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 ( the Sorts of A (\/) V);
A1:
the carrier of (DTConMSA ( the Sorts of A (\/) V)) = (Terminals (DTConMSA ( the Sorts of A (\/) V))) \/ (NonTerminals (DTConMSA ( the Sorts of A (\/) V)))
by LANG1:1;
reconsider e = {} as Node of t by TREES_1:22;
NonTerminals (DTConMSA ( the Sorts of A (\/) V)) = [: the carrier' of S,{ the carrier of S}:]
by MSAFREE:6;
then
( t . e in Terminals (DTConMSA ( the Sorts of A (\/) 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 x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or 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 Lm4; verum