let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S
for t being set holds
( ( 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] ) ) & ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )
let X be ManySortedSet of the carrier of S; :: thesis: for t being set holds
( ( 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] ) ) & ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )
let t be set ; :: thesis: ( ( 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] ) ) & ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )
set D = DTConMSA X;
A1: Union (coprod X) c= Terminals (DTConMSA X) by Th6;
A2: 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: for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X)

proof

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

end;

let s be SortSymbol of S; :: thesis: for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X)
let x be set ; :: thesis: ( x in X . s implies [x,s] in Terminals (DTConMSA X) )
assume A10: x in X . s ; :: thesis: [x,s] in Terminals (DTConMSA X)
set t = [x,s];
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then A11: (coprod X) . s in rng (coprod X) by FUNCT_1:def 3;
[x,s] in coprod (s,X) by A10, Def2;
then [x,s] in (coprod X) . s by Def3;
then [x,s] in Union (coprod X) by A2, A11, TARSKI:def 4;
hence [x,s] in Terminals (DTConMSA X) by A1; :: thesis: verum