set NH = OSNat_Hom (ParsedTermsOSA X),(LCongruence X);
let A, B be Function of (OSFreeGen s,X),(PTVars s,X); :: thesis: ( ( for t being Symbol of (DTConOSA X) st ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) in OSFreeGen s,X holds
A . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t ) & ( for t being Symbol of (DTConOSA X) st ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) in OSFreeGen s,X holds
B . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t ) implies A = B )
assume that
A15: for t being Symbol of (DTConOSA X) st ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) in OSFreeGen s,X holds
A . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t and
A16: for t being Symbol of (DTConOSA X) st ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) in OSFreeGen s,X holds
B . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t ; :: thesis: A = B
set D = DTConOSA X;
set C = { (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) } ;
A17: OSFreeGen s,X = { (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) } by Th31;
then A18: ( dom A = { (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) } & dom B = { (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) } ) by FUNCT_2:def 1;
for i being set st i in { (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) } holds
A . i = B . i

proof

let i be set ; :: thesis: ( i in { (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) } implies A . i = B . i )
assume A19: i in { (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) } ; :: thesis: A . i = B . i
then consider t being Symbol of (DTConOSA X) such that
A20: ( i = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) & t in Terminals (DTConOSA X) & t `2 = s ) ;
( A . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t & B . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t ) by A15, A16, A17, A19, A20;
hence A . i = B . i by A20; :: thesis: verum

end;

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