set D = DTConMSA X;
set OU = [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X));
consider p being FinSequence such that
A2: t ==> p by A1;
A3: [t,p] in the Rules of (DTConMSA X) by A2, LANG1:def 1;
reconsider a = t as Element of [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) ;
reconsider p = p as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by A3, 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
A4: a = [o,x2] by DOMAIN_1:9;
take o ; :: thesis: [o,the carrier of S] = t
thus [o,the carrier of S] = t by A4, TARSKI:def 1; :: thesis: verum