let A, B be Function of (OSFreeGen (s,X)),(PTVars (s,X)); ( ( 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
; 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 ;
( 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 ) }
;
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;
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; verum