set D = DTConMSA X;
set C = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } ;
let A, B be Function of (FreeGen (s,X)),(X . s); ( ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
A . (root-tree t) = t `1 ) & ( for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
B . (root-tree t) = t `1 ) implies A = B )
assume that
A8:
for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
A . (root-tree t) = t `1
and
A9:
for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
B . (root-tree t) = t `1
; A = B
A10:
FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }
by Th13;
A11:
for i being object st i in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } holds
A . i = B . i
( dom A = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } & dom B = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } )
by A10, FUNCT_2:def 1;
hence
A = B
by A11, FUNCT_1:2; verum