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

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