let S be locally_directed OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for s being Element of S holds 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 ) }
let X be non-empty ManySortedSet of S; :: thesis: for s being Element of S holds 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 ) }
let s be Element of S; :: thesis: 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 ) }
set D = DTConOSA X;
set NH = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X));
set 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 ) } ;
thus OSFreeGen (s,X) 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 ) } :: according to XBOOLE_0:def 10 :: thesis: { (((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 ) } c= OSFreeGen (s,X)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OSFreeGen (s,X) or x 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 ) } )
assume x in OSFreeGen (s,X) ; :: thesis: x 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 ) }
then consider a being object such that
A1: a in X . s and
A2: x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) by Def25;
A3: [a,s] in Terminals (DTConOSA X) by A1, Th4;
then reconsider t = [a,s] as Symbol of (DTConOSA X) ;
t `2 = s ;
hence x 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 ) } by A2, A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x 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 ) } or x in OSFreeGen (s,X) )
assume x 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: x in OSFreeGen (s,X)
then consider t being Symbol of (DTConOSA X) such that
A4: x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) and
A5: t in Terminals (DTConOSA X) and
A6: t `2 = s ;
consider s1 being Element of S, a being set such that
A7: a in X . s1 and
A8: t = [a,s1] by A5, Th4;
s = s1 by A6, A8;
hence x in OSFreeGen (s,X) by A4, A7, A8, Def25; :: thesis: verum