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

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

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

end;

then A4: ( canonical_homomorphism A0 is_homomorphism Free (S,X0),A0 & ( for s being SortSymbol of S
for i being Element of X0 . s holds ((canonical_homomorphism A0) . s) . (root-tree [i,s]) = root-tree [i,s] ) ) by Def7;
reconsider hG = h || H as ManySortedFunction of G, the Sorts of A0 ;
consider g being ManySortedFunction of A0,A0 such that
A5: ( g is_homomorphism A0,A0 & g || G = hG ) by Def6;
take g ; :: thesis: ( g is_homomorphism A0,A0 & h = g ** (canonical_homomorphism A0) )
thus g is_homomorphism A0,A0 by A5; :: thesis: h = g ** (canonical_homomorphism A0)
A6: g ** (canonical_homomorphism A0) is_homomorphism Free (S,X0),A0 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 A0)) || H) . x

let x be object ; :: thesis: ( x in the carrier of S implies (h || H) . x = ((g ** (canonical_homomorphism A0)) || H) . x )
assume x in the carrier of S ; :: thesis: (h || H) . x = ((g ** (canonical_homomorphism A0)) || H) . x
then reconsider s = x as SortSymbol of S ;
A7: ( dom ((h || H) . s) = H . s & dom (((g ** (canonical_homomorphism A0)) || 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 A0)) || H) . x) . y

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

end;

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

end;

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