let S be locally_directed OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
set FA = FreeOSA X;
set PTA = ParsedTermsOSA X;
set SPTA = the Sorts of (ParsedTermsOSA X);
set FG = OSFreeGen X;
let U1 be non-empty monotone OSAlgebra of S; :: according to OSAFREE:def 2 :: thesis:
let F be ManySortedFunction of OSFreeGen X, the Sorts of U1; :: thesis:
set SA = the Sorts of (FreeOSA X);
set S1 = the Sorts of U1;
set R = LCongruence X;
set NH = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X));
reconsider NH1 = OSNat_Hom ((ParsedTermsOSA X),(LCongruence X)) as ManySortedFunction of (ParsedTermsOSA X),(FreeOSA X) ;
set NHP = NH1 || (PTVars X);

A1: now :: thesis:

let s be Element of S; :: thesis:
A2: (NH1 || (PTVars X)) . s = (NH1 . s) | ((PTVars X) . s) by MSAFREE:def 1;
hence (NH1 || (PTVars X)) . s = (NH1 . s) | (PTVars (s,X)) by Def24; :: thesis:
thus PTVars (s,X) c= the Sorts of (ParsedTermsOSA X) . s ; :: thesis:
thus ( dom (NH1 . s) = the Sorts of (ParsedTermsOSA X) . s & rng (NH1 . s) c= the Sorts of (FreeOSA X) . s ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis:
A3: (PTVars X) . s = PTVars (s,X) by Def24;
hence A4: dom ((NH1 || (PTVars X)) . s) = PTVars (s,X) by FUNCT_2:def 1; :: thesis:
for y being object holds
( y in (OSFreeGen X) . s iff ex x being object st
( x in dom ((NH1 || (PTVars X)) . s) & y = ((NH1 || (PTVars X)) . s) . x ) )

proof

let y be object ; :: thesis:
thus ( y in (OSFreeGen X) . s implies ex x being object st
( x in dom ((NH1 || (PTVars X)) . s) & y = ((NH1 || (PTVars X)) . s) . x ) ) :: thesis:

proof

assume y in (OSFreeGen X) . s ; :: thesis:
then y in OSFreeGen (s,X) by Def26;
then consider a being object such that
A5: a in X . s and
A6: y = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) by Def25;
take x = root-tree [a,s]; :: thesis:
root-tree [a,s] in dom ((NH1 || (PTVars X)) . s) by A4, A5, Def23;
hence ( x in dom ((NH1 || (PTVars X)) . s) & y = ((NH1 || (PTVars X)) . s) . x ) by A2, A6, FUNCT_1:47; :: thesis:

end;

given x being object such that A7: x in dom ((NH1 || (PTVars X)) . s) and
A8: y = ((NH1 || (PTVars X)) . s) . x ; :: thesis:
consider a being object such that
A9: a in X . s and
A10: x = root-tree [a,s] by A3, A7, Def23;
y = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) by A2, A7, A8, A10, FUNCT_1:47;
then y in OSFreeGen (s,X) by A9, Def25;
hence y in (OSFreeGen X) . s by Def26; :: thesis:

end;

hence A11: rng ((NH1 || (PTVars X)) . s) = (OSFreeGen X) . s by FUNCT_1:def 3; :: thesis:
hence (NH1 || (PTVars X)) . s is Function of (PTVars (s,X)),((OSFreeGen X) . s) by A4, FUNCT_2:1; :: thesis:
thus (NH1 || (PTVars X)) . s is Function of ((PTVars X) . s),((OSFreeGen X) . s) by A3, A4, A11, FUNCT_2:1; :: thesis:

end;

then for i being object st i in the carrier of S holds
(NH1 || (PTVars X)) . i is Function of ((PTVars X) . i),((OSFreeGen X) . i) ;
then reconsider NHP = NH1 || (PTVars X) as ManySortedFunction of PTVars X, OSFreeGen X by PBOOLE:def 15;
consider h being ManySortedFunction of (ParsedTermsOSA X),U1 such that
A12: h is_homomorphism ParsedTermsOSA X,U1 and
A13: h is order-sorted and
A14: h || (PTVars X) = F ** NHP by Th37;
reconsider hCng = OSCng h as monotone OSCongruence of ParsedTermsOSA X by A12, A13, OSALG_4:24;
reconsider H = OSHomQuot (h,(LCongruence X)) as ManySortedFunction of (FreeOSA X),U1 ;
take H ; :: thesis:
A15: LCongruence X c= hCng by Def17;
hence ( H is_homomorphism FreeOSA X,U1 & H is order-sorted ) by A12, A13, OSALG_4:25; :: thesis:
for s being Element of S holds F . s = (H . s) | ((OSFreeGen X) . s)

proof

let s be Element of S; :: thesis:
A16: (OSFreeGen X) . s = OSFreeGen (s,X) by Def26;
then (OSFreeGen X) . s c= the Sorts of (FreeOSA X) . s ;
then (OSFreeGen X) . s c= dom (OSHomQuot (h,(LCongruence X),s)) by FUNCT_2:def 1;
then A17: dom ((OSHomQuot (h,(LCongruence X),s)) | ((OSFreeGen X) . s)) = (OSFreeGen X) . s by RELAT_1:62;
rng ((OSHomQuot (h,(LCongruence X),s)) | ((OSFreeGen X) . s)) c= the Sorts of U1 . s by RELAT_1:def 19;
then reconsider OSF = (OSHomQuot (h,(LCongruence X),s)) | ((OSFreeGen X) . s) as Function of ((OSFreeGen X) . s),( the Sorts of U1 . s) by A17, FUNCT_2:2;

now :: thesis:

A18: dom (NHP . s) = PTVars (s,X) by A1;
A19: (h . s) | ((PTVars X) . s) = (F ** NHP) . s by A14, MSAFREE:def 1
.= (F . s) * (NHP . s) by MSUALG_3:2 ;
let x be object ; :: thesis:
assume A20: x in (OSFreeGen X) . s ; :: thesis:
consider a being object such that
A21: a in X . s and
A22: x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) by A16, A20, Def25;
reconsider xa = root-tree [a,s] as Element of the Sorts of (ParsedTermsOSA X) . s by A21, Th10;
A23: OSClass ((LCongruence X),xa) = (OSNat_Hom ((ParsedTermsOSA X),(LCongruence X),s)) . xa by OSALG_4:def 21
.= x by A22, OSALG_4:def 22 ;
A24: root-tree [a,s] in PTVars (s,X) by A21, Def23;
then xa in (PTVars X) . s by Def24;
then A25: (h . s) . xa = ((h . s) | ((PTVars X) . s)) . xa by FUNCT_1:49;
A26: (OSHomQuot (h,(LCongruence X),s)) . (OSClass ((LCongruence X),xa)) = (h . s) . xa by A12, A13, A15, OSALG_4:def 27;
(NHP . s) . xa = (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) | (PTVars (s,X))) . xa by A1
.= ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . xa by A24, FUNCT_1:49 ;
then (h . s) . xa = (F . s) . x by A22, A24, A19, A25, A18, FUNCT_1:13;
hence (F . s) . x = ((OSHomQuot (h,(LCongruence X),s)) | ((OSFreeGen X) . s)) . x by A20, A23, A26, FUNCT_1:49; :: thesis:

end;

then F . s = OSF by FUNCT_2:12;
hence F . s = (H . s) | ((OSFreeGen X) . s) by OSALG_4:def 28; :: thesis:

end;

then for i being set st i in the carrier of S holds
F . i = (H . i) | ((OSFreeGen X) . i) ;
hence H || (OSFreeGen X) = F by MSAFREE:def 1; :: thesis: