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); :: thesis: ( ( 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 ; :: thesis: 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

proof

let i be object ; :: thesis: ( i in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } implies A . i = B . i )
assume A12: i in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } ; :: thesis: A . i = B . i
then consider t being Symbol of (DTConMSA X) such that
A13: i = root-tree t and
t in Terminals (DTConMSA X) and
t `2 = s ;
A . (root-tree t) = t `1 by A8, A10, A12, A13;
hence A . i = B . i by A9, A10, A12, A13; :: thesis: verum

end;

( 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; :: thesis: verum