let C be initialized standardized ConstructorSignature; :: thesis: for e being expression of C st (e . {}) `1 in Vars holds
ex x being Element of Vars st
( x = (e . {}) `1 & e = x -term C )
let t be expression of C; :: thesis: ( (t . {}) `1 in Vars implies ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C ) )
assume A1: (t . {}) `1 in Vars ; :: thesis: ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C )
set X = MSVars C;
set V = (MSVars C) (\/) ( the carrier of C --> {0});
reconsider q = t as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
per cases ( q . {} in [: the carrier' of C,{ the carrier of C}:] or ex s being SortSymbol of C ex v being Element of ((MSVars C) (\/) ( the carrier of C --> {0})) . s st q . {} = [v,s] ) by MSATERM:2;
suppose q . {} in [: the carrier' of C,{ the carrier of C}:] ; :: thesis: ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C )
then ( (q . {}) `1 in the carrier' of C & the carrier' of C misses Vars ) by Th10, MCART_1:10;
hence ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C ) by A1, XBOOLE_0:3; :: thesis: verum
end;
suppose ex s being SortSymbol of C ex v being Element of ((MSVars C) (\/) ( the carrier of C --> {0})) . s st q . {} = [v,s] ; :: thesis: ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C )
then consider s being SortSymbol of C, v being Element of ((MSVars C) (\/) ( the carrier of C --> {0})) . s such that
A2: t . {} = [v,s] ;
A3: q = root-tree [v,s] by A2, MSATERM:5;
reconsider x = v as Element of Vars by A1, A2;
take x ; :: thesis: ( x = (t . {}) `1 & t = x -term C )
the carrier of C = {a_Type,an_Adj,a_Term} by ABCMIZ_1:def 9;
then A4: ( s = a_Term or s = a_Type or s = an_Adj ) by ENUMSET1:def 1;
( the carrier of C --> {0}) . s = {0} ;
then ((MSVars C) (\/) ( the carrier of C --> {0})) . s = ((MSVars C) . s) \/ {0} by PBOOLE:def 4;
then A5: ( s = a_Term or ((MSVars C) (\/) ( the carrier of C --> {0})) . s = {} \/ {0} ) by A4, ABCMIZ_1:def 25;
( v in ((MSVars C) (\/) ( the carrier of C --> {0})) . s & x <> 0 ) ;
hence ( x = (t . {}) `1 & t = x -term C ) by A2, A3, A5; :: thesis: verum
end;
end;