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 (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; :: thesis: 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 ; :: thesis: ( ( 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] ) ) :: thesis: for s being SortSymbol of S

for x being set st x in X . s holds

[x,s] in Terminals (DTConMSA X)

[x,s] in Terminals (DTConMSA X)

let x be set ; :: thesis: ( x in X . s implies [x,s] in Terminals (DTConMSA X) )

assume A10: x in X . s ; :: thesis: [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; :: thesis: verum

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; :: thesis: 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 ; :: thesis: ( ( 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] ) ) :: thesis: for s being SortSymbol of S

for x being set st x in X . s holds

[x,s] in Terminals (DTConMSA X)

proof

let s be SortSymbol of S; :: thesis: for x being set st x in X . s holds
assume that

A3: t in Terminals (DTConMSA X) 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 (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 ; :: 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;A3: t in Terminals (DTConMSA X) 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 (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 ; :: 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

[x,s] in Terminals (DTConMSA X)

let x be set ; :: thesis: ( x in X . s implies [x,s] in Terminals (DTConMSA X) )

assume A10: x in X . s ; :: thesis: [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; :: thesis: verum