let S be non empty non void ManySortedSign ; 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; 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; 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 ) }
XBOOLE_0:def 10 { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } c= FreeGen (s,X)
let x be object ; TARSKI:def 3 ( 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) )
assume
x in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }
; 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; verum