let S be OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for t being set holds
( t in Terminals (DTConOSA X) iff ex s being Element of S ex x being set st
( x in X . s & t = [x,s] ) )
let X be non-empty ManySortedSet of S; :: thesis: for t being set holds
( t in Terminals (DTConOSA X) iff ex s being Element of S ex x being set st
( x in X . s & t = [x,s] ) )
let t be set ; :: thesis: ( t in Terminals (DTConOSA X) iff ex s being Element of S ex x being set st
( x in X . s & t = [x,s] ) )
set D = DTConOSA X;
A1: Terminals (DTConOSA X) = Union (coprod X) by Th3
.= union (rng (coprod X)) by CARD_3:def 4 ;
thus ( t in Terminals (DTConOSA X) implies ex s being Element of S ex x being set st
( x in X . s & t = [x,s] ) ) :: thesis: ( ex s being Element of S ex x being set st
( x in X . s & t = [x,s] ) implies t in Terminals (DTConOSA X) )

proof

assume t in Terminals (DTConOSA X) ; :: thesis: ex s being Element of S ex x being set st
( x in X . s & t = [x,s] )
then consider A being set such that
A2: t in A and
A3: A in rng (coprod X) by A1, TARSKI:def 4;
consider s being object such that
A4: s in dom (coprod X) and
A5: (coprod X) . s = A by A3, FUNCT_1:def 3;
reconsider s = s as Element of S by A4;
(coprod X) . s = coprod (s,X) by MSAFREE:def 3;
then consider x being set such that
A6: x in X . s and
A7: t = [x,s] by A2, A5, MSAFREE:def 2;
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 A6, A7; :: thesis: verum

end;

given s being Element of S, x being set such that A8: x in X . s and
A9: t = [x,s] ; :: thesis: t in Terminals (DTConOSA X)
t in coprod (s,X) by A8, A9, MSAFREE:def 2;
then A10: t in (coprod X) . s by MSAFREE:def 3;
dom (coprod X) = the carrier of S by PARTFUN1:def 2;
then (coprod X) . s in rng (coprod X) by FUNCT_1:def 3;
hence t in Terminals (DTConOSA X) by A1, A10, TARSKI:def 4; :: thesis: verum