let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S holds union (rng ()) = { () where t is Symbol of () : t in Terminals () }
let X be V5() ManySortedSet of the carrier of S; :: thesis: union (rng ()) = { () where t is Symbol of () : t in Terminals () }
set D = DTConMSA X;
set A = union (rng ());
set B = { () where t is Symbol of () : t in Terminals () } ;
thus union (rng ()) c= { () where t is Symbol of () : t in Terminals () } :: according to XBOOLE_0:def 10 :: thesis: { () where t is Symbol of () : t in Terminals () } c= union (rng ())
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng ()) or x in { () where t is Symbol of () : t in Terminals () } )
assume x in union (rng ()) ; :: thesis: x in { () where t is Symbol of () : t in Terminals () }
then consider C being set such that
A1: x in C and
A2: C in rng () by TARSKI:def 4;
consider s being object such that
A3: s in dom () and
A4: (FreeGen X) . s = C by ;
reconsider s = s as SortSymbol of S by A3;
C = FreeGen (s,X) by
.= { () where t is Symbol of () : ( t in Terminals () & t `2 = s ) } by Th13 ;
then ex t being Symbol of () st
( x = root-tree t & t in Terminals () & t `2 = s ) by A1;
hence x in { () where t is Symbol of () : t in Terminals () } ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { () where t is Symbol of () : t in Terminals () } or x in union (rng ()) )
assume x in { () where t is Symbol of () : t in Terminals () } ; :: thesis: x in union (rng ())
then consider t being Symbol of () such that
A5: x = root-tree t and
A6: t in Terminals () ;
consider s being SortSymbol of S, a being set such that
a in X . s and
A7: t = [a,s] by ;
t `2 = s by A7;
then x in { () where tt is Symbol of () : ( tt in Terminals () & tt `2 = s ) } by A5, A6;
then x in FreeGen (s,X) by Th13;
then A8: x in () . s by Def16;
dom () = the carrier of S by PARTFUN1:def 2;
then (FreeGen X) . s in rng () by FUNCT_1:def 3;
hence x in union (rng ()) by ; :: thesis: verum