let S be OrderSortedSign; for X being V2() 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 V2() 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 t be set ; ( 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] ) )
( 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)
;
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
;
ex x being set st
( x in X . s & t = [x,s] )
take
x
;
( x in X . s & t = [x,s] )
thus
(
x in X . s &
t = [x,s] )
by A6, A7;
verum
end;
given s being Element of S, x being set such that A8:
x in X . s
and
A9:
t = [x,s]
; 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; verum