let S be locally_directed OrderSortedSign; :: thesis: for X being V2() ManySortedSet of S holds OSFreeGen X is osfree
let X be V2() ManySortedSet of S; :: thesis: OSFreeGen X is osfree
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: for f being ManySortedFunction of OSFreeGen X, the Sorts of U1 ex h being ManySortedFunction of (FreeOSA X),U1 st
( h is_homomorphism FreeOSA X,U1 & h is order-sorted & h || (OSFreeGen X) = f )
let F be ManySortedFunction of OSFreeGen X, the Sorts of U1; :: thesis: ex h being ManySortedFunction of (FreeOSA X),U1 st
( h is_homomorphism FreeOSA X,U1 & h is order-sorted & h || (OSFreeGen X) = F )
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);
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: ( H is_homomorphism FreeOSA X,U1 & H is order-sorted & H || (OSFreeGen X) = F )
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: H || (OSFreeGen X) = F
for s being Element of S holds F . s = (H . s) | ((OSFreeGen X) . s) 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: verum