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
A5: for t being Symbol of (DTConMSA X) st root-tree t in FreeGen s,X holds
A . (root-tree t) = t `1 and
A6: 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
set D = DTConMSA X;
set C = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } ;
A7: FreeGen s,X = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by Th14;
then A8: ( 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 FUNCT_2:def 1;
for i being set 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 set ; :: 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 A9: 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
A10: ( i = root-tree t & t in Terminals (DTConMSA X) & t `2 = s ) ;
( A . (root-tree t) = t `1 & B . (root-tree t) = t `1 ) by A5, A6, A7, A9, A10;
hence A . i = B . i by A10; :: thesis: verum

end;

hence A = B by A8, FUNCT_1:9; :: thesis: verum