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 () & X is V5() 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 () ) )

let X be ManySortedSet of the carrier of S; :: thesis: for t being set holds
( ( t in Terminals () & X is V5() 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 () ) )

let t be set ; :: thesis: ( ( t in Terminals () & X is V5() 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 () ) )

set D = DTConMSA X;
A1: Union () c= Terminals () by Th6;
A2: Union () = union (rng ()) by CARD_3:def 4;
thus ( t in Terminals () & X is V5() 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 ()
proof
assume that
A3: t in Terminals () and
A4: X is V5() ; :: thesis: ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] )

Terminals () = Union () by ;
then consider A being set such that
A5: t in A and
A6: A in rng () by ;
consider s being object such that
A7: s in dom () and
A8: (coprod X) . s = A by ;
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 ()

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