let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S holds union (rng (FreeGen X)) = { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) }
let X be non-empty ManySortedSet of the carrier of S; :: thesis: union (rng (FreeGen X)) = { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) }
set D = DTConMSA X;
set A = union (rng (FreeGen X));
set B = { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) } ;
thus union (rng (FreeGen X)) c= { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) } :: according to XBOOLE_0:def 10 :: thesis: { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) } c= union (rng (FreeGen X))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng (FreeGen X)) or x in { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) } )
assume x in union (rng (FreeGen X)) ; :: thesis: x in { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) }
then consider C being set such that
A1: x in C and
A2: C in rng (FreeGen X) by TARSKI:def 4;
consider s being object such that
A3: s in dom (FreeGen X) and
A4: (FreeGen X) . s = C by A2, FUNCT_1:def 3;
reconsider s = s as SortSymbol of S by A3;
C = FreeGen (s,X) by A4, Def16
.= { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by Th13 ;
then ex t being Symbol of (DTConMSA X) st
( x = root-tree t & t in Terminals (DTConMSA X) & t `2 = s ) by A1;
hence x in { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) } or x in union (rng (FreeGen X)) )
assume x in { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) } ; :: thesis: x in union (rng (FreeGen X))
then consider t being Symbol of (DTConMSA X) such that
A5: x = root-tree t and
A6: t in Terminals (DTConMSA X) ;
consider s being SortSymbol of S, a being set such that
a in X . s and
A7: t = [a,s] by A6, Th7;
t `2 = s by A7;
then x in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by A5, A6;
then x in FreeGen (s,X) by Th13;
then A8: x in (FreeGen X) . s by Def16;
dom (FreeGen X) = the carrier of S by PARTFUN1:def 2;
then (FreeGen X) . s in rng (FreeGen X) by FUNCT_1:def 3;
hence x in union (rng (FreeGen X)) by A8, TARSKI:def 4; :: thesis: verum