let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
for A being MSAlgebra of 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 V5() ManySortedSet of ; :: thesis: for A being MSAlgebra of 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 of 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: NonTerminals (DTConMSA (the Sorts of A \/ V)) = [:the carrier' of S,{the carrier of S}:] by MSAFREE:6;
A2: 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:47;
( t . e in Terminals (DTConMSA (the Sorts of A \/ V)) or t . e in [:the carrier' of S,{the carrier of S}:] ) by A1, A2, 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