set A = NFAlgebra R;
A1: the Sorts of (NFAlgebra R) = NForms R by Def20;
thus FreeGen X is ManySortedSubset of the Sorts of (NFAlgebra R) :: according to MSAFREE4:def 7 :: thesis:

proof

let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis:
assume i in the carrier of S ; :: thesis:
then reconsider s = i as SortSymbol of S ;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in (FreeGen X) . i ; :: thesis:
Free (S,X) = FreeMSA X by MSAFREE3:31;
then (FreeGen X) . s c= the Sorts of (Free (S,X)) . s by PBOOLE:def 2, PBOOLE:def 18;
then reconsider x = x as Element of (Free (S,X)),s by A2;
( x is_a_normal_form_wrt R . s & R . s reduces x,x ) by A2, Def18, REWRITE1:12;
then ( x is_a_normal_form_of x,R . s & nf (x,(R . s)) is_a_normal_form_of x,R . s ) by REWRITE1:54;
then ( x = nf (x,(R . s)) & (NForms R) . s = { (nf (y,(R . s))) where y is Element of (Free (S,X)),s : verum } ) by Def19, REWRITE1:53;
hence x in the Sorts of (NFAlgebra R) . i by A1; :: thesis:

end;

hereby :: according to MSAFREE4:def 8 :: thesis:

let o be OperSymbol of S; :: thesis:
let p be FinSequence; :: thesis:
assume A3: ( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of (NFAlgebra R) . (the_result_sort_of o) ) ; :: thesis:
then A4: ( dom p = dom (the_arity_of o) & dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom (the_arity_of o) ) by MSUALG_3:6, PRALG_2:3;
reconsider q = p as FinSequence ;
(Den (o,(Free (S,X)))) . p in { (nf (z,(R . (the_result_sort_of o)))) where z is Element of the Sorts of (Free (S,X)) . (the_result_sort_of o) : verum } by A1, A3, Def19;
then consider z being Element of the Sorts of (Free (S,X)) . (the_result_sort_of o) such that
A5: (Den (o,(Free (S,X)))) . p = nf (z,(R . (the_result_sort_of o))) ;
A6: (Den (o,(Free (S,X)))) . p is_a_normal_form_of z,R . (the_result_sort_of o) by A5, REWRITE1:54;

A7: now :: thesis:

let i be object ; :: thesis:
assume A8: i in dom p ; :: thesis:
then A9: the Sorts of (Free (S,X)) . ((the_arity_of o) . i) = ( the Sorts of (Free (S,X)) * (the_arity_of o)) . i by A4, FUNCT_1:13;
reconsider j = i as Element of NAT by A8;
reconsider ai = (the_arity_of o) . i as SortSymbol of S by A4, A8, FUNCT_1:102;
A10: ai = (the_arity_of o) /. j by A8, A4, PARTFUN1:def 6;
Args (o,(Free (S,X))) = product ( the Sorts of (Free (S,X)) * (the_arity_of o)) by PRALG_2:3;
then reconsider pj = p . i as Element of the Sorts of (Free (S,X)) . ((the_arity_of o) . i) by A3, A9, A8, A4, CARD_3:9;
assume p . i nin ((NForms R) * (the_arity_of o)) . i ; :: thesis:
then p . i nin (NForms R) . ((the_arity_of o) . i) by A4, A8, FUNCT_1:13;
then pj nin { (nf (b,(R . ((the_arity_of o) /. i)))) where b is Element of the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) : verum } by A10, Def19;
then ( nf (pj,(R . ((the_arity_of o) . i))) is_a_normal_form_of pj,R . ((the_arity_of o) . i) & ( for a being Element of the Sorts of (Free (S,X)) . ((the_arity_of o) . i) holds pj <> nf (a,(R . ((the_arity_of o) . i))) ) ) by A10, REWRITE1:54;
then ( R . ((the_arity_of o) . i) reduces pj, nf (pj,(R . ((the_arity_of o) . i))) & nf (pj,(R . ((the_arity_of o) . i))) <> pj ) ;
then consider x being object such that
A11: [pj,x] in R . ((the_arity_of o) . i) by REWRITE1:33, REWRITE1:def 5;
reconsider x = x as Element of the Sorts of (Free (S,X)) . ((the_arity_of o) . i) by A11, ZFMISC_1:87;
set f = transl (o,j,q,(Free (S,X)));
A12: (transl (o,j,q,(Free (S,X)))) . pj = (Den (o,(Free (S,X)))) . (q +* (j,pj)) by A10, MSUALG_6:def 4
.= (Den (o,(Free (S,X)))) . p by FUNCT_7:35 ;
[((transl (o,j,q,(Free (S,X)))) . pj),((transl (o,j,q,(Free (S,X)))) . x)] in R . (the_result_sort_of o) by A11, A3, A8, A4, A10, MSUALG_6:def 5, MSUALG_6:def 8;
hence contradiction by A6, A12, REWRITE1:def 5; :: thesis:

end;

dom ((NForms R) * (the_arity_of o)) = dom (the_arity_of o) by A1, PRALG_2:3;
then p in product ((NForms R) * (the_arity_of o)) by A4, A7, CARD_3:9;
hence p in Args (o,(NFAlgebra R)) by A1, PRALG_2:3; :: thesis:
hence (Den (o,(NFAlgebra R))) . p = nf (((Den (o,(Free (S,X)))) . p),(R . (the_result_sort_of o))) by Def20
.= (Den (o,(Free (S,X)))) . p by A6, Th17 ;
:: thesis:

end;

let f be ManySortedFunction of FreeGen X, the Sorts of (NFAlgebra R); :: according to MSAFREE4:def 9 :: thesis:
let G be ManySortedSubset of the Sorts of (NFAlgebra R); :: thesis:
assume A13: G = FreeGen X ; :: thesis:
reconsider H = FreeGen X as GeneratorSet of Free (S,X) by MSAFREE3:31;
( the Sorts of (NFAlgebra R) = NForms R & H is_transformable_to NForms R & H is_transformable_to the Sorts of (Free (S,X)) ) by Def20, Th21;
then A14: ( the Sorts of (NFAlgebra R) c= the Sorts of (Free (S,X)) & rngs f c= the Sorts of (NFAlgebra R) & doms f = H ) by MSSUBFAM:17, PBOOLE:def 18;
then ( rngs f c= the Sorts of (Free (S,X)) & FreeMSA X = Free (S,X) ) by PBOOLE:13, MSAFREE3:31;
then ( f is ManySortedFunction of H, the Sorts of (Free (S,X)) & H is free ) by A14, Th21, EQUATION:4;
then consider g being ManySortedFunction of (Free (S,X)),(Free (S,X)) such that
A15: ( g is_homomorphism Free (S,X), Free (S,X) & g || H = f ) ;
deffunc H₂( SortSymbol of S, Element of (NFAlgebra R),S) -> set = nf (((g . S) . X),(R . S));
defpred S₁[ object , object , object ] means R = nf (((g . S) . X),(R . S));
A16: for s, x being object st s in the carrier of S & x in the Sorts of (NFAlgebra R) . s holds
ex y being object st
( y in the Sorts of (NFAlgebra R) . s & S₁[s,x,y] )

proof

let s, x be object ; :: thesis:
assume A17: s in the carrier of S ; :: thesis:
assume A18: x in the Sorts of (NFAlgebra R) . s ; :: thesis:
reconsider t = s as SortSymbol of S by A17;
reconsider z = x as Element of (NFAlgebra R),t by A18;
take y = H₂(t,z); :: thesis:
(NForms R) . t c= the Sorts of (Free (S,X)) . t by PBOOLE:def 2, PBOOLE:def 18;
then reconsider a = (g . t) . z as Element of (Free (S,X)),t by A1, FUNCT_2:5;
y = nf (a,(R . t)) ;
then y in { (nf (u,(R . t))) where u is Element of (Free (S,X)),t : verum } ;
hence y in the Sorts of (NFAlgebra R) . s by A1, Def19; :: thesis:
thus S₁[s,x,y] ; :: thesis:

end;

consider h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) such that
A19: for s, x being object st s in the carrier of S & x in the Sorts of (NFAlgebra R) . s holds
( (h . s) . x in the Sorts of (NFAlgebra R) . s & S₁[s,x,(h . s) . x] ) from YELLOW18:sch 23(A16);
take h ; :: thesis:
thus h is_homomorphism NFAlgebra R, NFAlgebra R :: thesis:

proof

let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis:
assume Args (o,(NFAlgebra R)) <> {} ; :: thesis:
let x be Element of Args (o,(NFAlgebra R)); :: thesis:
(NForms R) * (the_arity_of o) c= the Sorts of (Free (S,X)) * (the_arity_of o) by Th15, PBOOLE:def 18;
then product ((NForms R) * (the_arity_of o)) c= product ( the Sorts of (Free (S,X)) * (the_arity_of o)) by Th16;
then product ((NForms R) * (the_arity_of o)) c= Args (o,(Free (S,X))) by PRALG_2:3;
then ( Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X))) & x in Args (o,(NFAlgebra R)) ) by A1, PRALG_2:3;
then reconsider y = x as Element of Args (o,(Free (S,X))) ;
A20: for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) by A19;
reconsider Dy = (Den (o,(Free (S,X)))) . y as Element of (Free (S,X)),(the_result_sort_of o) by FUNCT_2:15;
(Den (o,(NFAlgebra R))) . x in Result (o,(NFAlgebra R)) ;
then (Den (o,(NFAlgebra R))) . x in the Sorts of (NFAlgebra R) . (the_result_sort_of o) by FUNCT_2:15;
hence (h . (the_result_sort_of o)) . ((Den (o,(NFAlgebra R))) . x) = nf (((g . (the_result_sort_of o)) . ((Den (o,(NFAlgebra R))) . x)),(R . (the_result_sort_of o))) by A19
.= nf (((g . (the_result_sort_of o)) . (nf (((Den (o,(Free (S,X)))) . x),(R . (the_result_sort_of o))))),(R . (the_result_sort_of o))) by Def20
.= nf (((g . (the_result_sort_of o)) . Dy),(R . (the_result_sort_of o))) by A15, Th80
.= nf (((Den (o,(Free (S,X)))) . (g # y)),(R . (the_result_sort_of o))) by A15
.= nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . (the_result_sort_of o))) by A15, A20, Th85
.= nf ((nf (((Den (o,(Free (S,X)))) . (h # x)),(R . (the_result_sort_of o)))),(R . (the_result_sort_of o))) by Def20
.= nf (((Den (o,(Free (S,X)))) . (h # x)),(R . (the_result_sort_of o))) by Th18
.= (Den (o,(NFAlgebra R))) . (h # x) by Def20 ;
:: thesis:

end;

let a be Element of S; :: according to PBOOLE:def 21 :: thesis:
A21: ( dom (f . a) = H . a & dom ((h || G) . a) = G . a ) by FUNCT_2:def 1;
hence dom (f . a) = dom ((h || G) . a) by A13; :: according to FUNCT_1:def 11 :: thesis:
let x be object ; :: thesis:
assume A22: x in dom (f . a) ; :: thesis:
A23: G . a c= the Sorts of (NFAlgebra R) . a by PBOOLE:def 2, PBOOLE:def 18;
reconsider fax = (f . a) . x as Element of (NFAlgebra R),a by A22, FUNCT_2:5;
the Sorts of (NFAlgebra R) = NForms R by Def20;
hence (f . a) . x = nf (fax,(R . a)) by Th79
.= nf ((((g . a) | (H . a)) . x),(R . a)) by A15, MSAFREE:def 1
.= nf (((g . a) . x),(R . a)) by A22, FUNCT_1:49
.= (h . a) . x by A23, A13, A21, A22, A19
.= ((h . a) | (G . a)) . x by A13, A22, FUNCT_1:49
.= ((h || G) . a) . x by MSAFREE:def 1 ;
:: thesis: