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 ;
then A3: the Sorts of () is OrderSortedSet of S1 by ;
then reconsider I = Image F as non-empty OSAlgebra of S1 by OSALG_1:17;
thus Image F is order-sorted by ; :: 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 ;
A6: G is_homomorphism U1,I by ;
A7: G is "onto" by ;
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 ;
A10: Args (o1,U1) c= Args (o2,U1) by ;
A11: dom (Den (o2,I)) = Args (o2,I) by FUNCT_2:def 1;
A12: (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) by ;
A13: the_result_sort_of o1 <= the_result_sort_of o2 by A8;
for a, b being object 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 object ; :: 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 ;
then consider y being Element of Args (o1,U1) such that
A17: G # y = a by ;
reconsider y1 = y as Element of Args (o2,U1) by A10;
A18: ( G # y1 = G # y & (Den (o2,U1)) . y = (Den (o1,U1)) . y ) by ;
set x = (Den (o1,U1)) . y;
(G . ()) . ((Den (o1,U1)) . y) = (Den (o1,I)) . a by ;
then A19: b = (G . ()) . ((Den (o1,U1)) . y) by ;
Result (o1,U1) = (O1 * the ResultSort of S1) . o1 by MSUALG_1:def 5
.= O1 . ( the ResultSort of S1 . o1) by
.= O1 . () by MSUALG_1:def 2
.= dom (G . ()) by FUNCT_2:def 1 ;
then (G . ()) . ((Den (o1,U1)) . y) = (G . ()) . ((Den (o1,U1)) . y) by A1, A4, A13;
then b = (Den (o2,I)) . a by ;
hence [a,b] in Den (o2,I) by ; :: 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