let S be non empty non void ManySortedSign ; :: thesis: for X0 being non-empty countable ManySortedSet of S
for A0 being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for G being GeneratorSet of A0 st G = FreeGen X0 holds
G is Equations (S,A0) -free
let X0 be non-empty countable ManySortedSet of S; :: thesis: for A0 being X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for G being GeneratorSet of A0 st G = FreeGen X0 holds
G is Equations (S,A0) -free
let A0 be X0,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for G being GeneratorSet of A0 st G = FreeGen X0 holds
G is Equations (S,A0) -free
set A = A0;
A1: FreeMSA X0 = Free (S,X0) by MSAFREE3:31;
let G be GeneratorSet of A0; :: thesis: ( G = FreeGen X0 implies G is Equations (S,A0) -free )
assume A2: G = FreeGen X0 ; :: thesis: G is Equations (S,A0) -free
set T = Equations (S,A0);
let B be non-empty Equations (S,A0) -satisfying MSAlgebra over S; :: according to MSAFREE4:def 12 :: thesis: for f being ManySortedFunction of G, the Sorts of B ex h being ManySortedFunction of A0,B st
( h is_homomorphism A0,B & h || G = f )
let f be ManySortedFunction of G, the Sorts of B; :: thesis: ex h being ManySortedFunction of A0,B st
( h is_homomorphism A0,B & h || G = f )
reconsider f0 = f as ManySortedFunction of FreeGen X0, the Sorts of B by A2;
reconsider H = FreeGen X0 as free GeneratorSet of Free (S,X0) by A1;
consider g being ManySortedFunction of (Free (S,X0)),B such that
A3: ( g is_homomorphism Free (S,X0),B & g || H = f0 ) by MSAFREE:def 5;
the Sorts of A0 is MSSubset of (Free (S,X0)) by Def6;
then reconsider i = id the Sorts of A0 as ManySortedFunction of A0,(Free (S,X0)) by Th22;
take h = g ** i; :: thesis: ( h is_homomorphism A0,B & h || G = f )
thus h is_homomorphism A0,B :: thesis: h || G = f

proof

let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,A0) = {} or for b₁ being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . b₁) = (Den (o,B)) . (h # b₁) )
assume Args (o,A0) <> {} ; :: thesis: for b₁ being Element of Args (o,A0) holds (h . (the_result_sort_of o)) . ((Den (o,A0)) . b₁) = (Den (o,B)) . (h # b₁)
let x be Element of Args (o,A0); :: thesis: (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = (Den (o,B)) . (h # x)
set s = the_result_sort_of o;
(Den (o,A0)) . x in Result (o,A0) ;
then A4: (Den (o,A0)) . x in the Sorts of A0 . (the_result_sort_of o) by FUNCT_2:15;
A5: i . (the_result_sort_of o) = id ( the Sorts of A0 . (the_result_sort_of o)) by MSUALG_3:def 1;
( x in Args (o,A0) & Args (o,A0) c= Args (o,(Free (S,X0))) ) by Th41;
then reconsider x0 = x as Element of Args (o,(Free (S,X0))) ;
set w = the "1-1" ManySortedFunction of X0, the carrier of S --> NAT;
( (Den (o,A0)) . x is Element of Result (o,A0) & (Den (o,(Free (S,X0)))) . x0 is Element of Result (o,(Free (S,X0))) ) ;
then reconsider f1 = (Den (o,A0)) . x, f2 = (Den (o,(Free (S,X0)))) . x0 as Term of S,X0 by Th42;
reconsider f = (Den (o,(Free (S,X0)))) . x0 as Element of (Free (S,X0)),(the_result_sort_of o) by MSUALG_9:18;
reconsider fa = ((canonical_homomorphism A0) . (the_result_sort_of o)) . f as Element of (Free (S,X0)),(the_result_sort_of o) by Th39;
f1 in the Sorts of A0 . (the_result_sort_of o) by MSUALG_9:18;
then f1 is Element of (Free (S,X0)),(the_result_sort_of o) by Th39;
then ( f1 in the Sorts of (Free (S,X0)) . (the_result_sort_of o) & f2 in the Sorts of (Free (S,X0)) . (the_result_sort_of o) ) by MSUALG_9:18;
then ( f1 in FreeSort (X0,(the_result_sort_of o)) & f2 in FreeSort (X0,(the_result_sort_of o)) ) by A1, MSAFREE:def 11;
then ( the_sort_of f1 = the_result_sort_of o & the_sort_of f2 = the_result_sort_of o ) by MSATERM:def 5;
then reconsider t2 = # (f1, the "1-1" ManySortedFunction of X0, the carrier of S --> NAT), t1 = # (f2, the "1-1" ManySortedFunction of X0, the carrier of S --> NAT) as Element of (TermAlg S),(the_result_sort_of o) by Th60;
A6: f1 = ((canonical_homomorphism A0) . (the_result_sort_of o)) . f by Th67;
A0 |= t1 '=' t2 by A6, Th71;
then t1 '=' t2 in { e where e is Element of (Equations S) . (the_result_sort_of o) : A0 |= e } ;
then ( t1 '=' t2 in (Equations (S,A0)) . (the_result_sort_of o) & B |= Equations (S,A0) ) by Def14, Def11;
then A7: (g . (the_result_sort_of o)) . f = (g . (the_result_sort_of o)) . fa by A6, A3, Th74;

A8: now :: thesis: for n being Nat st n in dom x holds
(h # x) . n = (g . ((the_arity_of o) /. n)) . (x . n)

let n be Nat; :: thesis: ( n in dom x implies (h # x) . n = (g . ((the_arity_of o) /. n)) . (x . n) )
set an = (the_arity_of o) /. n;
assume A9: n in dom x ; :: thesis: (h # x) . n = (g . ((the_arity_of o) /. n)) . (x . n)
A10: ( dom ( the Sorts of A0 * (the_arity_of o)) = dom (the_arity_of o) & dom x = dom (the_arity_of o) ) by MSUALG_3:6, PRALG_2:3;
then x . n in ( the Sorts of A0 * (the_arity_of o)) . n by A9, MSUALG_3:6;
then x . n in the Sorts of A0 . ((the_arity_of o) . n) by A9, A10, FUNCT_1:13;
then A11: x . n in the Sorts of A0 . ((the_arity_of o) /. n) by A9, A10, PARTFUN1:def 6;
thus (h # x) . n = (h . ((the_arity_of o) /. n)) . (x . n) by A9, MSUALG_3:def 6
.= ((g . ((the_arity_of o) /. n)) * (i . ((the_arity_of o) /. n))) . (x . n) by MSUALG_3:2
.= (g . ((the_arity_of o) /. n)) . ((i . ((the_arity_of o) /. n)) . (x . n)) by A11, FUNCT_2:15
.= (g . ((the_arity_of o) /. n)) . ((id ( the Sorts of A0 . ((the_arity_of o) /. n))) . (x . n)) by MSUALG_3:def 1
.= (g . ((the_arity_of o) /. n)) . (x . n) by A11, FUNCT_1:17 ; :: thesis: verum

end;

thus (h . (the_result_sort_of o)) . ((Den (o,A0)) . x) = ((g . (the_result_sort_of o)) * (i . (the_result_sort_of o))) . ((Den (o,A0)) . x) by MSUALG_3:2
.= (g . (the_result_sort_of o)) . ((i . (the_result_sort_of o)) . ((Den (o,A0)) . x)) by A4, FUNCT_2:15
.= (g . (the_result_sort_of o)) . ((Den (o,A0)) . x) by A5, A4, FUNCT_1:18
.= (g . (the_result_sort_of o)) . ((Den (o,(Free (S,X0)))) . x0) by A7, Th67
.= (Den (o,B)) . (g # x0) by A3
.= (Den (o,B)) . (h # x) by A8, MSUALG_3:def 6 ; :: thesis: verum

end;

now :: thesis: for x being object st x in the carrier of S holds
(h || G) . x = f . x

let x be object ; :: thesis: ( x in the carrier of S implies (h || G) . x = f . x )
assume x in the carrier of S ; :: thesis: (h || G) . x = f . x
then reconsider s = x as SortSymbol of S ;
A12: G . s c= the Sorts of A0 . s by PBOOLE:def 2, PBOOLE:def 18;
( dom (g . s) = the Sorts of (Free (S,X0)) . s & rng (i . s) c= the Sorts of (Free (S,X0)) . s ) by FUNCT_2:def 1;
then dom ((g . s) * (i . s)) = dom (i . s) by RELAT_1:27
.= the Sorts of A0 . s by FUNCT_2:def 1 ;
then A13: dom (((g . s) * (i . s)) | (G . s)) = G . s by A12, RELAT_1:62;
the Sorts of A0 is MSSubset of (Free (S,X0)) by Def6;
then the Sorts of A0 . s c= the Sorts of (Free (S,X0)) . s by PBOOLE:def 2, PBOOLE:def 18;
then ( G . s c= the Sorts of (Free (S,X0)) . s & dom (g . s) = the Sorts of (Free (S,X0)) . s ) by A12, FUNCT_2:def 1;
then A14: dom ((g . s) | (H . s)) = G . s by A2, RELAT_1:62;

A15: now :: thesis: for x being object st x in G . s holds
(((g . s) * (i . s)) | (G . s)) . x = ((g . s) | (H . s)) . x

let x be object ; :: thesis: ( x in G . s implies (((g . s) * (i . s)) | (G . s)) . x = ((g . s) | (H . s)) . x )
assume A16: x in G . s ; :: thesis: (((g . s) * (i . s)) | (G . s)) . x = ((g . s) | (H . s)) . x
hence (((g . s) * (i . s)) | (G . s)) . x = ((g . s) * (i . s)) . x by FUNCT_1:49
.= (g . s) . ((i . s) . x) by A12, A16, FUNCT_2:15
.= (g . s) . ((id ( the Sorts of A0 . s)) . x) by MSUALG_3:def 1
.= (g . s) . x by A12, A16, FUNCT_1:17
.= ((g . s) | (H . s)) . x by A2, A16, FUNCT_1:49 ;
:: thesis: verum

end;

thus (h || G) . x = (h . s) | (G . s) by MSAFREE:def 1
.= ((g . s) * (i . s)) | (G . s) by MSUALG_3:2
.= (g . s) | (H . s) by A13, A14, A15
.= f . x by A3, MSAFREE:def 1 ; :: thesis: verum

end;

hence h || G = f ; :: thesis: verum