let S be OrderSortedSign; :: thesis: for X being V5() ManySortedSet of holds union (rng (ParsedTerms X)) = TS (DTConOSA X)
let X be V5() ManySortedSet of ; :: thesis: union (rng (ParsedTerms X)) = TS (DTConOSA X)
set D = DTConOSA X;
A1: ( dom (ParsedTerms X) = the carrier of S & dom (coprod X) = the carrier of S ) by PARTFUN1:def 4;
thus union (rng (ParsedTerms X)) c= TS (DTConOSA X) :: according to XBOOLE_0:def 10 :: thesis: TS (DTConOSA X) c= union (rng (ParsedTerms X))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng (ParsedTerms X)) or x in TS (DTConOSA X) )
assume x in union (rng (ParsedTerms X)) ; :: thesis: x in TS (DTConOSA X)
then consider A being set such that
A2: ( x in A & A in rng (ParsedTerms X) ) by TARSKI:def 4;
consider s being set such that
A3: ( s in dom (ParsedTerms X) & (ParsedTerms X) . s = A ) by A2, FUNCT_1:def 5;
reconsider s = s as Element of S by A3, PARTFUN1:def 4;
A = ParsedTerms X,s by A3, Def8
.= { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o1 being OperSymbol of S st
( [o1,the carrier of S] = a . {} & the_result_sort_of o1 <= s ) ) } ;
then consider a being Element of TS (DTConOSA X) such that
A4: a = x and
( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o1 being OperSymbol of S st
( [o1,the carrier of S] = a . {} & the_result_sort_of o1 <= s ) ) by A2;
thus x in TS (DTConOSA X) by A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in TS (DTConOSA X) or x in union (rng (ParsedTerms X)) )
assume x in TS (DTConOSA X) ; :: thesis: x in union (rng (ParsedTerms X))
then reconsider t = x as Element of TS (DTConOSA X) ;
A5: rng t c= the carrier of (DTConOSA X) by RELAT_1:def 19;
{} in dom t by TREES_1:47;
then A6: t . {} in rng t by FUNCT_1:def 5;
A7: the carrier of (DTConOSA X) = (Terminals (DTConOSA X)) \/ (NonTerminals (DTConOSA X)) by LANG1:1;
A8: ( Terminals (DTConOSA X) = Union (coprod X) & NonTerminals (DTConOSA X) = [:the carrier' of S,{the carrier of S}:] ) by Th3;

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

suppose A9: t . {} in Terminals (DTConOSA X) ; :: thesis: x in union (rng (ParsedTerms X))

then reconsider a = t . {} as Terminal of (DTConOSA X) ;
A10: t = root-tree a by DTCONSTR:9;
a in union (rng (coprod X)) by A8, A9, CARD_3:def 4;
then consider A being set such that
A11: ( a in A & A in rng (coprod X) ) by TARSKI:def 4;
consider s being set such that
A12: ( s in dom (coprod X) & (coprod X) . s = A ) by A11, FUNCT_1:def 5;
reconsider s = s as Element of S by A12, PARTFUN1:def 4;
A = coprod s,X by A12, MSAFREE:def 3;
then consider b being set such that
A13: ( b in X . s & a = [b,s] ) by A11, MSAFREE:def 2;
t in ParsedTerms X,s by A10, A13;
then A14: t in (ParsedTerms X) . s by Def8;
(ParsedTerms X) . s in rng (ParsedTerms X) by A1, FUNCT_1:def 5;
hence x in union (rng (ParsedTerms X)) by A14, TARSKI:def 4; :: thesis: verum

end;

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

then reconsider a = t . {} as NonTerminal of (DTConOSA X) ;
consider o being Element of the carrier' of S, x2 being Element of {the carrier of S} such that
A15: a = [o,x2] by A8, DOMAIN_1:9;
A16: x2 = the carrier of S by TARSKI:def 1;
set rs = the_result_sort_of o;
t in ParsedTerms X,(the_result_sort_of o) by A15, A16;
then A17: t in (ParsedTerms X) . (the_result_sort_of o) by Def8;
(ParsedTerms X) . (the_result_sort_of o) in rng (ParsedTerms X) by A1, FUNCT_1:def 5;
hence x in union (rng (ParsedTerms X)) by A17, TARSKI:def 4; :: thesis: verum

end;

end;