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,(Image F) ex F2 being ManySortedFunction of (Image F),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,(Image F) ex F2 being ManySortedFunction of (Image F),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,(Image F) ex F2 being ManySortedFunction of (Image F),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,(Image F) ex F2 being ManySortedFunction of (Image F),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 (Image F),(Image F) holds H is ManySortedFunction of (Image F),U2

consider F1 being ManySortedFunction of U1,(Image F) 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 (Image F),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 A5, MSUALG_3:4; :: thesis: F2 is order-sorted

Image F is order-sorted by A1, A2, Th11;

then the Sorts of (Image F) is OrderSortedSet of S1 by OSALG_1:17;

hence F2 is order-sorted ; :: thesis: verum

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),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,(Image F) ex F2 being ManySortedFunction of (Image F),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,(Image F) ex F2 being ManySortedFunction of (Image F),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,(Image F) ex F2 being ManySortedFunction of (Image F),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 (Image F),(Image F) holds H is ManySortedFunction of (Image F),U2

proof

then reconsider F2 = id the Sorts of (Image F) as ManySortedFunction of (Image F),U2 ;
let H be ManySortedFunction of (Image F),(Image F); :: thesis: H is ManySortedFunction of (Image F),U2

for i being object st i in the carrier of S1 holds

H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i)

end;for i being object st i in the carrier of S1 holds

H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i)

proof

hence
H is ManySortedFunction of (Image F),U2
by PBOOLE:def 15; :: thesis: verum
let i be object ; :: thesis: ( i in the carrier of S1 implies H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) )

assume A3: i in the carrier of S1 ; :: thesis: H . i is Function of ( the Sorts of (Image F) . 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 (Image F) . i),( the Sorts of (Image F) . i) by A3, PBOOLE:def 15;

A4: dom f = the Sorts of U1 . i by A3, FUNCT_2:def 1;

the Sorts of (Image F) = F .:.: the Sorts of U1 by A1, MSUALG_3:def 12;

then the Sorts of (Image F) . i = f .: ( the Sorts of U1 . i) by A3, PBOOLE:def 20

.= rng f by A4, RELAT_1:113 ;

then h is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) by FUNCT_2:7;

hence H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) ; :: thesis: verum

end;assume A3: i in the carrier of S1 ; :: thesis: H . i is Function of ( the Sorts of (Image F) . 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 (Image F) . i),( the Sorts of (Image F) . i) by A3, PBOOLE:def 15;

A4: dom f = the Sorts of U1 . i by A3, FUNCT_2:def 1;

the Sorts of (Image F) = F .:.: the Sorts of U1 by A1, MSUALG_3:def 12;

then the Sorts of (Image F) . i = f .: ( the Sorts of U1 . i) by A3, PBOOLE:def 20

.= rng f by A4, RELAT_1:113 ;

then h is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) by FUNCT_2:7;

hence H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) ; :: thesis: verum

consider F1 being ManySortedFunction of U1,(Image F) 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 (Image F),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 A5, MSUALG_3:4; :: thesis: F2 is order-sorted

Image F is order-sorted by A1, A2, Th11;

then the Sorts of (Image F) is OrderSortedSet of S1 by OSALG_1:17;

hence F2 is order-sorted ; :: thesis: verum