let S be non empty non void ManySortedSign ; for X being ManySortedSet of the carrier of S
for t being set holds
( ( t in Terminals (DTConMSA X) & 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 (DTConMSA X) ) )
let X be ManySortedSet of the carrier of S; for t being set holds
( ( t in Terminals (DTConMSA X) & 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 (DTConMSA X) ) )
let t be set ; ( ( t in Terminals (DTConMSA X) & 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 (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 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 (DTConMSA X)proof
assume that A3:
t in Terminals (DTConMSA X)
and A4:
X is
V5()
;
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
;
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 A9;
verum
end;
let s be SortSymbol of S; for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X)
let x be set ; ( x in X . s implies [x,s] in Terminals (DTConMSA X) )
assume A10:
x in X . s
; [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; verum