set D = DTConMSA X;
set OU = [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X));
reconsider a = t as Element of [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) ;
consider p being FinSequence such that
A2: t ==> p by A1;
[t,p] in the Rules of (DTConMSA X) by A2, LANG1:def 1;
then reconsider p = p as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:106;
[a,p] in REL X by A2, LANG1:def 1;
then a in [:the carrier' of S,{the carrier of S}:] by Def9;
then consider o being OperSymbol of S, x2 being Element of {the carrier of S} such that
A3: a = [o,x2] by DOMAIN_1:9;
take o ; :: thesis: [o,the carrier of S] = t
thus [o,the carrier of S] = t by A3, TARSKI:def 1; :: thesis: verum