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