let S be non empty non void ManySortedSign ; :: thesis:
let X be ManySortedSet of ; :: thesis:
let t be set ; :: thesis:
set D = DTConMSA X;
A1: Union (coprod X) = union (rng (coprod X)) by CARD_3:def 4;
thus ( t in Terminals (DTConMSA X) & X is non-empty implies ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] ) ) :: thesis:

assume A2: ( t in Terminals (DTConMSA X) & X is non-empty ) ; :: thesis:
then Terminals (DTConMSA X) = Union (coprod X) by Th6;
then consider A being set such that
A3: ( t in A & A in rng (coprod X) ) by A1, A2, TARSKI:def 4;
consider s being set such that
A4: ( s in dom (coprod X) & (coprod X) . s = A ) by A3, FUNCT_1:def 5;
reconsider s = s as SortSymbol of S by A4, PARTFUN1:def 4;
take s ; :: thesis:
(coprod X) . s = coprod s,X by Def3;
then consider x being set such that
A5: ( x in X . s & t = [x,s] ) by A3, A4, Def2;
take x ; :: thesis:
thus ( x in X . s & t = [x,s] ) by A5; :: thesis:

end;

let s be SortSymbol of S; :: thesis:
let x be set ; :: thesis:
assume A6: x in X . s ; :: thesis:
set t = [x,s];
[x,s] in coprod s,X by A6, Def2;
then A7: [x,s] in (coprod X) . s by Def3;
dom (coprod X) = the carrier of S by PARTFUN1:def 4;
then (coprod X) . s in rng (coprod X) by FUNCT_1:def 5;
then ( [x,s] in Union (coprod X) & Union (coprod X) c= Terminals (DTConMSA X) ) by A1, A7, Th6, TARSKI:def 4;
hence [x,s] in Terminals (DTConMSA X) ; :: thesis: