let S be locally_directed OrderSortedSign; :: thesis:
let X be V16() 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

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 Def25; :: 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 Def25;
hence A4: dom ((NH1 || (PTVars X)) . s) = PTVars s,X by FUNCT_2:def 1; :: thesis:
for y being set holds
( y in (OSFreeGen X) . s iff ex x being set st
( x in dom ((NH1 || (PTVars X)) . s) & y = ((NH1 || (PTVars X)) . s) . x ) )

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

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

end;

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

end;

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

end;

then for i being set 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 18;
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 Th38;
reconsider hCng = OSCng h as monotone OSCongruence of ParsedTermsOSA X by A12, A13, OSALG_4:26;
reconsider H = OSHomQuot h,(LCongruence X) as ManySortedFunction of (FreeOSA X),U1 ;
take H ; :: thesis:
A15: LCongruence X c= hCng by Def18;
hence ( H is_homomorphism FreeOSA X,U1 & H is order-sorted ) by A12, A13, OSALG_4:27; :: thesis:
for s being Element of S
for f being Function of (the Sorts of (FreeOSA X) . s),(the Sorts of U1 . s) st f = H . s holds
F . s = f | ((OSFreeGen X) . s)

let s be Element of S; :: thesis:
A16: (OSFreeGen X) . s = OSFreeGen s,X by Def27;
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:91;
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:4;

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 set ; :: thesis:
assume A20: x in (OSFreeGen X) . s ; :: thesis:
consider a being set such that
A21: a in X . s and
A22: x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) by A16, A20, Def26;
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 23
.= x by A22, OSALG_4:def 24 ;
A24: root-tree [a,s] in PTVars s,X by A21, Def24;
then xa in (PTVars X) . s by Def25;
then A25: (h . s) . xa = ((h . s) | ((PTVars X) . s)) . xa by FUNCT_1:72;
A26: (OSHomQuot h,(LCongruence X),s) . (OSClass (LCongruence X),xa) = (h . s) . xa by A12, A13, A15, OSALG_4:def 29;
(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:72 ;
then (h . s) . xa = (F . s) . x by A22, A24, A19, A25, A18, FUNCT_1:23;
hence (F . s) . x = ((OSHomQuot h,(LCongruence X),s) | ((OSFreeGen X) . s)) . x by A20, A23, A26, FUNCT_1:72; :: thesis:

end;

then A27: F . s = OSF by FUNCT_2:18;
let f be Function of (the Sorts of (FreeOSA X) . s),(the Sorts of U1 . s); :: thesis:
assume f = H . s ; :: thesis:
hence F . s = f | ((OSFreeGen X) . s) by A27, OSALG_4:def 30; :: thesis:

end;

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