let S1 be OrderSortedSign; :: thesis: for U1, U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted 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 & F1 is order-sorted & F2 is order-sorted )

let U1, U2 be non-empty OSAlgebra of S1; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted 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 & F1 is order-sorted & F2 is order-sorted )

let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 & F is order-sorted 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 & F1 is order-sorted & F2 is order-sorted ) )

assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted ; :: 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 & F1 is order-sorted & F2 is order-sorted )

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 S1 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 S1 implies H . i is Function of ( the Sorts of () . i),( the Sorts of U2 . i) )
assume A3: i in the carrier of S1 ; :: 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;
reconsider h = H . i as Function of ( the Sorts of () . i),( the Sorts of () . i) by ;
A4: dom f = the Sorts of U1 . i by ;
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 FUNCT_2:7;
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 ;
consider F1 being ManySortedFunction of U1,() such that
A5: ( F1 = F & F1 is order-sorted ) and
A6: F1 is_epimorphism U1, Image F by A1, A2, Th15;
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 & F1 is order-sorted & F2 is order-sorted )

take F2 ; :: thesis: ( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus F1 is_epimorphism U1, Image F by A6; :: thesis: ( F2 is_monomorphism Image F,U2 & F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus F2 is_monomorphism Image F,U2 by MSUALG_3:22; :: thesis: ( F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus ( F = F2 ** F1 & F1 is order-sorted ) by ; :: thesis: F2 is order-sorted
Image F is order-sorted by A1, A2, Th11;
then the Sorts of () is OrderSortedSet of S1 by OSALG_1:17;
hence F2 is order-sorted ; :: thesis: verum