let S1 be OrderSortedSign; :: thesis: for U1 being non-empty monotone OSAlgebra of S1
for U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds
( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
let U1 be non-empty monotone OSAlgebra of S1; :: thesis: for U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds
( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
let U2 be non-empty OSAlgebra of S1; :: thesis: for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds
( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
let F be ManySortedFunction of U1,U2; :: thesis: ( F is order-sorted & F is_homomorphism U1,U2 implies ( Image F is order-sorted & Image F is monotone OSAlgebra of S1 ) )
assume that
A1: F is order-sorted and
A2: F is_homomorphism U1,U2 ; :: thesis: ( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )
reconsider O1 = the Sorts of U1 as OrderSortedSet of S1 by OSALG_1:17;
F .:.: O1 is OrderSortedSet of S1 by A1, Th8;
then A3: the Sorts of (Image F) is OrderSortedSet of S1 by A2, MSUALG_3:def 14;
then reconsider I = Image F as non-empty OSAlgebra of S1 by OSALG_1:17;
thus Image F is order-sorted by A3, OSALG_1:17; :: thesis: Image F is monotone OSAlgebra of S1
consider G being ManySortedFunction of U1,I such that
A4: F = G and
A5: G is_epimorphism U1,I by A2, MSUALG_3:21;
A6: G is_homomorphism U1,I by A5, MSUALG_3:def 10;
A7: G is "onto" by A5, MSUALG_3:def 10;
for o1, o2 being OperSymbol of S1 st o1 <= o2 holds
Den o1,I c= Den o2,I

proof

let o1, o2 be OperSymbol of S1; :: thesis: ( o1 <= o2 implies Den o1,I c= Den o2,I )
assume A8: o1 <= o2 ; :: thesis: Den o1,I c= Den o2,I
A9: Args o1,I c= Args o2,I by A8, OSALG_1:26;
A10: Args o1,U1 c= Args o2,U1 by A8, OSALG_1:26;
A11: dom (Den o2,I) = Args o2,I by FUNCT_2:def 1;
A12: (Den o2,U1) | (Args o1,U1) = Den o1,U1 by A8, OSALG_1:def 23;
A13: the_result_sort_of o1 <= the_result_sort_of o2 by A8, OSALG_1:def 22;
for a, b being set st [a,b] in Den o1,I holds
[a,b] in Den o2,I

proof

set s1 = the_result_sort_of o1;
set s2 = the_result_sort_of o2;
o1 in the carrier' of S1 ;
then A14: o1 in dom the ResultSort of S1 by FUNCT_2:def 1;
let a, b be set ; :: thesis: ( [a,b] in Den o1,I implies [a,b] in Den o2,I )
assume A15: [a,b] in Den o1,I ; :: thesis: [a,b] in Den o2,I
A16: a in Args o1,I by A15, ZFMISC_1:106;
then consider y being Element of Args o1,U1 such that
A17: G # y = a by A7, MSUALG_9:18;
reconsider y1 = y as Element of Args o2,U1 by A10, TARSKI:def 3;
A18: ( G # y1 = G # y & (Den o2,U1) . y = (Den o1,U1) . y ) by A1, A4, A8, A12, Th13, FUNCT_1:72;
set x = (Den o1,U1) . y;
(G . (the_result_sort_of o1)) . ((Den o1,U1) . y) = (Den o1,I) . a by A6, A17, MSUALG_3:def 9;
then A19: b = (G . (the_result_sort_of o1)) . ((Den o1,U1) . y) by A15, FUNCT_1:8;
Result o1,U1 = (O1 * the ResultSort of S1) . o1 by MSUALG_1:def 10
.= O1 . (the ResultSort of S1 . o1) by A14, FUNCT_1:23
.= O1 . (the_result_sort_of o1) by MSUALG_1:def 7
.= dom (G . (the_result_sort_of o1)) by FUNCT_2:def 1 ;
then (G . (the_result_sort_of o1)) . ((Den o1,U1) . y) = (G . (the_result_sort_of o2)) . ((Den o1,U1) . y) by A1, A4, A13, Def1;
then b = (Den o2,I) . a by A6, A17, A19, A18, MSUALG_3:def 9;
hence [a,b] in Den o2,I by A9, A11, A16, FUNCT_1:8; :: thesis: verum

end;

hence Den o1,I c= Den o2,I by RELAT_1:def 3; :: thesis: verum

end;

hence Image F is monotone OSAlgebra of S1 by OSALG_1:27; :: thesis: verum