let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex F1 being ManySortedFunction of U1,() ex F2 being ManySortedFunction of (),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )

let U1, U2 be non-empty MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex F1 being ManySortedFunction of U1,() ex F2 being ManySortedFunction of (),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )

let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 implies ex F1 being ManySortedFunction of U1,() ex F2 being ManySortedFunction of (),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 ) )

assume A1: F is_homomorphism U1,U2 ; :: thesis: ex F1 being ManySortedFunction of U1,() ex F2 being ManySortedFunction of (),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )

then reconsider F1 = F as ManySortedFunction of U1,() by Lm3;
for H being ManySortedFunction of (),() holds H is ManySortedFunction of (),U2
proof
let H be ManySortedFunction of (),(); :: thesis: H is ManySortedFunction of (),U2
for i being object st i in the carrier of S holds
H . i is Function of ( the Sorts of () . i),( the Sorts of U2 . i)
proof
let i be object ; :: thesis: ( i in the carrier of S implies H . i is Function of ( the Sorts of () . i),( the Sorts of U2 . i) )
assume A2: i in the carrier of S ; :: thesis: H . i is Function of ( the Sorts of () . i),( the Sorts of U2 . i)
then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def 15;
A3: dom f = the Sorts of U1 . i by ;
reconsider h = H . i as Function of ( the Sorts of () . i),( the Sorts of () . i) by ;
A4: rng f c= the Sorts of U2 . i by RELAT_1:def 19;
the Sorts of () = F .:.: the Sorts of U1 by ;
then the Sorts of () . i = f .: ( the Sorts of U1 . i) by
.= rng f by ;
then h is Function of ( the Sorts of () . i),( the Sorts of U2 . i) by ;
hence H . i is Function of ( the Sorts of () . i),( the Sorts of U2 . i) ; :: thesis: verum
end;
hence H is ManySortedFunction of (),U2 by PBOOLE:def 15; :: thesis: verum
end;
then reconsider F2 = id the Sorts of () as ManySortedFunction of (),U2 ;
take F1 ; :: thesis: ex F2 being ManySortedFunction of (),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )

take F2 ; :: thesis: ( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
thus F1 is_epimorphism U1, Image F by ; :: thesis: ( F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
thus F2 is_monomorphism Image F,U2 by Th22; :: thesis: F = F2 ** F1
thus F = F2 ** F1 by Th4; :: thesis: verum