let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty 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 non-empty ManySortedSet of the carrier of S; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: verum