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 )
set NH = OSNat_Hom (ParsedTermsOSA X),(LCongruence X);
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 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;
A19: 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 A20: 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
A21: i = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t) and
t in Terminals (DTConOSA X) and
t `2 = s ;
A . (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) = root-tree t by A15, A17, A20, A21;
hence A . i = B . i by A16, A17, A20, A21; :: thesis: verum

end;

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 ) } by A17, FUNCT_2:def 1;
hence A = B by A18, A19, FUNCT_1:9; :: thesis: verum