let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S holds union (rng (FreeSort X)) = TS (DTConMSA X)

let X be V5() ManySortedSet of the carrier of S; :: thesis: union (rng (FreeSort X)) = TS (DTConMSA X)

set D = DTConMSA X;

A1: dom (FreeSort X) = the carrier of S by PARTFUN1:def 2;

thus union (rng (FreeSort X)) c= TS (DTConMSA X) :: according to XBOOLE_0:def 10 :: thesis: TS (DTConMSA X) c= union (rng (FreeSort X))

assume x in TS (DTConMSA X) ; :: thesis: x in union (rng (FreeSort X))

then reconsider t = x as Element of TS (DTConMSA X) ;

A6: ( rng t c= the carrier of (DTConMSA X) & the carrier of (DTConMSA X) = (Terminals (DTConMSA X)) \/ (NonTerminals (DTConMSA X)) ) by LANG1:1, RELAT_1:def 19;

{} in dom t by TREES_1:22;

then A7: t . {} in rng t by FUNCT_1:def 3;

A8: NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] by Th6;

A9: Terminals (DTConMSA X) = Union (coprod X) by Th6;

let X be V5() ManySortedSet of the carrier of S; :: thesis: union (rng (FreeSort X)) = TS (DTConMSA X)

set D = DTConMSA X;

A1: dom (FreeSort X) = the carrier of S by PARTFUN1:def 2;

thus union (rng (FreeSort X)) c= TS (DTConMSA X) :: according to XBOOLE_0:def 10 :: thesis: TS (DTConMSA X) c= union (rng (FreeSort X))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TS (DTConMSA X) or x in union (rng (FreeSort X)) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng (FreeSort X)) or x in TS (DTConMSA X) )

assume x in union (rng (FreeSort X)) ; :: thesis: x in TS (DTConMSA X)

then consider A being set such that

A2: x in A and

A3: A in rng (FreeSort X) by TARSKI:def 4;

consider s being object such that

A4: s in dom (FreeSort X) and

A5: (FreeSort X) . s = A by A3, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A4;

A = FreeSort (X,s) by A5, Def11

.= { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) } ;

then ex a being Element of TS (DTConMSA X) st

( a = x & ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) ) by A2;

hence x in TS (DTConMSA X) ; :: thesis: verum

end;assume x in union (rng (FreeSort X)) ; :: thesis: x in TS (DTConMSA X)

then consider A being set such that

A2: x in A and

A3: A in rng (FreeSort X) by TARSKI:def 4;

consider s being object such that

A4: s in dom (FreeSort X) and

A5: (FreeSort X) . s = A by A3, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A4;

A = FreeSort (X,s) by A5, Def11

.= { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) } ;

then ex a being Element of TS (DTConMSA X) st

( a = x & ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) ) by A2;

hence x in TS (DTConMSA X) ; :: thesis: verum

assume x in TS (DTConMSA X) ; :: thesis: x in union (rng (FreeSort X))

then reconsider t = x as Element of TS (DTConMSA X) ;

A6: ( rng t c= the carrier of (DTConMSA X) & the carrier of (DTConMSA X) = (Terminals (DTConMSA X)) \/ (NonTerminals (DTConMSA X)) ) by LANG1:1, RELAT_1:def 19;

{} in dom t by TREES_1:22;

then A7: t . {} in rng t by FUNCT_1:def 3;

A8: NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] by Th6;

A9: Terminals (DTConMSA X) = Union (coprod X) by Th6;

per cases
( t . {} in Terminals (DTConMSA X) or t . {} in NonTerminals (DTConMSA X) )
by A7, A6, XBOOLE_0:def 3;

end;

suppose A10:
t . {} in Terminals (DTConMSA X)
; :: thesis: x in union (rng (FreeSort X))

then reconsider a = t . {} as Terminal of (DTConMSA X) ;

a in union (rng (coprod X)) by A9, A10, CARD_3:def 4;

then consider A being set such that

A11: a in A and

A12: A in rng (coprod X) by TARSKI:def 4;

consider s being object such that

A13: s in dom (coprod X) and

A14: (coprod X) . s = A by A12, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A13;

A = coprod (s,X) by A14, Def3;

then ( t = root-tree a & ex b being set st

( b in X . s & a = [b,s] ) ) by A11, Def2, DTCONSTR:9;

then t in FreeSort (X,s) ;

then A15: t in (FreeSort X) . s by Def11;

(FreeSort X) . s in rng (FreeSort X) by A1, FUNCT_1:def 3;

hence x in union (rng (FreeSort X)) by A15, TARSKI:def 4; :: thesis: verum

end;a in union (rng (coprod X)) by A9, A10, CARD_3:def 4;

then consider A being set such that

A11: a in A and

A12: A in rng (coprod X) by TARSKI:def 4;

consider s being object such that

A13: s in dom (coprod X) and

A14: (coprod X) . s = A by A12, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A13;

A = coprod (s,X) by A14, Def3;

then ( t = root-tree a & ex b being set st

( b in X . s & a = [b,s] ) ) by A11, Def2, DTCONSTR:9;

then t in FreeSort (X,s) ;

then A15: t in (FreeSort X) . s by Def11;

(FreeSort X) . s in rng (FreeSort X) by A1, FUNCT_1:def 3;

hence x in union (rng (FreeSort X)) by A15, TARSKI:def 4; :: thesis: verum

suppose
t . {} in NonTerminals (DTConMSA X)
; :: thesis: x in union (rng (FreeSort X))

then reconsider a = t . {} as NonTerminal of (DTConMSA X) ;

consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that

A16: a = [o,x2] by A8, DOMAIN_1:1;

set rs = the_result_sort_of o;

x2 = the carrier of S by TARSKI:def 1;

then t in FreeSort (X,(the_result_sort_of o)) by A16;

then A17: t in (FreeSort X) . (the_result_sort_of o) by Def11;

(FreeSort X) . (the_result_sort_of o) in rng (FreeSort X) by A1, FUNCT_1:def 3;

hence x in union (rng (FreeSort X)) by A17, TARSKI:def 4; :: thesis: verum

end;consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that

A16: a = [o,x2] by A8, DOMAIN_1:1;

set rs = the_result_sort_of o;

x2 = the carrier of S by TARSKI:def 1;

then t in FreeSort (X,(the_result_sort_of o)) by A16;

then A17: t in (FreeSort X) . (the_result_sort_of o) by Def11;

(FreeSort X) . (the_result_sort_of o) in rng (FreeSort X) by A1, FUNCT_1:def 3;

hence x in union (rng (FreeSort X)) by A17, TARSKI:def 4; :: thesis: verum