let S1 be OrderSortedSign; :: thesis: for U1, 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

let U1, 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

let F be ManySortedFunction of U1,U2; :: thesis: ( F is order-sorted & F is_homomorphism U1,U2 implies Image F is order-sorted )

assume that

A1: F is order-sorted and

A2: F is_homomorphism U1,U2 ; :: thesis: Image F is order-sorted

reconsider O1 = the Sorts of U1 as OrderSortedSet of S1 by OSALG_1:17;

F .:.: O1 is OrderSortedSet of S1 by A1, Th7;

then the Sorts of (Image F) is OrderSortedSet of S1 by A2, MSUALG_3:def 12;

hence Image F is order-sorted by OSALG_1:17; :: thesis: verum

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

Image F is order-sorted

let U1, 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

let F be ManySortedFunction of U1,U2; :: thesis: ( F is order-sorted & F is_homomorphism U1,U2 implies Image F is order-sorted )

assume that

A1: F is order-sorted and

A2: F is_homomorphism U1,U2 ; :: thesis: Image F is order-sorted

reconsider O1 = the Sorts of U1 as OrderSortedSet of S1 by OSALG_1:17;

F .:.: O1 is OrderSortedSet of S1 by A1, Th7;

then the Sorts of (Image F) is OrderSortedSet of S1 by A2, MSUALG_3:def 12;

hence Image F is order-sorted by OSALG_1:17; :: thesis: verum