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
; [o, the carrier of S] = t
thus
[o, the carrier of S] = t
by A3, TARSKI:def 1; verum