let S be locally_directed OrderSortedSign; :: thesis:
let X be V5() ManySortedSet of ; :: 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: (PTVars X) . s = PTVars s,X by Def25;
A3: (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:
thus A4: dom ((NH1 || (PTVars X)) . s) = PTVars s,X by A2, 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 & 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 A3, A5, FUNCT_1:70; :: thesis:

end;

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

end;

hence A8: 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 A2, A4, A8, 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
A9: ( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = F ** NHP ) by Th38;
reconsider hCng = OSCng h as monotone OSCongruence of ParsedTermsOSA X by A9, OSALG_4:26;
A10: LCongruence X c= hCng by Def18;
reconsider H = OSHomQuot h,(LCongruence X) as ManySortedFunction of (FreeOSA X),U1 ;
take H ; :: thesis:
thus ( H is_homomorphism FreeOSA X,U1 & H is order-sorted ) by A9, A10, 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:
let f be Function of (the Sorts of (FreeOSA X) . s),(the Sorts of U1 . s); :: thesis:
assume A11: f = H . s ; :: thesis:
A12: (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 A13: ( dom ((OSHomQuot h,(LCongruence X),s) | ((OSFreeGen X) . s)) = (OSFreeGen X) . s & rng ((OSHomQuot h,(LCongruence X),s) | ((OSFreeGen X) . s)) c= rng (OSHomQuot h,(LCongruence X),s) ) by RELAT_1:91, RELAT_1:99;
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 A13, FUNCT_2:4;

let x be set ; :: thesis:
assume A14: x in (OSFreeGen X) . s ; :: thesis:
consider a being set such that
A15: ( a in X . s & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) by A12, A14, Def26;
A16: root-tree [a,s] in PTVars s,X by A15, Def24;
reconsider xa = root-tree [a,s] as Element of the Sorts of (ParsedTermsOSA X) . s by A15, Th10;
A17: xa in (PTVars X) . s by A16, Def25;
A18: OSClass (LCongruence X),xa = (OSNat_Hom (ParsedTermsOSA X),(LCongruence X),s) . xa by OSALG_4:def 23
.= x by A15, OSALG_4:def 24 ;
A19: (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 A16, FUNCT_1:72 ;
A20: (OSHomQuot h,(LCongruence X),s) . (OSClass (LCongruence X),xa) = (h . s) . xa by A9, A10, OSALG_4:def 29;
A21: (h . s) | ((PTVars X) . s) = (F ** NHP) . s by A9, MSAFREE:def 1
.= (F . s) * (NHP . s) by MSUALG_3:2 ;
A22: (h . s) . xa = ((h . s) | ((PTVars X) . s)) . xa by A17, FUNCT_1:72;
dom (NHP . s) = PTVars s,X by A1;
then (h . s) . xa = (F . s) . x by A15, A16, A19, A21, A22, FUNCT_1:23;
hence (F . s) . x = ((OSHomQuot h,(LCongruence X),s) | ((OSFreeGen X) . s)) . x by A14, A18, A20, FUNCT_1:72; :: thesis:

end;

then F . s = OSF by FUNCT_2:18;
hence F . s = f | ((OSFreeGen X) . s) by A11, 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: