let S be non empty non void ManySortedSign ; :: thesis: for U0, U1 being non-empty MSAlgebra over S
for W being strict non-empty free MSAlgebra over S
for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds
for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
let U0, U1 be non-empty MSAlgebra over S; :: thesis: for W being strict non-empty free MSAlgebra over S
for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds
for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
let W be strict non-empty free MSAlgebra over S; :: thesis: for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds
for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
let F be ManySortedFunction of U0,U1; :: thesis: ( F is_epimorphism U0,U1 implies for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H ) )
assume A1: F is_epimorphism U0,U1 ; :: thesis: for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
set sU0 = the Sorts of U0;
set sU1 = the Sorts of U1;
set I = the carrier of S;
let G be ManySortedFunction of W,U1; :: thesis: ( G is_homomorphism W,U1 implies ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H ) )
assume A2: G is_homomorphism W,U1 ; :: thesis: ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )
consider Gen being GeneratorSet of W such that
A3: Gen is free by MSAFREE:def 6;
defpred S₁[ object , object , object ] means ex f being Function of ( the Sorts of U0 . $3),( the Sorts of U1 . $3) ex g being Function of (Gen . $3),( the Sorts of U1 . $3) st
( f = F . $3 & g = (G || Gen) . $3 & $1 in f " {(g . $2)} );
A4: for i being object st i in the carrier of S holds
for x being object st x in Gen . i holds
ex y being object st
( y in the Sorts of U0 . i & S₁[y,x,i] )

proof

let i be object ; :: thesis: ( i in the carrier of S implies for x being object st x in Gen . i holds
ex y being object st
( y in the Sorts of U0 . i & S₁[y,x,i] ) )
assume A5: i in the carrier of S ; :: thesis: for x being object st x in Gen . i holds
ex y being object st
( y in the Sorts of U0 . i & S₁[y,x,i] )
reconsider g = (G || Gen) . i as Function of (Gen . i),( the Sorts of U1 . i) by A5, PBOOLE:def 15;
reconsider f = F . i as Function of ( the Sorts of U0 . i),( the Sorts of U1 . i) by A5, PBOOLE:def 15;
let x be object ; :: thesis: ( x in Gen . i implies ex y being object st
( y in the Sorts of U0 . i & S₁[y,x,i] ) )
assume x in Gen . i ; :: thesis: ex y being object st
( y in the Sorts of U0 . i & S₁[y,x,i] )
then A6: g . x in the Sorts of U1 . i by A5, FUNCT_2:5;
F is "onto" by A1;
then rng (F . i) = the Sorts of U1 . i by A5;
then f " {(g . x)} <> {} by A6, FUNCT_2:41;
then consider y being object such that
A7: y in f " {(g . x)} by XBOOLE_0:def 1;
take y ; :: thesis: ( y in the Sorts of U0 . i & S₁[y,x,i] )
thus y in the Sorts of U0 . i by A7; :: thesis: S₁[y,x,i]
thus S₁[y,x,i] by A7; :: thesis: verum

end;

consider H being ManySortedFunction of Gen, the Sorts of U0 such that
A8: for i being object st i in the carrier of S holds
ex h being Function of (Gen . i),( the Sorts of U0 . i) st
( h = H . i & ( for x being object st x in Gen . i holds
S₁[h . x,x,i] ) ) from MSSUBFAM:sch 1(A4);
consider H1 being ManySortedFunction of W,U0 such that
A9: H1 is_homomorphism W,U0 and
A10: H1 || Gen = H by A3;

now :: thesis: for i being object st i in the carrier of S holds
(G || Gen) . i = (F ** H) . i

let i be object ; :: thesis: ( i in the carrier of S implies (G || Gen) . i = (F ** H) . i )
assume A11: i in the carrier of S ; :: thesis: (G || Gen) . i = (F ** H) . i
then reconsider f9 = F . i as Function of ( the Sorts of U0 . i),( the Sorts of U1 . i) by PBOOLE:def 15;
reconsider g9 = (G || Gen) . i as Function of (Gen . i),( the Sorts of U1 . i) by A11, PBOOLE:def 15;
consider h being Function of (Gen . i),( the Sorts of U0 . i) such that
A12: h = H . i and
A13: for x being object st x in Gen . i holds
ex f being Function of ( the Sorts of U0 . i),( the Sorts of U1 . i) ex g being Function of (Gen . i),( the Sorts of U1 . i) st
( f = F . i & g = (G || Gen) . i & h . x in f " {(g . x)} ) by A8, A11;

A14: now :: thesis: for x being object st x in Gen . i holds
(f9 * h) . x = g9 . x

let x be object ; :: thesis: ( x in Gen . i implies (f9 * h) . x = g9 . x )
assume A15: x in Gen . i ; :: thesis: (f9 * h) . x = g9 . x
then consider f being Function of ( the Sorts of U0 . i),( the Sorts of U1 . i), g being Function of (Gen . i),( the Sorts of U1 . i) such that
A16: ( f = F . i & g = (G || Gen) . i ) and
A17: h . x in f " {(g . x)} by A13;
f . (h . x) in {(g . x)} by A11, A17, FUNCT_2:38;
then f . (h . x) = g . x by TARSKI:def 1;
hence (f9 * h) . x = g9 . x by A15, A16, A17, FUNCT_2:15; :: thesis: verum

end;

( Gen . i = dom g9 & Gen . i = dom (f9 * h) ) by A11, FUNCT_2:def 1;
then g9 = f9 * h by A14, FUNCT_1:2;
hence (G || Gen) . i = (F ** H) . i by A11, A12, MSUALG_3:2; :: thesis: verum

end;

then G || Gen = F ** (H1 || Gen) by A10;
then A18: G || Gen = (F ** H1) || Gen by EXTENS_1:4;
take H1 ; :: thesis: ( H1 is_homomorphism W,U0 & G = F ** H1 )
thus H1 is_homomorphism W,U0 by A9; :: thesis: G = F ** H1
F is_homomorphism U0,U1 by A1;
then F ** H1 is_homomorphism W,U1 by A9, MSUALG_3:10;
hence G = F ** H1 by A2, A18, EXTENS_1:19; :: thesis: verum