let S be non empty non void ManySortedSign ; :: thesis: for X being V5() 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 V5() 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))

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

let X be V5() 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 { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) } or x in union (rng (FreeGen X)) )
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;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

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