let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S holds union (rng ()) = TS ()
let X be V5() ManySortedSet of the carrier of S; :: thesis: union (rng ()) = TS ()
set D = DTConMSA X;
A1: dom () = the carrier of S by PARTFUN1:def 2;
thus union (rng ()) c= TS () :: according to XBOOLE_0:def 10 :: thesis: TS () c= union (rng ())
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng ()) or x in TS () )
assume x in union (rng ()) ; :: thesis: x in TS ()
then consider A being set such that
A2: x in A and
A3: A in rng () by TARSKI:def 4;
consider s being object such that
A4: s in dom () and
A5: (FreeSort X) . s = A by ;
reconsider s = s as SortSymbol of S by A4;
A = FreeSort (X,s) by
.= { a where a is Element of TS () : ( 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 () 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 () ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TS () or x in union (rng ()) )
assume x in TS () ; :: thesis: x in union (rng ())
then reconsider t = x as Element of TS () ;
A6: ( rng t c= the carrier of () & the carrier of () = () \/ () ) by ;
{} in dom t by TREES_1:22;
then A7: t . {} in rng t by FUNCT_1:def 3;
A8: NonTerminals () = [: the carrier' of S,{ the carrier of S}:] by Th6;
A9: Terminals () = Union () by Th6;
per cases by ;
suppose A10: t . {} in Terminals () ; :: thesis: x in union (rng ())
then reconsider a = t . {} as Terminal of () ;
a in union (rng ()) by ;
then consider A being set such that
A11: a in A and
A12: A in rng () by TARSKI:def 4;
consider s being object such that
A13: s in dom () and
A14: (coprod X) . s = A by ;
reconsider s = s as SortSymbol of S by A13;
A = coprod (s,X) by ;
then ( t = root-tree a & ex b being set st
( b in X . s & a = [b,s] ) ) by ;
then t in FreeSort (X,s) ;
then A15: t in () . s by Def11;
(FreeSort X) . s in rng () by ;
hence x in union (rng ()) by ; :: thesis: verum
end;
suppose t . {} in NonTerminals () ; :: thesis: x in union (rng ())
then reconsider a = t . {} as NonTerminal of () ;
consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that
A16: a = [o,x2] by ;
set rs = the_result_sort_of o;
x2 = the carrier of S by TARSKI:def 1;
then t in FreeSort (X,) by A16;
then A17: t in () . by Def11;
(FreeSort X) . in rng () by ;
hence x in union (rng ()) by ; :: thesis: verum
end;
end;