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, Th7;

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

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 8;

A7: G is "onto" by A5, MSUALG_3:def 8;

for o1, o2 being OperSymbol of S1 st o1 <= o2 holds

Den (o1,I) c= Den (o2,I)

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, Th7;

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

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 8;

A7: G is "onto" by A5, MSUALG_3:def 8;

for o1, o2 being OperSymbol of S1 st o1 <= o2 holds

Den (o1,I) c= Den (o2,I)

proof

hence
Image F is monotone OSAlgebra of S1
by OSALG_1:27; :: thesis: verum
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 21;

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)

end;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 21;

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

hence
Den (o1,I) c= Den (o2,I)
by RELAT_1:def 3; :: thesis: verum
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 A15, ZFMISC_1:87;

then consider y being Element of Args (o1,U1) such that

A17: G # y = a by A7, MSUALG_9:17;

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 A1, A4, A8, A12, Th12, FUNCT_1:49;

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 7;

then A19: b = (G . (the_result_sort_of o1)) . ((Den (o1,U1)) . y) by A15, FUNCT_1:1;

Result (o1,U1) = (O1 * the ResultSort of S1) . o1 by MSUALG_1:def 5

.= O1 . ( the ResultSort of S1 . o1) by A14, FUNCT_1:13

.= O1 . (the_result_sort_of o1) by MSUALG_1:def 2

.= 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;

then b = (Den (o2,I)) . a by A6, A17, A19, A18, MSUALG_3:def 7;

hence [a,b] in Den (o2,I) by A9, A11, A16, FUNCT_1:1; :: thesis: verum

end;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 A15, ZFMISC_1:87;

then consider y being Element of Args (o1,U1) such that

A17: G # y = a by A7, MSUALG_9:17;

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 A1, A4, A8, A12, Th12, FUNCT_1:49;

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 7;

then A19: b = (G . (the_result_sort_of o1)) . ((Den (o1,U1)) . y) by A15, FUNCT_1:1;

Result (o1,U1) = (O1 * the ResultSort of S1) . o1 by MSUALG_1:def 5

.= O1 . ( the ResultSort of S1 . o1) by A14, FUNCT_1:13

.= O1 . (the_result_sort_of o1) by MSUALG_1:def 2

.= 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;

then b = (Den (o2,I)) . a by A6, A17, A19, A18, MSUALG_3:def 7;

hence [a,b] in Den (o2,I) by A9, A11, A16, FUNCT_1:1; :: thesis: verum