let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for A being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
let X be non-empty ManySortedSet of S; :: thesis: for A being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
let A be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
set X0 = X;
let h be ManySortedFunction of (Free (S,X)),A; :: thesis: ( h is_homomorphism Free (S,X),A implies ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) ) )
assume A1: h is_homomorphism Free (S,X),A ; :: thesis: ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
set ww = canonical_homomorphism A;
reconsider H = FreeGen X as GeneratorSet of Free (S,X) by Th45;
reconsider G = FreeGen X as GeneratorSet of A by Th45;

A2: now :: thesis: for s being SortSymbol of S
for i being Element of X . s holds ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s]

let s be SortSymbol of S; :: thesis: for i being Element of X . s holds ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s]
let i be Element of X . s; :: thesis: ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s]
root-tree [i,s] in FreeGen (s,X) by MSAFREE:def 15;
then A3: root-tree [i,s] in H . s by MSAFREE:def 16;
G c= the Sorts of A by PBOOLE:def 18;
then H . s c= the Sorts of A . s ;
hence ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s] by A3, Th47; :: thesis: verum

end;

then A4: ( canonical_homomorphism A is_homomorphism Free (S,X),A & ( for s being SortSymbol of S
for i being Element of X . s holds ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s] ) ) by Def10;
reconsider hG = h || H as ManySortedFunction of G, the Sorts of A ;
consider g being ManySortedFunction of A,A such that
A5: ( g is_homomorphism A,A & g || G = hG ) by Def9;
take g ; :: thesis: ( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )
thus g is_homomorphism A,A by A5; :: thesis: h = g ** (canonical_homomorphism A)
A6: g ** (canonical_homomorphism A) is_homomorphism Free (S,X),A by A4, A5, MSUALG_3:10;

now :: thesis: for x being object st x in the carrier of S holds
(h || H) . x = ((g ** (canonical_homomorphism A)) || H) . x

let x be object ; :: thesis: ( x in the carrier of S implies (h || H) . x = ((g ** (canonical_homomorphism A)) || H) . x )
assume x in the carrier of S ; :: thesis: (h || H) . x = ((g ** (canonical_homomorphism A)) || H) . x
then reconsider s = x as SortSymbol of S ;
A7: ( dom ((h || H) . s) = H . s & dom (((g ** (canonical_homomorphism A)) || H) . s) = H . s ) by FUNCT_2:def 1;

now :: thesis: for y being object st y in H . s holds
((h || H) . x) . y = (((g ** (canonical_homomorphism A)) || H) . x) . y

let y be object ; :: thesis: ( y in H . s implies ((h || H) . x) . y = (((g ** (canonical_homomorphism A)) || H) . x) . y )
assume A8: y in H . s ; :: thesis: ((h || H) . x) . y = (((g ** (canonical_homomorphism A)) || H) . x) . y
then y in FreeGen (s,X) by MSAFREE:def 16;
then consider z being set such that
A9: ( z in X . s & y = root-tree [z,s] ) by MSAFREE:def 15;
A10: ((canonical_homomorphism A) . s) . y = root-tree [z,s] by A2, A9;
then ((canonical_homomorphism A) . s) . y in FreeGen (s,X) by A9, MSAFREE:def 15;
then A11: ((canonical_homomorphism A) . s) . y in G . s by MSAFREE:def 16;
A12: H . s c= the Sorts of (Free (S,X)) . s by PBOOLE:def 2, PBOOLE:def 18;
A13: dom (g ** (canonical_homomorphism A)) = the carrier of S /\ the carrier of S by PARTFUN1:def 2;
thus ((h || H) . x) . y = ((g . s) | (G . s)) . (((canonical_homomorphism A) . s) . y) by A9, A10, A5, MSAFREE:def 1
.= (g . s) . (((canonical_homomorphism A) . s) . y) by A11, FUNCT_1:49
.= ((g . s) * ((canonical_homomorphism A) . s)) . y by A8, A12, FUNCT_2:15
.= ((g ** (canonical_homomorphism A)) . s) . y by A13, PBOOLE:def 19
.= (((g ** (canonical_homomorphism A)) . s) | (H . s)) . y by A8, FUNCT_1:49
.= (((g ** (canonical_homomorphism A)) || H) . x) . y by MSAFREE:def 1 ; :: thesis: verum

end;

hence (h || H) . x = ((g ** (canonical_homomorphism A)) || H) . x by A7; :: thesis: verum

end;

hence h = g ** (canonical_homomorphism A) by A1, A6, EXTENS_1:19, PBOOLE:3; :: thesis: verum