set A = OSFreeGen (s,X);
set R = LCongruence X;
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set NHs = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X),s);
set D = DTConOSA X;
set NH = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X));
defpred S1[ object , object ] means for t being Symbol of (DTConOSA X) st $1 = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) holds
$2 = root-tree t;
A1: (OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X),s) by OSALG_4:def 22;
A2: for x being object st x in OSFreeGen (s,X) holds
ex a being object st
( a in PTVars (s,X) & S1[x,a] )
proof
let x be object ; :: thesis: ( x in OSFreeGen (s,X) implies ex a being object st
( a in PTVars (s,X) & S1[x,a] ) )
assume x in OSFreeGen (s,X) ; :: thesis: ex a being object st
( a in PTVars (s,X) & S1[x,a] )
then 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 Th30;
then consider t being Symbol of (DTConOSA X) such that
A3: x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) and
A4: t in Terminals (DTConOSA X) and
A5: t `2 = s ;
A6: x = (OSNat_Hom ((ParsedTermsOSA X),(LCongruence X),s)) . (root-tree t) by A3, OSALG_4:def 22;
take root-tree t ; :: thesis: ( root-tree t in PTVars (s,X) & S1[x, root-tree t] )
consider s1 being Element of S, a being set such that
A7: a in X . s1 and
A8: t = [a,s1] by A4, Th4;
A9: s = s1 by A5, A8;
hence root-tree t in PTVars (s,X) by A7, A8, Def23; :: thesis: S1[x, root-tree t]
reconsider rt = root-tree t as Element of the Sorts of (ParsedTermsOSA X) . s by A7, A8, A9, Th10;
A10: (OSNat_Hom ((ParsedTermsOSA X),(LCongruence X),s)) . rt = OSClass ((LCongruence X),rt) by OSALG_4:def 21;
reconsider tt = root-tree t as Element of TS (DTConOSA X) by A7, A8, Th10;
let t1 be Symbol of (DTConOSA X); :: thesis: ( x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t1) implies root-tree t = root-tree t1 )
assume A11: x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t1) ; :: thesis: root-tree t = root-tree t1
A12: OSClass ((LCongruence X),tt) = OSClass ((LCongruence X),rt) by Def27;
OSClass ((LCongruence X),tt) <> {} by Th32;
then x <> {} by A12, A6, OSALG_4:def 21;
then root-tree t1 in dom (OSNat_Hom ((ParsedTermsOSA X),(LCongruence X),s)) by A1, A11, FUNCT_1:def 2;
then reconsider rt1 = root-tree t1 as Element of the Sorts of (ParsedTermsOSA X) . s ;
reconsider tt2 = rt1 as Element of TS (DTConOSA X) by Th15;
A13: OSClass ((LCongruence X),tt2) = OSClass ((LCongruence X),rt1) by Def27;
x = (OSNat_Hom ((ParsedTermsOSA X),(LCongruence X),s)) . (root-tree t1) by A11, OSALG_4:def 22;
then OSClass ((LCongruence X),rt1) = OSClass ((LCongruence X),rt) by A6, A10, OSALG_4:def 21;
then tt2 in OSClass ((LCongruence X),tt) by A12, A13, Th34;
hence root-tree t = root-tree t1 by A7, A8, Th36; :: thesis: verum
end;
consider f being Function such that
A14: ( dom f = OSFreeGen (s,X) & rng f c= PTVars (s,X) & ( for x being object st x in OSFreeGen (s,X) holds
S1[x,f . x] ) ) from FUNCT_1:sch 6(A2);
 reconsider f = f as Function of (OSFreeGen (s,X)),(PTVars (s,X)) by A14, FUNCT_2:2;
take f ; :: thesis: for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds
f . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t
let t be Symbol of (DTConOSA X); :: thesis: ( ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) implies f . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t )
assume ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) ; :: thesis: f . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t
hence f . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t by A14; :: thesis: verum