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 Th30;
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 object 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 object ; :: 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:2; :: thesis: verum