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

hence A = B by A11, FUNCT_1:2; :: thesis: verum

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

( 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;
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;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

hence A = B by A11, FUNCT_1:2; :: thesis: verum