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 A2: (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:9;

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 Lem3, MCART_1:10;
hence ex x being Element of Vars st
( x = (t . {} ) `1 & t = x -term C ) by A2, 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
A3: t . {} = [v,s] ;
A4: q = root-tree [v,s] by A3, MSATERM:5;
reconsider x = v as Element of Vars by A2, A3, MCART_1:7;
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 A6: ( s = a_Term or s = a_Type or s = an_Adj ) by ENUMSET1:def 1;
(the carrier of C --> {0 }) . s = {0 } by FUNCOP_1:13;
then ((MSVars C) \/ (the carrier of C --> {0 })) . s = ((MSVars C) . s) \/ {0 } by PBOOLE:def 7;
then A7: ( s = a_Term or ((MSVars C) \/ (the carrier of C --> {0 })) . s = {} \/ {0 } ) by A6, 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 A3, MCART_1:7, A4, A7; :: thesis: verum

end;

end;