let S be OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
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 V5() ManySortedSet of ; :: 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 & A in rng (coprod X) ) by A1, TARSKI:def 4;
consider s being set such that
A3: ( s in dom (coprod X) & (coprod X) . s = A ) by A2, FUNCT_1:def 5;
reconsider s = s as Element of S by A3, PARTFUN1:def 4;
take s ; :: thesis: ex x being set st
( x in X . s & t = [x,s] )
(coprod X) . s = coprod s,X by MSAFREE:def 3;
then consider x being set such that
A4: ( x in X . s & t = [x,s] ) by A2, A3, MSAFREE:def 2;
take x ; :: thesis: ( x in X . s & t = [x,s] )
thus ( x in X . s & t = [x,s] ) by A4; :: thesis: verum

end;

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