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

now :: thesis: for s being SortSymbol of S
for i being Element of X0 . 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 X0 . s holds ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s]
let i be Element of X0 . s; :: thesis: ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s]
root-tree [i,s] in FreeGen (s,X0) by MSAFREE:def 15;
then A2: 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 A2, Th47; :: thesis: verum

end;

then A3: ( canonical_homomorphism A is_homomorphism Free (S,X0),A & ( for s being SortSymbol of S
for i being Element of X0 . s holds ((canonical_homomorphism A) . s) . (root-tree [i,s]) = root-tree [i,s] ) ) by Def10;
the Sorts of A is MSSubset of (Free (S,X0)) by Def6;
then reconsider hG = h || F as ManySortedFunction of F, the Sorts of (Free (S,X0)) by Th22;
( FreeGen Y is free & FreeMSA Y = Free (S,Y) ) by MSAFREE3:31;
then consider g being ManySortedFunction of (Free (S,Y)),(Free (S,X0)) such that
A4: ( g is_homomorphism Free (S,Y), Free (S,X0) & g || F = hG ) ;
take g ; :: thesis: ( g is_homomorphism Free (S,Y), Free (S,X0) & h = (canonical_homomorphism A) ** g & ( for G being GeneratorSet of Free (S,Y) st G = FreeGen Y holds
g || G = h || G ) )
thus g is_homomorphism Free (S,Y), Free (S,X0) by A4; :: thesis: ( h = (canonical_homomorphism A) ** g & ( for G being GeneratorSet of Free (S,Y) st G = FreeGen Y holds
g || G = h || G ) )
A5: (canonical_homomorphism A) ** g is_homomorphism Free (S,Y),A by A3, A4, MSUALG_3:10;

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

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

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

let y be object ; :: thesis: ( y in F . s implies ((h || F) . x) . y = ((((canonical_homomorphism A) ** g) || F) . x) . y )
assume A7: y in F . s ; :: thesis: ((h || F) . x) . y = ((((canonical_homomorphism A) ** g) || F) . x) . y
A8: (g . s) . y = ((g . s) | (F . s)) . y by A7, FUNCT_1:49
.= ((h || F) . s) . y by A4, MSAFREE:def 1 ;
then A9: (g . s) . y in the Sorts of A . s by A7, FUNCT_2:5;
A10: F . s c= the Sorts of (Free (S,Y)) . s by PBOOLE:def 2, PBOOLE:def 18;
A11: dom ((canonical_homomorphism A) ** g) = the carrier of S /\ the carrier of S by PARTFUN1:def 2;
thus ((h || F) . x) . y = ((canonical_homomorphism A) . s) . ((g . s) . y) by A8, A9, Th47
.= (((canonical_homomorphism A) . s) * (g . s)) . y by A7, A10, FUNCT_2:15
.= (((canonical_homomorphism A) ** g) . s) . y by A11, PBOOLE:def 19
.= ((((canonical_homomorphism A) ** g) . s) | (F . s)) . y by A7, FUNCT_1:49
.= ((((canonical_homomorphism A) ** g) || F) . x) . y by MSAFREE:def 1 ; :: thesis: verum

end;

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

end;

hence h = (canonical_homomorphism A) ** g by A1, A5, EXTENS_1:19, PBOOLE:3; :: thesis: for G being GeneratorSet of Free (S,Y) st G = FreeGen Y holds
g || G = h || G
thus for G being GeneratorSet of Free (S,Y) st G = FreeGen Y holds
g || G = h || G by A4; :: thesis: verum