let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S holds FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

let X be V5() ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S holds FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

let s be SortSymbol of S; :: thesis: FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

set D = DTConMSA X;

set A = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } ;

thus FreeGen (s,X) c= { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } :: according to XBOOLE_0:def 10 :: thesis: { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } c= FreeGen (s,X)

assume x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } ; :: thesis: x in FreeGen (s,X)

then consider t being Symbol of (DTConMSA X) such that

A4: x = root-tree t and

A5: t in Terminals (DTConMSA X) and

A6: t `2 = s ;

consider s1 being SortSymbol of S, a being set such that

A7: a in X . s1 and

A8: t = [a,s1] by A5, Th7;

s = s1 by A6, A8;

hence x in FreeGen (s,X) by A4, A7, A8, Def15; :: thesis: verum

for s being SortSymbol of S holds FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

let X be V5() ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S holds FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

let s be SortSymbol of S; :: thesis: FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

set D = DTConMSA X;

set A = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } ;

thus FreeGen (s,X) c= { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } :: according to XBOOLE_0:def 10 :: thesis: { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } c= FreeGen (s,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) & t `2 = s ) } or x in FreeGen (s,X) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in FreeGen (s,X) or x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } )

assume x in FreeGen (s,X) ; :: thesis: x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

then consider a being set such that

A1: a in X . s and

A2: x = root-tree [a,s] by Def15;

A3: [a,s] in Terminals (DTConMSA X) by A1, Th7;

then reconsider t = [a,s] as Symbol of (DTConMSA X) ;

t `2 = s ;

hence x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by A2, A3; :: thesis: verum

end;assume x in FreeGen (s,X) ; :: thesis: x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

then consider a being set such that

A1: a in X . s and

A2: x = root-tree [a,s] by Def15;

A3: [a,s] in Terminals (DTConMSA X) by A1, Th7;

then reconsider t = [a,s] as Symbol of (DTConMSA X) ;

t `2 = s ;

hence x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by A2, A3; :: thesis: verum

assume x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } ; :: thesis: x in FreeGen (s,X)

then consider t being Symbol of (DTConMSA X) such that

A4: x = root-tree t and

A5: t in Terminals (DTConMSA X) and

A6: t `2 = s ;

consider s1 being SortSymbol of S, a being set such that

A7: a in X . s1 and

A8: t = [a,s1] by A5, Th7;

s = s1 by A6, A8;

hence x in FreeGen (s,X) by A4, A7, A8, Def15; :: thesis: verum