let S be OrderSortedSign; for X being V2() ManySortedSet of S holds union (rng (ParsedTerms X)) = TS (DTConOSA X)
let X be V2() ManySortedSet of S; union (rng (ParsedTerms X)) = TS (DTConOSA X)
set D = DTConOSA X;
A1:
dom (ParsedTerms X) = the carrier of S
by PARTFUN1:def 2;
thus
union (rng (ParsedTerms X)) c= TS (DTConOSA X)
XBOOLE_0:def 10 TS (DTConOSA X) c= union (rng (ParsedTerms X))
let x be object ; TARSKI:def 3 ( not x in TS (DTConOSA X) or x in union (rng (ParsedTerms X)) )
A6:
the carrier of (DTConOSA X) = (Terminals (DTConOSA X)) \/ (NonTerminals (DTConOSA X))
by LANG1:1;
assume
x in TS (DTConOSA X)
; x in union (rng (ParsedTerms X))
then reconsider t = x as Element of TS (DTConOSA X) ;
A7:
rng t c= the carrier of (DTConOSA X)
by RELAT_1:def 19;
A8:
NonTerminals (DTConOSA X) = [: the carrier' of S,{ the carrier of S}:]
by Th3;
A9:
Terminals (DTConOSA X) = Union (coprod X)
by Th3;
{} in dom t
by TREES_1:22;
then A10:
t . {} in rng t
by FUNCT_1:def 3;
per cases
( t . {} in Terminals (DTConOSA X) or t . {} in NonTerminals (DTConOSA X) )
by A7, A10, A6, XBOOLE_0:def 3;
suppose A11:
t . {} in Terminals (DTConOSA X)
;
x in union (rng (ParsedTerms X))then reconsider a =
t . {} as
Terminal of
(DTConOSA X) ;
a in union (rng (coprod X))
by A9, A11, CARD_3:def 4;
then consider A being
set such that A12:
a in A
and A13:
A in rng (coprod X)
by TARSKI:def 4;
consider s being
object such that A14:
s in dom (coprod X)
and A15:
(coprod X) . s = A
by A13, FUNCT_1:def 3;
reconsider s =
s as
Element of
S by A14;
A = coprod (
s,
X)
by A15, MSAFREE:def 3;
then A16:
ex
b being
set st
(
b in X . s &
a = [b,s] )
by A12, MSAFREE:def 2;
t = root-tree a
by DTCONSTR:9;
then
t in ParsedTerms (
X,
s)
by A16;
then A17:
t in (ParsedTerms X) . s
by Def8;
(ParsedTerms X) . s in rng (ParsedTerms X)
by A1, FUNCT_1:def 3;
hence
x in union (rng (ParsedTerms X))
by A17, TARSKI:def 4;
verum end; end;