definition

let R be non empty Poset;
let F be ManySortedFunction of the carrier of R;
attr F is order-sorted means :Def1: :: OSALG_3:def 1
for s1, s2 being Element of R st s1 <= s2 holds
for a1 being set st a1 in dom (F . s1) holds
( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 );

end;

for R being non empty Poset
for F being ManySortedFunction of the carrier of R st F is order-sorted holds
for s1, s2 being Element of R st s1 <= s2 holds
( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 )

for R being non empty Poset
for A being OrderSortedSet of R
for B being V2 OrderSortedSet of R
for F being ManySortedFunction of A,B holds
( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds
for a1 being set st a1 in A . s1 holds
(F . s1) . a1 = (F . s2) . a1 )

for R being non empty Poset
for F being ManySortedFunction of the carrier of R st F is order-sorted holds
for w1, w2 being Element of the carrier of R * st w1 <= w2 holds
(F # ) . w1 c= (F # ) . w2

for R being non empty Poset
for A being OrderSortedSet of R holds id A is order-sorted

registration

let R be non empty Poset;
let A be OrderSortedSet of R;
cluster id A -> order-sorted ;
coherence by Th5;

end;

for R being non empty Poset
for A being OrderSortedSet of R
for B, C being V2 OrderSortedSet of R
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds
G ** F is order-sorted

for R being non empty Poset
for A, B being OrderSortedSet of R
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" & F is order-sorted holds
F "" is order-sorted

for R being non empty Poset
for A being OrderSortedSet of R
for F being ManySortedFunction of the carrier of R st F is order-sorted holds
F .:.: A is OrderSortedSet of R

definition

let S1 be OrderSortedSign;
let U1, U2 be OSAlgebra of S1;
pred U1,U2 are_os_isomorphic means :Def2: :: OSALG_3:def 2
ex F being ManySortedFunction of U1,U2 st
( F is_isomorphism U1,U2 & F is order-sorted );

end;

for S1 being OrderSortedSign
for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic

definition

let S1 be OrderSortedSign;
let U1, U2 be OSAlgebra of S1;
:: original: are_os_isomorphic
redefine pred U1,U2 are_os_isomorphic ;
reflexivity by Th9;

end;

definition

let S1 be OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S1;
:: original: are_os_isomorphic
redefine pred U1,U2 are_os_isomorphic ;
symmetry by Th10;

end;

for S1 being OrderSortedSign
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

for S1 being OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S1
for F being ManySortedFunction of U1,U2 st F is order-sorted holds
for o1, o2 being OperSymbol of S1 st o1 <= o2 holds
for x being Element of Args o1,U1
for x1 being Element of Args o2,U1 st x = x1 holds
F # x = F # x1

for S1 being OrderSortedSign
for U1 being monotone OSAlgebra of S1
for U2 being OSSubAlgebra of U1 holds U2 is monotone

registration

let S1 be OrderSortedSign;
let U1 be monotone OSAlgebra of S1;
cluster monotone MSSubAlgebra of U1;
existence

proof end;

end;

registration

let S1 be OrderSortedSign;
let U1 be monotone OSAlgebra of S1;
cluster -> monotone MSSubAlgebra of U1;
coherence by Th15;

end;

for S1 being OrderSortedSign
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 G being ManySortedFunction of U1,(Image F) st
( F = G & G is order-sorted & G is_epimorphism U1, Image F )

for S1 being OrderSortedSign
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 )

registration

let S1 be OrderSortedSign;
let U1 be OSAlgebra of S1;
cluster MSAlgebra(# the Sorts of U1,the Charact of U1 #) -> order-sorted ;
coherence

proof end;

end;

for S1 being OrderSortedSign
for U1 being OSAlgebra of S1 holds
( U1 is monotone iff MSAlgebra(# the Sorts of U1,the Charact of U1 #) is monotone )

for S1 being OrderSortedSign
for U1, U2 being strict non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds
( U1 is monotone iff U2 is monotone )