:: OSALG_3 semantic presentation

begin


definition
let R be non empty Poset;
let F be ManySortedFunction of the carrier of R;
attrF 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;

:: deftheorem Def1 defines order-sorted OSALG_3:def_1_:_
 for R being non empty Poset
for F being ManySortedFunction of the carrier of R holds
( F is order-sorted iff 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 ) );

theorem Th1: :: OSALG_3:1
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 )
proof
let R be non empty Poset; ::_thesis: 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 )
let F be ManySortedFunction of the carrier of R; ::_thesis: ( F is order-sorted implies for s1, s2 being Element of R st s1 <= s2 holds
( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 ) )
assume A1: F is order-sorted ; ::_thesis: for s1, s2 being Element of R st s1 <= s2 holds
( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 )
let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies ( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 ) )
assume A2: s1 <= s2 ; ::_thesis: ( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 )
thus  dom (F . s1) c= dom (F . s2) ::_thesis: F . s1 c= F . s2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (F . s1) or x in dom (F . s2) )
assume  x in dom (F . s1) ; ::_thesis: x in dom (F . s2)
hence  x in dom (F . s2) by A1, A2, Def1; ::_thesis: verum
end;
 for a, b being set st [a,b] in F . s1 holds
[a,b] in F . s2
proof
let y, z be set ; ::_thesis: ( [y,z] in F . s1 implies [y,z] in F . s2 )
assume A3: [y,z] in F . s1 ; ::_thesis: [y,z] in F . s2
 y in dom (F . s1) by A3, XTUPLE_0:def_12;
then A4: ( y in dom (F . s2) & (F . s1) . y = (F . s2) . y ) by A1, A2, Def1;
 (F . s1) . y = z by A3, FUNCT_1:1;
hence  [y,z] in F . s2 by A4, FUNCT_1:1; ::_thesis: verum
end;
hence  F . s1 c= F . s2 by RELAT_1:def_3; ::_thesis: verum
end;

theorem Th2: :: OSALG_3:2
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 )
proof
let R be non empty Poset; ::_thesis: 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 )
let A be OrderSortedSet of R; ::_thesis: 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 )
let B be V2() OrderSortedSet of R; ::_thesis: 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 )
let F be ManySortedFunction of A,B; ::_thesis: ( 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 )
hereby  ::_thesis: ( ( 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 ) implies F is order-sorted )
assume A1: F is order-sorted ; ::_thesis: 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
let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies for a1 being set st a1 in A . s1 holds
(F . s1) . a1 = (F . s2) . a1 )
assume A2: s1 <= s2 ; ::_thesis: for a1 being set st a1 in A . s1 holds
(F . s1) . a1 = (F . s2) . a1
let a1 be set ; ::_thesis: ( a1 in A . s1 implies (F . s1) . a1 = (F . s2) . a1 )
assume  a1 in A . s1 ; ::_thesis: (F . s1) . a1 = (F . s2) . a1
then  a1 in dom (F . s1) by FUNCT_2:def_1;
hence  (F . s1) . a1 = (F . s2) . a1 by A1, A2, Def1; ::_thesis: verum
end;
assume A3: 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 ; ::_thesis: F is order-sorted
let s1, s2 be Element of R; :: according to OSALG_3:def_1 ::_thesis: ( s1 <= s2 implies for a1 being set st a1 in dom (F . s1) holds
( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) )
assume A4: s1 <= s2 ; ::_thesis: for a1 being set st a1 in dom (F . s1) holds
( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 )
A5: ( dom (F . s1) = A . s1 & dom (F . s2) = A . s2 ) by FUNCT_2:def_1;
let a1 be set ; ::_thesis: ( a1 in dom (F . s1) implies ( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) )
assume A6: a1 in dom (F . s1) ; ::_thesis: ( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 )
 A . s1 c= A . s2 by A4, OSALG_1:def_16;
hence  a1 in dom (F . s2) by A6, A5; ::_thesis: (F . s1) . a1 = (F . s2) . a1
thus  (F . s1) . a1 = (F . s2) . a1 by A3, A4, A6; ::_thesis: verum
end;

theorem :: OSALG_3:3
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
proof
let R be non empty Poset; ::_thesis: 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
let F be ManySortedFunction of the carrier of R; ::_thesis: ( F is order-sorted implies for w1, w2 being Element of the carrier of R * st w1 <= w2 holds
(F #) . w1 c= (F #) . w2 )
assume A1: F is order-sorted ; ::_thesis: for w1, w2 being Element of the carrier of R * st w1 <= w2 holds
(F #) . w1 c= (F #) . w2
let w1, w2 be Element of the carrier of R * ; ::_thesis: ( w1 <= w2 implies (F #) . w1 c= (F #) . w2 )
assume A2: w1 <= w2 ; ::_thesis: (F #) . w1 c= (F #) . w2
A3: len w1 = len w2 by A2, OSALG_1:def_6;
then A4: dom w1 = dom w2 by FINSEQ_3:29;
thus  (F #) . w1 c= (F #) . w2 ::_thesis: verum
proof
set a = (F #) . w1;
set b = (F #) . w2;
A5: (F #) . w1 = product (F * w1) by FINSEQ_2:def_5;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (F #) . w1 or x in (F #) . w2 )
assume  x in (F #) . w1 ; ::_thesis: x in (F #) . w2
then consider g being Function such that
A6: ( x = g & dom g = dom (F * w1) ) and
A7: for y being set st y in dom (F * w1) holds
g . y in (F * w1) . y by A5, CARD_3:def_5;
A8: dom F = the carrier of R by PARTFUN1:def_2;
 rng w2 c= the carrier of R ;
then A9: dom (F * w2) = dom w2 by A8, RELAT_1:27;
 rng w1 c= the carrier of R ;
then A10: dom (F * w1) = dom w1 by A8, RELAT_1:27;
A11: for z being set st z in dom (F * w2) holds
g . z in (F * w2) . z
proof
let z be set ; ::_thesis: ( z in dom (F * w2) implies g . z in (F * w2) . z )
assume A12: z in dom (F * w2) ; ::_thesis: g . z in (F * w2) . z
A13: (F * w2) . z = F . (w2 . z) by A12, FUNCT_1:12;
 ( w1 . z in rng w1 & w2 . z in rng w2 ) by A4, A9, A12, FUNCT_1:3;
then reconsider s1 = w1 . z, s2 = w2 . z as Element of R ;
 z in dom (F * w1) by A3, A10, A9, A12, FINSEQ_3:29;
then  s1 <= s2 by A2, A10, OSALG_1:def_6;
then A14: F . s1 c= F . s2 by A1, Th1;
 ( g . z in (F * w1) . z & (F * w1) . z = F . (w1 . z) ) by A4, A7, A10, A9, A12, FUNCT_1:12;
hence  g . z in (F * w2) . z by A13, A14; ::_thesis: verum
end;
 (F #) . w2 = product (F * w2) by FINSEQ_2:def_5;
hence  x in (F #) . w2 by A4, A6, A10, A9, A11, CARD_3:def_5; ::_thesis: verum
end;
end;

theorem Th4: :: OSALG_3:4
for R being non empty Poset
for A being OrderSortedSet of R holds id A is order-sorted
proof
let R be non empty Poset; ::_thesis: for A being OrderSortedSet of R holds id A is order-sorted
let A be OrderSortedSet of R; ::_thesis: id A is order-sorted
set F = id A;
let s1, s2 be Element of R; :: according to OSALG_3:def_1 ::_thesis: ( s1 <= s2 implies for a1 being set st a1 in dom ((id A) . s1) holds
( a1 in dom ((id A) . s2) & ((id A) . s1) . a1 = ((id A) . s2) . a1 ) )
assume  s1 <= s2 ; ::_thesis: for a1 being set st a1 in dom ((id A) . s1) holds
( a1 in dom ((id A) . s2) & ((id A) . s1) . a1 = ((id A) . s2) . a1 )
then A1: A . s1 c= A . s2 by OSALG_1:def_16;
let a1 be set ; ::_thesis: ( a1 in dom ((id A) . s1) implies ( a1 in dom ((id A) . s2) & ((id A) . s1) . a1 = ((id A) . s2) . a1 ) )
assume A2: a1 in dom ((id A) . s1) ; ::_thesis: ( a1 in dom ((id A) . s2) & ((id A) . s1) . a1 = ((id A) . s2) . a1 )
 ( A . s1 = {} implies A . s1 = {} ) ;
then A3: dom ((id A) . s1) = A . s1 by FUNCT_2:def_1;
 ( A . s2 = {} implies A . s2 = {} ) ;
then  dom ((id A) . s2) = A . s2 by FUNCT_2:def_1;
hence  a1 in dom ((id A) . s2) by A2, A3, A1; ::_thesis: ((id A) . s1) . a1 = ((id A) . s2) . a1
((id A) . s1) . a1 = (id (A . s1)) . a1 by MSUALG_3:def_1
.= a1 by A2, FUNCT_1:18
.= (id (A . s2)) . a1 by A2, A3, A1, FUNCT_1:18
.= ((id A) . s2) . a1 by MSUALG_3:def_1 ;
hence  ((id A) . s1) . a1 = ((id A) . s2) . a1 ; ::_thesis: verum
end;

registration
let R be non empty Poset;
let A be OrderSortedSet of R;
cluster id A ->  order-sorted ;
coherence
 id A is order-sorted by Th4;
end;

theorem Th5: :: OSALG_3:5
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
proof
let R be non empty Poset; ::_thesis: 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
let A be OrderSortedSet of R; ::_thesis: 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
let B, C be V2() OrderSortedSet of R; ::_thesis: 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
let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds
G ** F is order-sorted
let G be ManySortedFunction of B,C; ::_thesis: ( F is order-sorted & G is order-sorted implies G ** F is order-sorted )
assume that
A1: F is order-sorted and
A2: G is order-sorted ; ::_thesis: G ** F is order-sorted
 for s1, s2 being Element of R st s1 <= s2 holds
for a1 being set st a1 in A . s1 holds
((G ** F) . s1) . a1 = ((G ** F) . s2) . a1
proof
let s1, s2 be Element of R; ::_thesis: ( s1 <= s2 implies for a1 being set st a1 in A . s1 holds
((G ** F) . s1) . a1 = ((G ** F) . s2) . a1 )
assume A3: s1 <= s2 ; ::_thesis: for a1 being set st a1 in A . s1 holds
((G ** F) . s1) . a1 = ((G ** F) . s2) . a1
A4: A . s1 c= A . s2 by A3, OSALG_1:def_16;
let a1 be set ; ::_thesis: ( a1 in A . s1 implies ((G ** F) . s1) . a1 = ((G ** F) . s2) . a1 )
assume A5: a1 in A . s1 ; ::_thesis: ((G ** F) . s1) . a1 = ((G ** F) . s2) . a1
A6: (F . s1) . a1 = (F . s2) . a1 by A1, A3, A5, Th2;
 (F . s1) . a1 in B . s1 by A5, FUNCT_2:5;
then A7: (G . s1) . ((F . s2) . a1) = (G . s2) . ((F . s2) . a1) by A2, A3, A6, Th2;
((G ** F) . s1) . a1 = ((G . s1) * (F . s1)) . a1 by MSUALG_3:2
.= (G . s1) . ((F . s2) . a1) by A5, A6, FUNCT_2:15
.= ((G . s2) * (F . s2)) . a1 by A5, A4, A7, FUNCT_2:15
.= ((G ** F) . s2) . a1 by MSUALG_3:2 ;
hence  ((G ** F) . s1) . a1 = ((G ** F) . s2) . a1 ; ::_thesis: verum
end;
hence  G ** F is order-sorted by Th2; ::_thesis: verum
end;

theorem Th6: :: OSALG_3:6
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
proof
let R be non empty Poset; ::_thesis: 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
let A, B be OrderSortedSet of R; ::_thesis: for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" & F is order-sorted holds
F "" is order-sorted
let F be ManySortedFunction of A,B; ::_thesis: ( F is "1-1" & F is "onto" & F is order-sorted implies F "" is order-sorted )
assume that
A1: F is "1-1" and
A2: F is "onto" and
A3: F is order-sorted ; ::_thesis: F "" is order-sorted
let s1, s2 be Element of R; :: according to OSALG_3:def_1 ::_thesis: ( s1 <= s2 implies for a1 being set st a1 in dom ((F "") . s1) holds
( a1 in dom ((F "") . s2) & ((F "") . s1) . a1 = ((F "") . s2) . a1 ) )
assume A4: s1 <= s2 ; ::_thesis: for a1 being set st a1 in dom ((F "") . s1) holds
( a1 in dom ((F "") . s2) & ((F "") . s1) . a1 = ((F "") . s2) . a1 )
A5: B . s1 c= B . s2 by A4, OSALG_1:def_16;
A6: (F "") . s2 = (F . s2) " by A1, A2, MSUALG_3:def_4;
A7: A . s1 c= A . s2 by A4, OSALG_1:def_16;
 s1 in the carrier of R ;
then  s1 in dom F by PARTFUN1:def_2;
then A8: F . s1 is one-to-one by A1, MSUALG_3:def_2;
 s2 in the carrier of R ;
then  s2 in dom F by PARTFUN1:def_2;
then A9: F . s2 is one-to-one by A1, MSUALG_3:def_2;
let a1 be set ; ::_thesis: ( a1 in dom ((F "") . s1) implies ( a1 in dom ((F "") . s2) & ((F "") . s1) . a1 = ((F "") . s2) . a1 ) )
assume A10: a1 in dom ((F "") . s1) ; ::_thesis: ( a1 in dom ((F "") . s2) & ((F "") . s1) . a1 = ((F "") . s2) . a1 )
A11: a1 in B . s1 by A10;
then A12: dom (F . s2) = A . s2 by A5, FUNCT_2:def_1;
set c1 = ((F . s1) ") . a1;
set c2 = ((F . s2) ") . a1;
A13: dom (F . s1) = A . s1 by A10, FUNCT_2:def_1;
A14: (F "") . s1 = (F . s1) " by A1, A2, MSUALG_3:def_4;
then A15: ((F . s1) ") . a1 in rng ((F . s1) ") by A10, FUNCT_1:3;
A16: rng (F . s1) = B . s1 by A2, MSUALG_3:def_3;
then  (F . s1) " is Function of (B . s1),(A . s1) by A8, FUNCT_2:25;
then A17: rng ((F . s1) ") c= A . s1 by RELAT_1:def_19;
then A18: ((F . s1) ") . a1 in A . s1 by A15;
A19: rng (F . s2) = B . s2 by A2, MSUALG_3:def_3;
then A20: (F . s2) . (((F . s2) ") . a1) = a1 by A5, A9, A11, FUNCT_1:35
.= (F . s1) . (((F . s1) ") . a1) by A10, A16, A8, FUNCT_1:35
.= (F . s2) . (((F . s1) ") . a1) by A3, A4, A15, A17, A13, Def1 ;
 a1 in B . s2 by A5, A11;
hence  a1 in dom ((F "") . s2) by A7, A18, FUNCT_2:def_1; ::_thesis: ((F "") . s1) . a1 = ((F "") . s2) . a1
 (F . s2) " is Function of (B . s2),(A . s2) by A19, A9, FUNCT_2:25;
then  ((F . s2) ") . a1 in dom (F . s2) by A5, A7, A11, A18, A12, FUNCT_2:5;
hence  ((F "") . s1) . a1 = ((F "") . s2) . a1 by A7, A9, A14, A6, A18, A12, A20, FUNCT_1:def_4; ::_thesis: verum
end;

theorem Th7: :: OSALG_3:7
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
proof
let R be non empty Poset; ::_thesis: 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
let A be OrderSortedSet of R; ::_thesis: for F being ManySortedFunction of the carrier of R st F is order-sorted holds
F .:.: A is OrderSortedSet of R
let F be ManySortedFunction of the carrier of R; ::_thesis: ( F is order-sorted implies F .:.: A is OrderSortedSet of R )
assume A1: F is order-sorted ; ::_thesis: F .:.: A is OrderSortedSet of R
reconsider C1 = F .:.: A as ManySortedSet of R ;
 C1 is order-sorted
proof
let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or C1 . s1 c= C1 . s2 )
assume  s1 <= s2 ; ::_thesis: C1 . s1 c= C1 . s2
then A2: ( A . s1 c= A . s2 & F . s1 c= F . s2 ) by A1, Th1, OSALG_1:def_16;
 ( C1 . s1 = (F . s1) .: (A . s1) & C1 . s2 = (F . s2) .: (A . s2) ) by PBOOLE:def_20;
hence  C1 . s1 c= C1 . s2 by A2, RELAT_1:125; ::_thesis: verum
end;
hence  F .:.: A is OrderSortedSet of R ; ::_thesis: verum
end;

definition
let S1 be OrderSortedSign;
let U1, U2 be OSAlgebra of S1;
predU1,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;

:: deftheorem Def2 defines are_os_isomorphic OSALG_3:def_2_:_
 for S1 being OrderSortedSign
for U1, U2 being OSAlgebra of S1 holds
( U1,U2 are_os_isomorphic iff ex F being ManySortedFunction of U1,U2 st
( F is_isomorphism U1,U2 & F is order-sorted ) );

theorem Th8: :: OSALG_3:8
for S1 being OrderSortedSign
for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic
proof
let S1 be OrderSortedSign; ::_thesis: for U1 being OSAlgebra of S1 holds U1,U1 are_os_isomorphic
let U1 be OSAlgebra of S1; ::_thesis: U1,U1 are_os_isomorphic
take  id the Sorts of U1 ; :: according to OSALG_3:def_2 ::_thesis: ( id the Sorts of U1 is_isomorphism U1,U1 & id the Sorts of U1 is order-sorted )
 the Sorts of U1 is OrderSortedSet of S1 by OSALG_1:17;
hence  ( id the Sorts of U1 is_isomorphism U1,U1 & id the Sorts of U1 is order-sorted ) by MSUALG_3:16; ::_thesis: verum
end;

theorem Th9: :: OSALG_3:9
for S1 being OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds
U2,U1 are_os_isomorphic
proof
let S1 be OrderSortedSign; ::_thesis: for U1, U2 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds
U2,U1 are_os_isomorphic
let U1, U2 be non-empty OSAlgebra of S1; ::_thesis: ( U1,U2 are_os_isomorphic implies U2,U1 are_os_isomorphic )
A1: ( the Sorts of U1 is OrderSortedSet of S1 & the Sorts of U2 is OrderSortedSet of S1 ) by OSALG_1:17;
assume  U1,U2 are_os_isomorphic ; ::_thesis: U2,U1 are_os_isomorphic
then consider F being ManySortedFunction of U1,U2 such that
A2: F is_isomorphism U1,U2 and
A3: F is order-sorted by Def2;
reconsider G = F "" as ManySortedFunction of U2,U1 ;
A4: G is_isomorphism U2,U1 by A2, MSUALG_3:14;
 ( F is "onto" & F is "1-1" ) by A2, MSUALG_3:13;
then  F "" is order-sorted by A3, A1, Th6;
hence  U2,U1 are_os_isomorphic by A4, Def2; ::_thesis: verum
end;

definition
let S1 be OrderSortedSign;
let U1, U2 be OSAlgebra of S1;
:: original: are_os_isomorphic
redefine predU1,U2 are_os_isomorphic ;
reflexivity
 for U1 being OSAlgebra of S1 holds (S1,b1,b1) by Th8;
end;

definition
let S1 be OrderSortedSign;
let U1, U2 be non-empty OSAlgebra of S1;
:: original: are_os_isomorphic
redefine predU1,U2 are_os_isomorphic ;
symmetry
 for U1, U2 being non-empty OSAlgebra of S1 st (S1,b1,b2) holds
(S1,b2,b1) by Th9;
end;

theorem :: OSALG_3:10
for S1 being OrderSortedSign
for U1, U2, U3 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic holds
U1,U3 are_os_isomorphic
proof
let S1 be OrderSortedSign; ::_thesis: for U1, U2, U3 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic holds
U1,U3 are_os_isomorphic
let U1, U2, U3 be non-empty OSAlgebra of S1; ::_thesis: ( U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic implies U1,U3 are_os_isomorphic )
assume that
A1: U1,U2 are_os_isomorphic and
A2: U2,U3 are_os_isomorphic ; ::_thesis: U1,U3 are_os_isomorphic
consider F being ManySortedFunction of U1,U2 such that
A3: F is_isomorphism U1,U2 and
A4: F is order-sorted by A1, Def2;
consider G being ManySortedFunction of U2,U3 such that
A5: G is_isomorphism U2,U3 and
A6: G is order-sorted by A2, Def2;
reconsider H = G ** F as ManySortedFunction of U1,U3 ;
A7: H is_isomorphism U1,U3 by A3, A5, MSUALG_3:15;
A8: the Sorts of U3 is V2() OrderSortedSet of S1 by OSALG_1:17;
 ( the Sorts of U1 is V2() OrderSortedSet of S1 & the Sorts of U2 is V2() OrderSortedSet of S1 ) by OSALG_1:17;
then  H is order-sorted by A4, A6, A8, Th5;
hence  U1,U3 are_os_isomorphic by A7, Def2; ::_thesis: verum
end;

theorem Th11: :: OSALG_3:11
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
proof
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
end;

theorem Th12: :: OSALG_3:12
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
proof
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 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
let U1, U2 be non-empty OSAlgebra of S1; ::_thesis: 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
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is order-sorted implies 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 )
assume A1: F is order-sorted ; ::_thesis: 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
let o1, o2 be OperSymbol of S1; ::_thesis: ( o1 <= o2 implies for x being Element of Args (o1,U1)
for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1 )
assume A2: o1 <= o2 ; ::_thesis: for x being Element of Args (o1,U1)
for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1
let x be Element of Args (o1,U1); ::_thesis: for x1 being Element of Args (o2,U1) st x = x1 holds
F # x = F # x1
let x1 be Element of Args (o2,U1); ::_thesis: ( x = x1 implies F # x = F # x1 )
assume A3: x = x1 ; ::_thesis: F # x = F # x1
A4: dom x = dom (the_arity_of o1) by MSUALG_3:6;
A5: for n being set st n in dom x holds
(F # x) . n = (F # x1) . n
proof
let n1 be set ; ::_thesis: ( n1 in dom x implies (F # x) . n1 = (F # x1) . n1 )
assume A6: n1 in dom x ; ::_thesis: (F # x) . n1 = (F # x1) . n1
reconsider n2 = n1 as Nat by A6, ORDINAL1:def_12;
reconsider pi1 = (the_arity_of o1) /. n2, pi2 = (the_arity_of o2) /. n2 as Element of S1 ;
A7: (the_arity_of o1) /. n2 = (the_arity_of o1) . n2 by A4, A6, PARTFUN1:def_6;
A8: the_arity_of o1 <= the_arity_of o2 by A2, OSALG_1:def_20;
then  len (the_arity_of o1) = len (the_arity_of o2) by OSALG_1:def_6;
then  dom (the_arity_of o1) = dom (the_arity_of o2) by FINSEQ_3:29;
then  (the_arity_of o2) /. n2 = (the_arity_of o2) . n2 by A4, A6, PARTFUN1:def_6;
then A9: pi1 <= pi2 by A4, A6, A8, A7, OSALG_1:def_6;
 rng (the_arity_of o1) c= the carrier of S1 ;
then  rng (the_arity_of o1) c= dom the Sorts of U1 by PARTFUN1:def_2;
then A10: n2 in dom ( the Sorts of U1 * (the_arity_of o1)) by A4, A6, RELAT_1:27;
dom (F . pi1) = the Sorts of U1 . pi1 by FUNCT_2:def_1
.= the Sorts of U1 . ((the_arity_of o1) . n2) by A4, A6, PARTFUN1:def_6
.= ( the Sorts of U1 * (the_arity_of o1)) . n2 by A4, A6, FUNCT_1:13 ;
then A11: x1 . n2 in dom (F . pi1) by A3, A10, MSUALG_3:6;
(F # x) . n2 = (F . ((the_arity_of o1) /. n2)) . (x1 . n2) by A3, A6, MSUALG_3:def_6
.= (F . pi2) . (x1 . n2) by A1, A11, A9, Def1
.= (F # x1) . n2 by A3, A6, MSUALG_3:def_6 ;
hence  (F # x) . n1 = (F # x1) . n1 ; ::_thesis: verum
end;
 dom x1 = dom (the_arity_of o2) by MSUALG_3:6;
then A12: dom (F # x1) = dom x1 by MSUALG_3:6;
 dom (F # x) = dom x by A4, MSUALG_3:6;
hence  F # x = F # x1 by A3, A12, A5, FUNCT_1:2; ::_thesis: verum
end;

theorem Th13: :: OSALG_3:13
for S1 being OrderSortedSign
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 )
proof
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)
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_21;
A13: the_result_sort_of o1 <= the_result_sort_of o2 by A8, OSALG_1:def_20;
 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: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, TARSKI:def_3;
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, Def1;
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;
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
end;

theorem Th14: :: OSALG_3:14
for S1 being OrderSortedSign
for U1 being monotone OSAlgebra of S1
for U2 being OSSubAlgebra of U1 holds U2 is monotone
proof
let S1 be OrderSortedSign; ::_thesis: for U1 being monotone OSAlgebra of S1
for U2 being OSSubAlgebra of U1 holds U2 is monotone
let U1 be monotone OSAlgebra of S1; ::_thesis: for U2 being OSSubAlgebra of U1 holds U2 is monotone
let U2 be OSSubAlgebra of U1; ::_thesis: U2 is monotone
let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def_21 ::_thesis: ( not o1 <= o2 or (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2) )
assume A1: o1 <= o2 ; ::_thesis: (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2)
A2: Args (o1,U2) c= Args (o2,U2) by A1, OSALG_1:26;
 ( the Sorts of U2 is MSSubset of U1 & the Sorts of U2 is OrderSortedSet of S1 ) by MSUALG_2:def_9, OSALG_1:17;
then reconsider B = the Sorts of U2 as OSSubset of U1 by OSALG_2:def_2;
A3: B is opers_closed by MSUALG_2:def_9;
then A4: B is_closed_on o1 by MSUALG_2:def_6;
A5: B is_closed_on o2 by A3, MSUALG_2:def_6;
A6: Den (o2,U2) = the Charact of U2 . o2 by MSUALG_1:def_6
.= (Opers (U1,B)) . o2 by MSUALG_2:def_9
.= o2 /. B by MSUALG_2:def_8
.= (Den (o2,U1)) | (((B #) * the Arity of S1) . o2) by A5, MSUALG_2:def_7
.= (Den (o2,U1)) | (Args (o2,U2)) by MSUALG_1:def_4 ;
A7: Den (o1,U2) = the Charact of U2 . o1 by MSUALG_1:def_6
.= (Opers (U1,B)) . o1 by MSUALG_2:def_9
.= o1 /. B by MSUALG_2:def_8
.= (Den (o1,U1)) | (((B #) * the Arity of S1) . o1) by A4, MSUALG_2:def_7
.= (Den (o1,U1)) | (Args (o1,U2)) by MSUALG_1:def_4 ;
 (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) by A1, OSALG_1:def_21;
then  Den (o1,U2) = (Den (o2,U1)) | ((Args (o1,U1)) /\ (Args (o1,U2))) by A7, RELAT_1:71
.= (Den (o2,U1)) | (Args (o1,U2)) by MSAFREE3:37, XBOOLE_1:28
.= (Den (o2,U1)) | ((Args (o2,U2)) /\ (Args (o1,U2))) by A2, XBOOLE_1:28
.= (Den (o2,U2)) | (Args (o1,U2)) by A6, RELAT_1:71 ;
hence  (Den (o2,U2)) | (Args (o1,U2)) = Den (o1,U2) ; ::_thesis: verum
end;

registration
let S1 be OrderSortedSign;
let U1 be monotone OSAlgebra of S1;
cluster order-sorted monotone for MSSubAlgebra of U1;
existence
 ex b1 being OSSubAlgebra of U1 st b1 is monotone
proof
set U2 = the OSSubAlgebra of U1;
take  the OSSubAlgebra of U1 ; ::_thesis: the OSSubAlgebra of U1 is monotone
thus  the OSSubAlgebra of U1 is monotone by Th14; ::_thesis: verum
end;
end;

registration
let S1 be OrderSortedSign;
let U1 be monotone OSAlgebra of S1;
cluster order-sorted  ->  monotone for MSSubAlgebra of U1;
coherence
 for b1 being OSSubAlgebra of U1 holds b1 is monotone by Th14;
end;

theorem Th15: :: OSALG_3:15
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 )
proof
let S1 be OrderSortedSign; ::_thesis: 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 )
let U1, U2 be non-empty OSAlgebra of S1; ::_thesis: 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 )
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is order-sorted & G is_epimorphism U1, Image F ) )
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted ; ::_thesis: ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is order-sorted & G is_epimorphism U1, Image F )
consider G being ManySortedFunction of U1,(Image F) such that
A3: ( F = G & G is_epimorphism U1, Image F ) by A1, MSUALG_3:21;
take  G ; ::_thesis: ( F = G & G is order-sorted & G is_epimorphism U1, Image F )
thus  ( F = G & G is order-sorted & G is_epimorphism U1, Image F ) by A2, A3; ::_thesis: verum
end;

theorem :: OSALG_3:16
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 )
proof
let S1 be OrderSortedSign; ::_thesis: 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 )
let U1, U2 be non-empty OSAlgebra of S1; ::_thesis: 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 )
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 & F is order-sorted implies 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 ) )
assume that
A1: F is_homomorphism U1,U2 and
A2: F is order-sorted ; ::_thesis: 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 )
 for H being ManySortedFunction of (Image F),(Image F) holds H is ManySortedFunction of (Image F),U2
proof
let H be ManySortedFunction of (Image F),(Image F); ::_thesis: H is ManySortedFunction of (Image F),U2
 for i being set st i in the carrier of S1 holds
H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S1 implies H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) )
assume A3: i in the carrier of S1 ; ::_thesis: H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i)
then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15;
reconsider h = H . i as Function of ( the Sorts of (Image F) . i),( the Sorts of (Image F) . i) by A3, PBOOLE:def_15;
A4: dom f = the Sorts of U1 . i by A3, FUNCT_2:def_1;
 the Sorts of (Image F) = F .:.: the Sorts of U1 by A1, MSUALG_3:def_12;
then  the Sorts of (Image F) . i = f .: ( the Sorts of U1 . i) by A3, PBOOLE:def_20
.= rng f by A4, RELAT_1:113 ;
then  h is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) by FUNCT_2:7;
hence  H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) ; ::_thesis: verum
end;
hence  H is ManySortedFunction of (Image F),U2 by PBOOLE:def_15; ::_thesis: verum
end;
then reconsider F2 = id the Sorts of (Image F) as ManySortedFunction of (Image F),U2 ;
consider F1 being ManySortedFunction of U1,(Image F) such that
A5: ( F1 = F & F1 is order-sorted ) and
A6: F1 is_epimorphism U1, Image F by A1, A2, Th15;
take  F1 ; ::_thesis: 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 )
take  F2 ; ::_thesis: ( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus  F1 is_epimorphism U1, Image F by A6; ::_thesis: ( F2 is_monomorphism Image F,U2 & F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus  F2 is_monomorphism Image F,U2 by MSUALG_3:22; ::_thesis: ( F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )
thus  ( F = F2 ** F1 & F1 is order-sorted ) by A5, MSUALG_3:4; ::_thesis: F2 is order-sorted
 Image F is order-sorted by A1, A2, Th11;
then  the Sorts of (Image F) is OrderSortedSet of S1 by OSALG_1:17;
hence  F2 is order-sorted ; ::_thesis: verum
end;

registration
let S1 be OrderSortedSign;
let U1 be OSAlgebra of S1;
cluster MSAlgebra(# the Sorts of U1, the Charact of U1 #) ->  order-sorted ;
coherence
 MSAlgebra(# the Sorts of U1, the Charact of U1 #) is order-sorted
proof
 the Sorts of U1 is OrderSortedSet of S1 by OSALG_1:17;
hence  MSAlgebra(# the Sorts of U1, the Charact of U1 #) is order-sorted by OSALG_1:17; ::_thesis: verum
end;
end;

theorem :: OSALG_3:17
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 )
proof
let S1 be OrderSortedSign; ::_thesis: for U1 being OSAlgebra of S1 holds
( U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )
let U1 be OSAlgebra of S1; ::_thesis: ( U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )
set U2 = MSAlgebra(# the Sorts of U1, the Charact of U1 #);
A1: now__::_thesis:_for_o1_being_OperSymbol_of_S1_holds_
(_Den_(o1,U1)_=_Den_(o1,MSAlgebra(#_the_Sorts_of_U1,_the_Charact_of_U1_#))_&_Args_(o1,U1)_=_Args_(o1,MSAlgebra(#_the_Sorts_of_U1,_the_Charact_of_U1_#))_)
let o1 be OperSymbol of S1; ::_thesis: ( Den (o1,U1) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) & Args (o1,U1) = Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) )
thus  Den (o1,U1) = the Charact of MSAlgebra(# the Sorts of U1, the Charact of U1 #) . o1 by MSUALG_1:def_6
.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by MSUALG_1:def_6 ; ::_thesis: Args (o1,U1) = Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))
thus  Args (o1,U1) = (( the Sorts of MSAlgebra(# the Sorts of U1, the Charact of U1 #) #) * the Arity of S1) . o1 by MSUALG_1:def_4
.= Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by MSUALG_1:def_4 ; ::_thesis: verum
end;
thus  ( U1 is monotone implies MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone ) ::_thesis: ( MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone implies U1 is monotone )
proof
assume A2: U1 is monotone ; ::_thesis: MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone
let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def_21 ::_thesis: ( not o1 <= o2 or (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) )
assume  o1 <= o2 ; ::_thesis: (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))
then A3: (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) by A2, OSALG_1:def_21;
thus (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = (Den (o2,U1)) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) by A1
.= Den (o1,U1) by A1, A3
.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by A1 ; ::_thesis: verum
end;
assume A4: MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone ; ::_thesis: U1 is monotone
let o1, o2 be OperSymbol of S1; :: according to OSALG_1:def_21 ::_thesis: ( not o1 <= o2 or (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1) )
assume  o1 <= o2 ; ::_thesis: (Den (o2,U1)) | (Args (o1,U1)) = Den (o1,U1)
then A5: (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) = Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by A4, OSALG_1:def_21;
thus (Den (o2,U1)) | (Args (o1,U1)) = (Den (o2,MSAlgebra(# the Sorts of U1, the Charact of U1 #))) | (Args (o1,U1)) by A1
.= Den (o1,MSAlgebra(# the Sorts of U1, the Charact of U1 #)) by A1, A5
.= Den (o1,U1) by A1 ; ::_thesis: verum
end;

theorem :: OSALG_3:18
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 )
proof
let S1 be OrderSortedSign; ::_thesis: for U1, U2 being strict non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds
( U1 is monotone iff U2 is monotone )
let U1, U2 be strict non-empty OSAlgebra of S1; ::_thesis: ( U1,U2 are_os_isomorphic implies ( U1 is monotone iff U2 is monotone ) )
assume  U1,U2 are_os_isomorphic ; ::_thesis: ( U1 is monotone iff U2 is monotone )
then consider F being ManySortedFunction of U1,U2 such that
A1: F is_isomorphism U1,U2 and
A2: F is order-sorted by Def2;
reconsider O1 = the Sorts of U1, O2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1:17;
reconsider F1 = F as ManySortedFunction of O1,O2 ;
 ( F is "onto" & F is "1-1" ) by A1, MSUALG_3:13;
then A3: F1 "" is order-sorted by A2, Th6;
A4: F is_epimorphism U1,U2 by A1, MSUALG_3:def_10;
then A5: F is_homomorphism U1,U2 by MSUALG_3:def_8;
then  Image F = U2 by A4, MSUALG_3:19;
hence  ( U1 is monotone implies U2 is monotone ) by A2, A5, Th13; ::_thesis: ( U2 is monotone implies U1 is monotone )
reconsider F2 = F1 "" as ManySortedFunction of U2,U1 ;
assume A6: U2 is monotone ; ::_thesis: U1 is monotone
 F "" is_isomorphism U2,U1 by A1, MSUALG_3:14;
then A7: F2 is_epimorphism U2,U1 by MSUALG_3:def_10;
then A8: F2 is_homomorphism U2,U1 by MSUALG_3:def_8;
then  Image F2 = U1 by A7, MSUALG_3:19;
hence  U1 is monotone by A3, A8, A6, Th13; ::_thesis: verum
end;