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:87;
[a,p] in REL X by A2, LANG1:def 1;
then a in [: the carrier' of S,{ the carrier of S}:] by Def7;
then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A3: a = [o,x2] by DOMAIN_1:1;
take o ; :: thesis: [o, the carrier of S] = t
thus [o, the carrier of S] = t by A3, TARSKI:def 1; :: thesis: verum