:: MSUALG_3 semantic presentation begin definition let I be non empty set ; let A, B be ManySortedSet of I; let F be ManySortedFunction of A,B; let i be Element of I; :: original: . redefine funcF . i -> Function of (A . i),(B . i); coherence F . i is Function of (A . i),(B . i) by PBOOLE:def_15; end; definition let S be non empty ManySortedSign ; let U1, U2 be MSAlgebra over S; mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1, the Sorts of U2; end; definition let I be set ; let A be ManySortedSet of I; func id A -> ManySortedFunction of A,A means :Def1: :: MSUALG_3:def 1 for i being set st i in I holds it . i = id (A . i); existence ex b1 being ManySortedFunction of A,A st for i being set st i in I holds b1 . i = id (A . i) proof deffunc H1( set ) -> Element of K19(K20((A . \$1),(A . \$1))) = id (A . \$1); consider f being Function such that A1: ( dom f = I & ( for i being set st i in I holds f . i = H1(i) ) ) from FUNCT_1:sch_3(); reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom f holds f . x is Function proof let x be set ; ::_thesis: ( x in dom f implies f . x is Function ) assume x in dom f ; ::_thesis: f . x is Function then f . x = id (A . x) by A1; hence f . x is Function ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of I by FUNCOP_1:def_6; for i being set st i in I holds f . i is Function of (A . i),(A . i) proof let i be set ; ::_thesis: ( i in I implies f . i is Function of (A . i),(A . i) ) assume i in I ; ::_thesis: f . i is Function of (A . i),(A . i) then f . i = id (A . i) by A1; hence f . i is Function of (A . i),(A . i) ; ::_thesis: verum end; then reconsider f = f as ManySortedFunction of A,A by PBOOLE:def_15; take f ; ::_thesis: for i being set st i in I holds f . i = id (A . i) thus for i being set st i in I holds f . i = id (A . i) by A1; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of A,A st ( for i being set st i in I holds b1 . i = id (A . i) ) & ( for i being set st i in I holds b2 . i = id (A . i) ) holds b1 = b2 proof let F, G be ManySortedFunction of A,A; ::_thesis: ( ( for i being set st i in I holds F . i = id (A . i) ) & ( for i being set st i in I holds G . i = id (A . i) ) implies F = G ) assume that A2: for i being set st i in I holds F . i = id (A . i) and A3: for i being set st i in I holds G . i = id (A . i) ; ::_thesis: F = G A4: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ F_._i_=_G_._i let i be set ; ::_thesis: ( i in I implies F . i = G . i ) assume A5: i in I ; ::_thesis: F . i = G . i then F . i = id (A . i) by A2; hence F . i = G . i by A3, A5; ::_thesis: verum end; ( dom F = I & dom G = I ) by PARTFUN1:def_2; hence F = G by A4, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines id MSUALG_3:def_1_:_ for I being set for A being ManySortedSet of I for b3 being ManySortedFunction of A,A holds ( b3 = id A iff for i being set st i in I holds b3 . i = id (A . i) ); definition let IT be Function; attrIT is "1-1" means :Def2: :: MSUALG_3:def 2 for i being set for f being Function st i in dom IT & IT . i = f holds f is one-to-one ; end; :: deftheorem Def2 defines "1-1" MSUALG_3:def_2_:_ for IT being Function holds ( IT is "1-1" iff for i being set for f being Function st i in dom IT & IT . i = f holds f is one-to-one ); registration let I be set ; cluster Relation-like I -defined Function-like total V41() V42() "1-1" for set ; existence ex b1 being ManySortedFunction of I st b1 is "1-1" proof set A = the ManySortedSet of I; take F = id the ManySortedSet of I; ::_thesis: F is "1-1" let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for f being Function st i in dom F & F . i = f holds f is one-to-one let f be Function; ::_thesis: ( i in dom F & F . i = f implies f is one-to-one ) A1: dom (id the ManySortedSet of I) = I by PARTFUN1:def_2; assume ( i in dom F & F . i = f ) ; ::_thesis: f is one-to-one then f = id ( the ManySortedSet of I . i) by A1, Def1; hence f is one-to-one ; ::_thesis: verum end; end; theorem Th1: :: MSUALG_3:1 for I being set for F being ManySortedFunction of I holds ( F is "1-1" iff for i being set st i in I holds F . i is one-to-one ) proof let I be set ; ::_thesis: for F being ManySortedFunction of I holds ( F is "1-1" iff for i being set st i in I holds F . i is one-to-one ) let F be ManySortedFunction of I; ::_thesis: ( F is "1-1" iff for i being set st i in I holds F . i is one-to-one ) A1: dom F = I by PARTFUN1:def_2; hence ( F is "1-1" implies for i being set st i in I holds F . i is one-to-one ) by Def2; ::_thesis: ( ( for i being set st i in I holds F . i is one-to-one ) implies F is "1-1" ) assume for i being set st i in I holds F . i is one-to-one ; ::_thesis: F is "1-1" then for i being set for f being Function st i in dom F & f = F . i holds f is one-to-one by A1; hence F is "1-1" by Def2; ::_thesis: verum end; definition let I be set ; let A, B be ManySortedSet of I; let IT be ManySortedFunction of A,B; attrIT is "onto" means :Def3: :: MSUALG_3:def 3 for i being set st i in I holds rng (IT . i) = B . i; end; :: deftheorem Def3 defines "onto" MSUALG_3:def_3_:_ for I being set for A, B being ManySortedSet of I for IT being ManySortedFunction of A,B holds ( IT is "onto" iff for i being set st i in I holds rng (IT . i) = B . i ); theorem Th2: :: MSUALG_3:2 for I being set for A, B, C being ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds ( dom (G ** F) = I & ( for i being set st i in I holds (G ** F) . i = (G . i) * (F . i) ) ) proof let I be set ; ::_thesis: for A, B, C being ManySortedSet of I for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds ( dom (G ** F) = I & ( for i being set st i in I holds (G ** F) . i = (G . i) * (F . i) ) ) let A, B, C be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B for G being ManySortedFunction of B,C holds ( dom (G ** F) = I & ( for i being set st i in I holds (G ** F) . i = (G . i) * (F . i) ) ) let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C holds ( dom (G ** F) = I & ( for i being set st i in I holds (G ** F) . i = (G . i) * (F . i) ) ) let G be ManySortedFunction of B,C; ::_thesis: ( dom (G ** F) = I & ( for i being set st i in I holds (G ** F) . i = (G . i) * (F . i) ) ) ( dom F = I & dom G = I ) by PARTFUN1:def_2; then (dom F) /\ (dom G) = I ; hence A1: dom (G ** F) = I by PBOOLE:def_19; ::_thesis: for i being set st i in I holds (G ** F) . i = (G . i) * (F . i) let i be set ; ::_thesis: ( i in I implies (G ** F) . i = (G . i) * (F . i) ) thus ( i in I implies (G ** F) . i = (G . i) * (F . i) ) by A1, PBOOLE:def_19; ::_thesis: verum end; definition let I be set ; let A be ManySortedSet of I; let B, C be V2() ManySortedSet of I; let F be ManySortedFunction of A,B; let G be ManySortedFunction of B,C; :: original: ** redefine funcG ** F -> ManySortedFunction of A,C; coherence G ** F is ManySortedFunction of A,C proof dom (G ** F) = I by Th2; then reconsider fg = G ** F as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; reconsider fg = fg as ManySortedFunction of I ; for i being set st i in I holds fg . i is Function of (A . i),(C . i) proof let i be set ; ::_thesis: ( i in I implies fg . i is Function of (A . i),(C . i) ) assume A1: i in I ; ::_thesis: fg . i is Function of (A . i),(C . i) then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider g = G . i as Function of (B . i),(C . i) by A1, PBOOLE:def_15; (G ** F) . i = g * f by A1, Th2; hence fg . i is Function of (A . i),(C . i) by A1; ::_thesis: verum end; hence G ** F is ManySortedFunction of A,C by PBOOLE:def_15; ::_thesis: verum end; end; theorem :: MSUALG_3:3 for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B holds F ** (id A) = F proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for F being ManySortedFunction of A,B holds F ** (id A) = F let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds F ** (id A) = F let F be ManySortedFunction of A,B; ::_thesis: F ** (id A) = F dom (F ** (id A)) = (dom F) /\ (dom (id A)) by PBOOLE:def_19 .= I /\ (dom (id A)) by PARTFUN1:def_2 .= I /\ I by PARTFUN1:def_2 .= I ; then reconsider G = F ** (id A) as ManySortedFunction of I by PARTFUN1:def_2, RELAT_1:def_18; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ G_._i_=_F_._i let i be set ; ::_thesis: ( i in I implies G . b1 = F . b1 ) assume A1: i in I ; ::_thesis: G . b1 = F . b1 then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider g = (id A) . i as Function of (A . i),(A . i) by A1, PBOOLE:def_15; A2: G . i = f * g by A1, Th2 .= f * (id (A . i)) by A1, Def1 ; percases not ( B . i = {} & not A . i = {} & not ( B . i = {} & A . i <> {} ) ) ; suppose ( B . i = {} implies A . i = {} ) ; ::_thesis: G . b1 = F . b1 then dom f = A . i by FUNCT_2:def_1; hence G . i = F . i by A2, RELAT_1:52; ::_thesis: verum end; suppose ( B . i = {} & A . i <> {} ) ; ::_thesis: G . b1 = F . b1 then f = {} ; hence G . i = F . i by A2; ::_thesis: verum end; end; end; hence F ** (id A) = F by PBOOLE:3; ::_thesis: verum end; theorem Th4: :: MSUALG_3:4 for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B holds (id B) ** F = F proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for F being ManySortedFunction of A,B holds (id B) ** F = F let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds (id B) ** F = F let F be ManySortedFunction of A,B; ::_thesis: (id B) ** F = F dom ((id B) ** F) = (dom (id B)) /\ (dom F) by PBOOLE:def_19 .= I /\ (dom F) by PARTFUN1:def_2 .= I /\ I by PARTFUN1:def_2 .= I ; then reconsider G = (id B) ** F as ManySortedFunction of I by PARTFUN1:def_2, RELAT_1:def_18; now__::_thesis:_for_i_being_set_st_i_in_I_holds_ G_._i_=_F_._i let i be set ; ::_thesis: ( i in I implies G . i = F . i ) assume A1: i in I ; ::_thesis: G . i = F . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider g = (id B) . i as Function of (B . i),(B . i) by A1, PBOOLE:def_15; ( g = id (B . i) & G . i = g * f ) by A1, Def1, Th2; hence G . i = F . i by FUNCT_2:17; ::_thesis: verum end; hence (id B) ** F = F by PBOOLE:3; ::_thesis: verum end; definition let I be set ; let A, B be ManySortedSet of I; let F be ManySortedFunction of A,B; assume that A1: F is "1-1" and A2: F is "onto" ; funcF "" -> ManySortedFunction of B,A means :Def4: :: MSUALG_3:def 4 for i being set st i in I holds it . i = (F . i) " ; existence ex b1 being ManySortedFunction of B,A st for i being set st i in I holds b1 . i = (F . i) " proof defpred S1[ set , set ] means \$2 = (F . \$1) " ; A3: for i being set st i in I holds ex u being set st S1[i,u] ; consider H being Function such that A4: ( dom H = I & ( for i being set st i in I holds S1[i,H . i] ) ) from CLASSES1:sch_1(A3); reconsider H = H as ManySortedSet of I by A4, PARTFUN1:def_2, RELAT_1:def_18; for x being set st x in dom H holds H . x is Function proof let x be set ; ::_thesis: ( x in dom H implies H . x is Function ) assume A5: x in dom H ; ::_thesis: H . x is Function then x in I by PARTFUN1:def_2; then reconsider f = F . x as Function of (A . x),(B . x) by PBOOLE:def_15; H . x = f " by A4, A5; hence H . x is Function ; ::_thesis: verum end; then reconsider H = H as ManySortedFunction of I by FUNCOP_1:def_6; for i being set st i in I holds H . i is Function of (B . i),(A . i) proof let i be set ; ::_thesis: ( i in I implies H . i is Function of (B . i),(A . i) ) assume A6: i in I ; ::_thesis: H . i is Function of (B . i),(A . i) then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; i in dom F by A6, PARTFUN1:def_2; then A7: f is one-to-one by A1, Def2; rng f = B . i by A2, A6, Def3; then f " is Function of (B . i),(A . i) by A7, FUNCT_2:25; hence H . i is Function of (B . i),(A . i) by A4, A6; ::_thesis: verum end; then reconsider H = H as ManySortedFunction of B,A by PBOOLE:def_15; take H ; ::_thesis: for i being set st i in I holds H . i = (F . i) " thus for i being set st i in I holds H . i = (F . i) " by A4; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of B,A st ( for i being set st i in I holds b1 . i = (F . i) " ) & ( for i being set st i in I holds b2 . i = (F . i) " ) holds b1 = b2 proof let H1, H2 be ManySortedFunction of B,A; ::_thesis: ( ( for i being set st i in I holds H1 . i = (F . i) " ) & ( for i being set st i in I holds H2 . i = (F . i) " ) implies H1 = H2 ) assume that A8: for i being set st i in I holds H1 . i = (F . i) " and A9: for i being set st i in I holds H2 . i = (F . i) " ; ::_thesis: H1 = H2 now__::_thesis:_for_i_being_set_st_i_in_I_holds_ H1_._i_=_H2_._i let i be set ; ::_thesis: ( i in I implies H1 . i = H2 . i ) assume A10: i in I ; ::_thesis: H1 . i = H2 . i then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; H1 . i = f " by A8, A10; hence H1 . i = H2 . i by A9, A10; ::_thesis: verum end; hence H1 = H2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def4 defines "" MSUALG_3:def_4_:_ for I being set for A, B being ManySortedSet of I for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds for b5 being ManySortedFunction of B,A holds ( b5 = F "" iff for i being set st i in I holds b5 . i = (F . i) " ); theorem Th5: :: MSUALG_3:5 for I being set for A, B being V2() ManySortedSet of I for H being ManySortedFunction of A,B for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) proof let I be set ; ::_thesis: for A, B being V2() ManySortedSet of I for H being ManySortedFunction of A,B for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) let A, B be V2() ManySortedSet of I; ::_thesis: for H being ManySortedFunction of A,B for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) let H be ManySortedFunction of A,B; ::_thesis: for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds ( H ** H1 = id B & H1 ** H = id A ) let H1 be ManySortedFunction of B,A; ::_thesis: ( H is "1-1" & H is "onto" & H1 = H "" implies ( H ** H1 = id B & H1 ** H = id A ) ) assume that A1: ( H is "1-1" & H is "onto" ) and A2: H1 = H "" ; ::_thesis: ( H ** H1 = id B & H1 ** H = id A ) A3: now__::_thesis:_for_i_being_set_st_i_in_I_holds_ (H_**_H1)_._i_=_id_(B_._i) let i be set ; ::_thesis: ( i in I implies (H ** H1) . i = id (B . i) ) assume A4: i in I ; ::_thesis: (H ** H1) . i = id (B . i) then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider h1 = H1 . i as Function of (B . i),(A . i) by A4, PBOOLE:def_15; i in dom H by A4, PARTFUN1:def_2; then A5: h is one-to-one by A1, Def2; h1 = h " by A1, A2, A4, Def4; then h * h1 = id (rng h) by A5, FUNCT_1:39; then h * h1 = id (B . i) by A1, A4, Def3; hence (H ** H1) . i = id (B . i) by A4, Th2; ::_thesis: verum end; for i being set st i in I holds (H1 ** H) . i = id (A . i) proof let i be set ; ::_thesis: ( i in I implies (H1 ** H) . i = id (A . i) ) assume A6: i in I ; ::_thesis: (H1 ** H) . i = id (A . i) then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def_15; reconsider h1 = H1 . i as Function of (B . i),(A . i) by A6, PBOOLE:def_15; i in dom H by A6, PARTFUN1:def_2; then A7: h is one-to-one by A1, Def2; ( h1 = h " & dom h = A . i ) by A1, A2, A6, Def4, FUNCT_2:def_1; then h1 * h = id (A . i) by A7, FUNCT_1:39; hence (H1 ** H) . i = id (A . i) by A6, Th2; ::_thesis: verum end; hence ( H ** H1 = id B & H1 ** H = id A ) by A3, Def1; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let U1 be non-empty MSAlgebra over S; let o be OperSymbol of S; cluster Args (o,U1) -> functional ; coherence Args (o,U1) is functional proof Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; hence Args (o,U1) is functional ; ::_thesis: verum end; end; begin theorem Th6: :: MSUALG_3:6 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1 being MSAlgebra over S for x being Function st x in Args (o,U1) holds ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U1 being MSAlgebra over S for x being Function st x in Args (o,U1) holds ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) let o be OperSymbol of S; ::_thesis: for U1 being MSAlgebra over S for x being Function st x in Args (o,U1) holds ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) let U1 be MSAlgebra over S; ::_thesis: for x being Function st x in Args (o,U1) holds ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) let x be Function; ::_thesis: ( x in Args (o,U1) implies ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) ) A1: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2; then A2: rng (the_arity_of o) c= dom the Sorts of U1 by FINSEQ_1:def_4; assume A3: x in Args (o,U1) ; ::_thesis: ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) then dom x = dom ( the Sorts of U1 * (the_arity_of o)) by A1, CARD_3:9; hence ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) by A3, A1, A2, CARD_3:9, RELAT_1:27; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let o be OperSymbol of S; let F be ManySortedFunction of U1,U2; let x be Element of Args (o,U1); assume that A1: Args (o,U1) <> {} and A2: Args (o,U2) <> {} ; funcF # x -> Element of Args (o,U2) equals :Def5: :: MSUALG_3:def 5 (Frege (F * (the_arity_of o))) . x; coherence (Frege (F * (the_arity_of o))) . x is Element of Args (o,U2) proof A3: dom ( the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) c= dom ( the Sorts of U1 * (the_arity_of o)) let e be set ; ::_thesis: ( e in dom ( the Sorts of U1 * (the_arity_of o)) implies e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ) A4: (F * (the_arity_of o)) . e is Function ; assume A5: e in dom ( the Sorts of U1 * (the_arity_of o)) ; ::_thesis: e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) then (the_arity_of o) . e in dom the Sorts of U1 by FUNCT_1:11; then (the_arity_of o) . e in the carrier of S by PARTFUN1:def_2; then A6: (the_arity_of o) . e in dom F by PARTFUN1:def_2; e in dom (the_arity_of o) by A5, FUNCT_1:11; then e in dom (F * (the_arity_of o)) by A6, FUNCT_1:11; hence e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A4, FUNCT_6:19; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) or e in dom ( the Sorts of U1 * (the_arity_of o)) ) assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; ::_thesis: e in dom ( the Sorts of U1 * (the_arity_of o)) then e in dom (F * (the_arity_of o)) by FUNCT_6:19; then A7: e in dom (the_arity_of o) by FUNCT_1:11; then reconsider f = e as Element of NAT ; (the_arity_of o) . f in the carrier of S by A7, FINSEQ_2:11; then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def_2; hence e in dom ( the Sorts of U1 * (the_arity_of o)) by A7, FUNCT_1:11; ::_thesis: verum end; now__::_thesis:_for_e_being_set_st_e_in_(F_*_(the_arity_of_o))_"_(SubFuncs_(rng_(F_*_(the_arity_of_o))))_holds_ (_the_Sorts_of_U1_*_(the_arity_of_o))_._e_=_proj1_((F_*_(the_arity_of_o))_._e) let e be set ; ::_thesis: ( e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) implies ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) ) A8: product ( the Sorts of U2 * (the_arity_of o)) <> {} by A2, PRALG_2:3; assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; ::_thesis: ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) then e in dom (F * (the_arity_of o)) by FUNCT_6:19; then A9: e in dom (the_arity_of o) by FUNCT_1:11; then reconsider f = e as Element of NAT ; (the_arity_of o) . f in the carrier of S by A9, FINSEQ_2:11; then (the_arity_of o) . e in dom the Sorts of U2 by PARTFUN1:def_2; then A10: e in dom ( the Sorts of U2 * (the_arity_of o)) by A9, FUNCT_1:11; A11: ( the Sorts of U2 * (the_arity_of o)) . e = the Sorts of U2 . ((the_arity_of o) . e) by A9, FUNCT_1:13; A12: now__::_thesis:_not_the_Sorts_of_U2_._((the_arity_of_o)_._e)_=_{} assume the Sorts of U2 . ((the_arity_of o) . e) = {} ; ::_thesis: contradiction then {} in rng ( the Sorts of U2 * (the_arity_of o)) by A10, A11, FUNCT_1:def_3; hence contradiction by A8, CARD_3:26; ::_thesis: verum end; reconsider Foe = F . ((the_arity_of o) . e) as Function of ( the Sorts of U1 . ((the_arity_of o) . e)),( the Sorts of U2 . ((the_arity_of o) . e)) by A9, FINSEQ_2:11, PBOOLE:def_15; thus ( the Sorts of U1 * (the_arity_of o)) . e = the Sorts of U1 . ((the_arity_of o) . e) by A9, FUNCT_1:13 .= dom Foe by A12, FUNCT_2:def_1 .= proj1 Foe .= proj1 ((F * (the_arity_of o)) . e) by A9, FUNCT_1:13 ; ::_thesis: verum end; then A13: the Sorts of U1 * (the_arity_of o) = doms (F * (the_arity_of o)) by A3, FUNCT_6:def_2; x in Args (o,U1) by A1; then A14: x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; then consider f being Function such that A15: x = f and dom f = dom (doms (F * (the_arity_of o))) and A16: for e being set st e in dom (doms (F * (the_arity_of o))) holds f . e in (doms (F * (the_arity_of o))) . e by A13, CARD_3:def_5; A17: dom ((F * (the_arity_of o)) .. f) = dom (F * (the_arity_of o)) by PRALG_1:def_17; A18: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4; then A19: rng (the_arity_of o) c= dom the Sorts of U2 by PARTFUN1:def_2; rng (the_arity_of o) c= dom F by A18, PARTFUN1:def_2; then A20: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27 .= dom ( the Sorts of U2 * (the_arity_of o)) by A19, RELAT_1:27 ; A21: now__::_thesis:_for_e_being_set_st_e_in_dom_(_the_Sorts_of_U2_*_(the_arity_of_o))_holds_ ((F_*_(the_arity_of_o))_.._f)_._e_in_(_the_Sorts_of_U2_*_(the_arity_of_o))_._e let e be set ; ::_thesis: ( e in dom ( the Sorts of U2 * (the_arity_of o)) implies ((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e ) A22: product ( the Sorts of U2 * (the_arity_of o)) <> {} by A2, PRALG_2:3; assume A23: e in dom ( the Sorts of U2 * (the_arity_of o)) ; ::_thesis: ((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e then A24: e in dom (the_arity_of o) by FUNCT_1:11; then reconsider g = F . ((the_arity_of o) . e) as Function of ( the Sorts of U1 . ((the_arity_of o) . e)),( the Sorts of U2 . ((the_arity_of o) . e)) by FINSEQ_2:11, PBOOLE:def_15; reconsider r = e as Element of NAT by A24; g = (F * (the_arity_of o)) . e by A20, A23, FUNCT_1:12; then A25: ((F * (the_arity_of o)) .. f) . e = g . (f . e) by A20, A23, PRALG_1:def_17; A26: ( the Sorts of U2 * (the_arity_of o)) . e = the Sorts of U2 . ((the_arity_of o) . e) by A24, FUNCT_1:13; A27: now__::_thesis:_not_the_Sorts_of_U2_._((the_arity_of_o)_._e)_=_{} assume the Sorts of U2 . ((the_arity_of o) . e) = {} ; ::_thesis: contradiction then {} in rng ( the Sorts of U2 * (the_arity_of o)) by A23, A26, FUNCT_1:def_3; hence contradiction by A22, CARD_3:26; ::_thesis: verum end; (the_arity_of o) . r in the carrier of S by A24, FINSEQ_2:11; then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def_2; then e in dom ( the Sorts of U1 * (the_arity_of o)) by A24, FUNCT_1:11; then f . e in (doms (F * (the_arity_of o))) . e by A13, A16; then f . e in the Sorts of U1 . ((the_arity_of o) . e) by A13, A24, FUNCT_1:13; then g . (f . e) in the Sorts of U2 . ((the_arity_of o) . e) by A27, FUNCT_2:5; hence ((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e by A23, A25, FUNCT_1:12; ::_thesis: verum end; (Frege (F * (the_arity_of o))) . x = (F * (the_arity_of o)) .. f by A14, A13, A15, PRALG_2:def_2; then (Frege (F * (the_arity_of o))) . x in product ( the Sorts of U2 * (the_arity_of o)) by A17, A20, A21, CARD_3:9; hence (Frege (F * (the_arity_of o))) . x is Element of Args (o,U2) by PRALG_2:3; ::_thesis: verum end; correctness ; end; :: deftheorem Def5 defines # MSUALG_3:def_5_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) st Args (o,U1) <> {} & Args (o,U2) <> {} holds F # x = (Frege (F * (the_arity_of o))) . x; Lm1: now__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_ for_U1,_U2_being_MSAlgebra_over_S for_o_being_OperSymbol_of_S for_F_being_ManySortedFunction_of_U1,U2 for_x_being_Element_of_Args_(o,U1) for_f,_u_being_Function_st_x_=_f_&_x_in_Args_(o,U1)_&_u_in_Args_(o,U2)_holds_ (_(_u_=_F_#_x_implies_for_n_being_Nat_st_n_in_dom_f_holds_ u_._n_=_(F_._((the_arity_of_o)_/._n))_._(f_._n)_)_&_(_(_for_n_being_Nat_st_n_in_dom_f_holds_ u_._n_=_(F_._((the_arity_of_o)_/._n))_._(f_._n)_)_implies_u_=_F_#_x_)_) let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being MSAlgebra over S for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let U1, U2 be MSAlgebra over S; ::_thesis: for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let o be OperSymbol of S; ::_thesis: for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let F be ManySortedFunction of U1,U2; ::_thesis: for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let x be Element of Args (o,U1); ::_thesis: for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) let f, u be Function; ::_thesis: ( x = f & x in Args (o,U1) & u in Args (o,U2) implies ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) ) assume that A1: x = f and A2: x in Args (o,U1) and A3: u in Args (o,U2) ; ::_thesis: ( ( u = F # x implies for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) A4: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4; then A5: rng (the_arity_of o) c= dom the Sorts of U1 by PARTFUN1:def_2; A6: F # x = (Frege (F * (the_arity_of o))) . x by A2, A3, Def5; A7: dom ( the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) c= dom ( the Sorts of U1 * (the_arity_of o)) let e be set ; ::_thesis: ( e in dom ( the Sorts of U1 * (the_arity_of o)) implies e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ) A8: (F * (the_arity_of o)) . e is Function ; assume A9: e in dom ( the Sorts of U1 * (the_arity_of o)) ; ::_thesis: e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) then (the_arity_of o) . e in dom the Sorts of U1 by FUNCT_1:11; then (the_arity_of o) . e in the carrier of S by PARTFUN1:def_2; then A10: (the_arity_of o) . e in dom F by PARTFUN1:def_2; e in dom (the_arity_of o) by A9, FUNCT_1:11; then e in dom (F * (the_arity_of o)) by A10, FUNCT_1:11; hence e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A8, FUNCT_6:19; ::_thesis: verum end; let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) or e in dom ( the Sorts of U1 * (the_arity_of o)) ) assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; ::_thesis: e in dom ( the Sorts of U1 * (the_arity_of o)) then e in dom (F * (the_arity_of o)) by FUNCT_6:19; then A11: e in dom (the_arity_of o) by FUNCT_1:11; then reconsider f = e as Element of NAT ; (the_arity_of o) . f in the carrier of S by A11, FINSEQ_2:11; then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def_2; hence e in dom ( the Sorts of U1 * (the_arity_of o)) by A11, FUNCT_1:11; ::_thesis: verum end; A12: Args (o,U2) = product ( the Sorts of U2 * (the_arity_of o)) by PRALG_2:3; then A13: dom u = dom ( the Sorts of U2 * (the_arity_of o)) by A3, CARD_3:9; A14: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; then A15: dom f = dom ( the Sorts of U1 * (the_arity_of o)) by A1, A2, CARD_3:9 .= dom (the_arity_of o) by A5, RELAT_1:27 ; rng (the_arity_of o) c= dom the Sorts of U2 by A4, PARTFUN1:def_2; then A16: dom u = dom (the_arity_of o) by A13, RELAT_1:27; now__::_thesis:_for_e_being_set_st_e_in_(F_*_(the_arity_of_o))_"_(SubFuncs_(rng_(F_*_(the_arity_of_o))))_holds_ (_the_Sorts_of_U1_*_(the_arity_of_o))_._e_=_proj1_((F_*_(the_arity_of_o))_._e) let e be set ; ::_thesis: ( e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) implies ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) ) assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; ::_thesis: ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) then e in dom (F * (the_arity_of o)) by FUNCT_6:19; then A17: e in dom (the_arity_of o) by FUNCT_1:11; then reconsider Foe = F . ((the_arity_of o) . e) as Function of ( the Sorts of U1 . ((the_arity_of o) . e)),( the Sorts of U2 . ((the_arity_of o) . e)) by FINSEQ_2:11, PBOOLE:def_15; ( the Sorts of U2 * (the_arity_of o)) . e in rng ( the Sorts of U2 * (the_arity_of o)) by A13, A16, A17, FUNCT_1:def_3; then A18: ( the Sorts of U2 * (the_arity_of o)) . e <> {} by A3, A12, CARD_3:26; ( ( the Sorts of U1 * (the_arity_of o)) . e = the Sorts of U1 . ((the_arity_of o) . e) & ( the Sorts of U2 * (the_arity_of o)) . e = the Sorts of U2 . ((the_arity_of o) . e) ) by A17, FUNCT_1:13; hence ( the Sorts of U1 * (the_arity_of o)) . e = dom Foe by A18, FUNCT_2:def_1 .= proj1 Foe .= proj1 ((F * (the_arity_of o)) . e) by A17, FUNCT_1:13 ; ::_thesis: verum end; then A19: the Sorts of U1 * (the_arity_of o) = doms (F * (the_arity_of o)) by A7, FUNCT_6:def_2; hereby ::_thesis: ( ( for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) assume u = F # x ; ::_thesis: for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) then A20: u = (Frege (F * (the_arity_of o))) . x by A2, A3, Def5; let n be Nat; ::_thesis: ( n in dom f implies u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) assume A21: n in dom f ; ::_thesis: u . n = (F . ((the_arity_of o) /. n)) . (f . n) then (the_arity_of o) . n in the carrier of S by A15, FINSEQ_2:11; then (the_arity_of o) . n in dom F by PARTFUN1:def_2; then A22: n in dom (F * (the_arity_of o)) by A15, A21, FUNCT_1:11; then A23: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12 .= F . ((the_arity_of o) /. n) by A15, A21, PARTFUN1:def_6 ; thus u . n = ((F * (the_arity_of o)) .. f) . n by A1, A2, A14, A19, A20, PRALG_2:def_2 .= (F . ((the_arity_of o) /. n)) . (f . n) by A22, A23, PRALG_1:def_17 ; ::_thesis: verum end; F # x is Element of product ( the Sorts of U2 * (the_arity_of o)) by PRALG_2:3; then reconsider g = F # x as Function ; A24: rng (the_arity_of o) c= dom F by A4, PARTFUN1:def_2; assume A25: for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ; ::_thesis: u = F # x A26: now__::_thesis:_for_e_being_set_st_e_in_dom_f_holds_ u_._e_=_g_._e let e be set ; ::_thesis: ( e in dom f implies u . e = g . e ) assume A27: e in dom f ; ::_thesis: u . e = g . e then reconsider n = e as Nat by A15; (the_arity_of o) . n in the carrier of S by A15, A27, FINSEQ_2:11; then (the_arity_of o) . n in dom F by PARTFUN1:def_2; then A28: n in dom (F * (the_arity_of o)) by A15, A27, FUNCT_1:11; then A29: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12 .= F . ((the_arity_of o) /. n) by A15, A27, PARTFUN1:def_6 ; thus u . e = (F . ((the_arity_of o) /. n)) . (f . n) by A25, A27 .= ((F * (the_arity_of o)) .. f) . n by A28, A29, PRALG_1:def_17 .= g . e by A1, A2, A14, A19, A6, PRALG_2:def_2 ; ::_thesis: verum end; F # x = (F * (the_arity_of o)) .. f by A1, A2, A14, A19, A6, PRALG_2:def_2; then dom g = dom (F * (the_arity_of o)) by PRALG_1:def_17 .= dom f by A15, A24, RELAT_1:27 ; hence u = F # x by A15, A16, A26, FUNCT_1:2; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; let o be OperSymbol of S; let F be ManySortedFunction of U1,U2; let x be Element of Args (o,U1); redefine func F # x means :Def6: :: MSUALG_3:def 6 for n being Nat st n in dom x holds it . n = (F . ((the_arity_of o) /. n)) . (x . n); compatibility for b1 being Element of Args (o,U2) holds ( b1 = F # x iff for n being Nat st n in dom x holds b1 . n = (F . ((the_arity_of o) /. n)) . (x . n) ) by Lm1; end; :: deftheorem Def6 defines # MSUALG_3:def_6_:_ for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for b7 being Element of Args (o,U2) holds ( b7 = F # x iff for n being Nat st n in dom x holds b7 . n = (F . ((the_arity_of o) /. n)) . (x . n) ); theorem Th7: :: MSUALG_3:7 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1 being MSAlgebra over S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U1 being MSAlgebra over S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x let o be OperSymbol of S; ::_thesis: for U1 being MSAlgebra over S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x let U1 be MSAlgebra over S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x ) set F = id the Sorts of U1; assume A1: Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x then reconsider AA = Args (o,U1) as non empty set ; let x be Element of Args (o,U1); ::_thesis: x = (id the Sorts of U1) # x reconsider Fx = (id the Sorts of U1) # x as Element of AA ; A2: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; then consider g being Function such that A3: Fx = g and dom g = dom ( the Sorts of U1 * (the_arity_of o)) and for x being set st x in dom ( the Sorts of U1 * (the_arity_of o)) holds g . x in ( the Sorts of U1 * (the_arity_of o)) . x by CARD_3:def_5; consider f being Function such that A4: x = f and dom f = dom ( the Sorts of U1 * (the_arity_of o)) and for x being set st x in dom ( the Sorts of U1 * (the_arity_of o)) holds f . x in ( the Sorts of U1 * (the_arity_of o)) . x by A1, A2, CARD_3:def_5; A5: dom f = dom (the_arity_of o) by A4, A3, Th6; A6: for y being set st y in dom f holds f . y = g . y proof let y be set ; ::_thesis: ( y in dom f implies f . y = g . y ) assume A7: y in dom f ; ::_thesis: f . y = g . y then reconsider n = y as Nat by A5; set p = (the_arity_of o) /. n; dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2; then rng (the_arity_of o) c= dom the Sorts of U1 by FINSEQ_1:def_4; then A8: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; then f . n in ( the Sorts of U1 * (the_arity_of o)) . n by A1, A4, A5, A7, Th6; then f . n in the Sorts of U1 . ((the_arity_of o) . n) by A5, A7, A8, FUNCT_1:12; then A9: f . n in the Sorts of U1 . ((the_arity_of o) /. n) by A5, A7, PARTFUN1:def_6; A10: (id the Sorts of U1) . ((the_arity_of o) /. n) = id ( the Sorts of U1 . ((the_arity_of o) /. n)) by Def1; g . n = ((id the Sorts of U1) . ((the_arity_of o) /. n)) . (f . n) by A4, A3, A7, Lm1; hence f . y = g . y by A10, A9, FUNCT_1:18; ::_thesis: verum end; dom g = dom (the_arity_of o) by A3, Th6; hence x = (id the Sorts of U1) # x by A4, A3, A6, Th6, FUNCT_1:2; ::_thesis: verum end; theorem Th8: :: MSUALG_3:8 for S being non empty non void ManySortedSign for o being OperSymbol of S for U1, U2, U3 being non-empty MSAlgebra over S for H1 being ManySortedFunction of U1,U2 for H2 being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for U1, U2, U3 being non-empty MSAlgebra over S for H1 being ManySortedFunction of U1,U2 for H2 being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x) let o be OperSymbol of S; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S for H1 being ManySortedFunction of U1,U2 for H2 being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x) let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for H1 being ManySortedFunction of U1,U2 for H2 being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x) let H1 be ManySortedFunction of U1,U2; ::_thesis: for H2 being ManySortedFunction of U2,U3 for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x) let H2 be ManySortedFunction of U2,U3; ::_thesis: for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x) let x be Element of Args (o,U1); ::_thesis: (H2 ** H1) # x = H2 # (H1 # x) A1: dom x = dom (the_arity_of o) by Th6; A2: dom (H1 # x) = dom (the_arity_of o) by Th6; A3: for y being set st y in dom (the_arity_of o) holds ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y proof rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4; then rng (the_arity_of o) c= dom the Sorts of U1 by PARTFUN1:def_2; then A4: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y ) assume A5: y in dom (the_arity_of o) ; ::_thesis: ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y then reconsider n = y as Nat ; set F = H2 ** H1; set p = (the_arity_of o) /. n; A6: ((H2 ** H1) # x) . n = ((H2 ** H1) . ((the_arity_of o) /. n)) . (x . n) by A1, A5, Def6; (the_arity_of o) /. n = (the_arity_of o) . n by A5, PARTFUN1:def_6; then A7: ( the Sorts of U1 * (the_arity_of o)) . n = the Sorts of U1 . ((the_arity_of o) /. n) by A5, A4, FUNCT_1:12; A8: (H2 ** H1) . ((the_arity_of o) /. n) = (H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n)) by Th2; A9: dom (H1 . ((the_arity_of o) /. n)) = the Sorts of U1 . ((the_arity_of o) /. n) by FUNCT_2:def_1; then dom ((H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n))) = dom (H1 . ((the_arity_of o) /. n)) by FUNCT_2:def_1; hence ((H2 ** H1) # x) . y = (H2 . ((the_arity_of o) /. n)) . ((H1 . ((the_arity_of o) /. n)) . (x . n)) by A5, A6, A4, A9, A7, A8, Th6, FUNCT_1:12 .= (H2 . ((the_arity_of o) /. n)) . ((H1 # x) . n) by A1, A5, Def6 .= (H2 # (H1 # x)) . y by A2, A5, Def6 ; ::_thesis: verum end; ( dom ((H2 ** H1) # x) = dom (the_arity_of o) & dom (H2 # (H1 # x)) = dom (the_arity_of o) ) by Th6; hence (H2 ** H1) # x = H2 # (H1 # x) by A3, FUNCT_1:2; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; predF is_homomorphism U1,U2 means :Def7: :: MSUALG_3:def 7 for o being OperSymbol of S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x); end; :: deftheorem Def7 defines is_homomorphism MSUALG_3:def_7_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_homomorphism U1,U2 iff for o being OperSymbol of S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) ); theorem Th9: :: MSUALG_3:9 for S being non empty non void ManySortedSign for U1 being MSAlgebra over S holds id the Sorts of U1 is_homomorphism U1,U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being MSAlgebra over S holds id the Sorts of U1 is_homomorphism U1,U1 let U1 be MSAlgebra over S; ::_thesis: id the Sorts of U1 is_homomorphism U1,U1 set F = id the Sorts of U1; let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) ) assume A1: Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) let x be Element of Args (o,U1); ::_thesis: ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) A2: (id the Sorts of U1) # x = x by A1, Th7; set r = the_result_sort_of o; A3: (id the Sorts of U1) . (the_result_sort_of o) = id ( the Sorts of U1 . (the_result_sort_of o)) by Def1; rng the ResultSort of S c= the carrier of S by RELAT_1:def_19; then rng the ResultSort of S c= dom the Sorts of U1 by PARTFUN1:def_2; then A4: ( Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by MSUALG_1:def_5, RELAT_1:27; o in the carrier' of S ; then o in dom the ResultSort of S by FUNCT_2:def_1; then A5: Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A4, FUNCT_1:12 .= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ; percases ( Result (o,U1) <> {} or Result (o,U1) = {} ) ; suppose Result (o,U1) <> {} ; ::_thesis: ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) then dom (Den (o,U1)) = Args (o,U1) by FUNCT_2:def_1; then ( rng (Den (o,U1)) c= Result (o,U1) & (Den (o,U1)) . x in rng (Den (o,U1)) ) by A1, FUNCT_1:def_3, RELAT_1:def_19; hence ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) by A2, A3, A5, FUNCT_1:18; ::_thesis: verum end; supposeA6: Result (o,U1) = {} ; ::_thesis: ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) then dom (Den (o,U1)) = {} ; then A7: (Den (o,U1)) . x = {} by FUNCT_1:def_2; dom ((id the Sorts of U1) . (the_result_sort_of o)) = {} by A5, A6; then ((id the Sorts of U1) . (the_result_sort_of o)) . {} = {} by FUNCT_1:def_2; hence ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) by A1, A7, Th7; ::_thesis: verum end; end; end; theorem Th10: :: MSUALG_3:10 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S for H1 being ManySortedFunction of U1,U2 for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds H2 ** H1 is_homomorphism U1,U3 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S for H1 being ManySortedFunction of U1,U2 for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds H2 ** H1 is_homomorphism U1,U3 let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for H1 being ManySortedFunction of U1,U2 for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds H2 ** H1 is_homomorphism U1,U3 let H1 be ManySortedFunction of U1,U2; ::_thesis: for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds H2 ** H1 is_homomorphism U1,U3 let H2 be ManySortedFunction of U2,U3; ::_thesis: ( H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 implies H2 ** H1 is_homomorphism U1,U3 ) assume that A1: H1 is_homomorphism U1,U2 and A2: H2 is_homomorphism U2,U3 ; ::_thesis: H2 ** H1 is_homomorphism U1,U3 let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x) ) assume Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x) let x be Element of Args (o,U1); ::_thesis: ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x) set F = H2 ** H1; set r = the_result_sort_of o; (H1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (H1 # x) by A1, Def7; then A3: (H2 . (the_result_sort_of o)) . ((H1 . (the_result_sort_of o)) . ((Den (o,U1)) . x)) = (Den (o,U3)) . (H2 # (H1 # x)) by A2, Def7; A4: ( (H2 ** H1) . (the_result_sort_of o) = (H2 . (the_result_sort_of o)) * (H1 . (the_result_sort_of o)) & dom ((H2 ** H1) . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) ) by Th2, FUNCT_2:def_1; rng the ResultSort of S c= the carrier of S by RELAT_1:def_19; then rng the ResultSort of S c= dom the Sorts of U1 by PARTFUN1:def_2; then A5: ( Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by MSUALG_1:def_5, RELAT_1:27; o in the carrier' of S ; then o in dom the ResultSort of S by FUNCT_2:def_1; then Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A5, FUNCT_1:12 .= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ; then ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (H2 # (H1 # x)) by A3, A4, FUNCT_1:12; hence ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x) by Th8; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; predF is_epimorphism U1,U2 means :Def8: :: MSUALG_3:def 8 ( F is_homomorphism U1,U2 & F is "onto" ); end; :: deftheorem Def8 defines is_epimorphism MSUALG_3:def_8_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_epimorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" ) ); theorem Th11: :: MSUALG_3:11 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds G ** F is_epimorphism U1,U3 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds G ** F is_epimorphism U1,U3 let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds G ** F is_epimorphism U1,U3 let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds G ** F is_epimorphism U1,U3 let G be ManySortedFunction of U2,U3; ::_thesis: ( F is_epimorphism U1,U2 & G is_epimorphism U2,U3 implies G ** F is_epimorphism U1,U3 ) assume that A1: F is_epimorphism U1,U2 and A2: G is_epimorphism U2,U3 ; ::_thesis: G ** F is_epimorphism U1,U3 A3: G is "onto" by A2, Def8; A4: F is "onto" by A1, Def8; for i being set st i in the carrier of S holds rng ((G ** F) . i) = the Sorts of U3 . i proof let i be set ; ::_thesis: ( i in the carrier of S implies rng ((G ** F) . i) = the Sorts of U3 . i ) assume A5: i in the carrier of S ; ::_thesis: rng ((G ** F) . i) = the Sorts of U3 . i then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15; reconsider g = G . i as Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by A5, PBOOLE:def_15; rng f = the Sorts of U2 . i by A4, A5, Def3; then A6: dom g = rng f by A5, FUNCT_2:def_1; rng g = the Sorts of U3 . i by A3, A5, Def3; then rng (g * f) = the Sorts of U3 . i by A6, RELAT_1:28; hence rng ((G ** F) . i) = the Sorts of U3 . i by A5, Th2; ::_thesis: verum end; then A7: G ** F is "onto" by Def3; ( F is_homomorphism U1,U2 & G is_homomorphism U2,U3 ) by A1, A2, Def8; then G ** F is_homomorphism U1,U3 by Th10; hence G ** F is_epimorphism U1,U3 by A7, Def8; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; predF is_monomorphism U1,U2 means :Def9: :: MSUALG_3:def 9 ( F is_homomorphism U1,U2 & F is "1-1" ); end; :: deftheorem Def9 defines is_monomorphism MSUALG_3:def_9_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_monomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "1-1" ) ); theorem Th12: :: MSUALG_3:12 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds G ** F is_monomorphism U1,U3 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds G ** F is_monomorphism U1,U3 let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds G ** F is_monomorphism U1,U3 let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds G ** F is_monomorphism U1,U3 let G be ManySortedFunction of U2,U3; ::_thesis: ( F is_monomorphism U1,U2 & G is_monomorphism U2,U3 implies G ** F is_monomorphism U1,U3 ) assume that A1: F is_monomorphism U1,U2 and A2: G is_monomorphism U2,U3 ; ::_thesis: G ** F is_monomorphism U1,U3 A3: G is "1-1" by A2, Def9; A4: F is "1-1" by A1, Def9; for i being set for h being Function st i in dom (G ** F) & (G ** F) . i = h holds h is one-to-one proof let i be set ; ::_thesis: for h being Function st i in dom (G ** F) & (G ** F) . i = h holds h is one-to-one let h be Function; ::_thesis: ( i in dom (G ** F) & (G ** F) . i = h implies h is one-to-one ) assume that A5: i in dom (G ** F) and A6: (G ** F) . i = h ; ::_thesis: h is one-to-one A7: i in the carrier of S by A5, PARTFUN1:def_2; then reconsider g = G . i as Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by PBOOLE:def_15; reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A7, PBOOLE:def_15; i in dom G by A7, PARTFUN1:def_2; then A8: g is one-to-one by A3, Def2; i in dom F by A7, PARTFUN1:def_2; then f is one-to-one by A4, Def2; then g * f is one-to-one by A8; hence h is one-to-one by A6, A7, Th2; ::_thesis: verum end; then A9: G ** F is "1-1" by Def2; ( F is_homomorphism U1,U2 & G is_homomorphism U2,U3 ) by A1, A2, Def9; then G ** F is_homomorphism U1,U3 by Th10; hence G ** F is_monomorphism U1,U3 by A9, Def9; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; let F be ManySortedFunction of U1,U2; predF is_isomorphism U1,U2 means :Def10: :: MSUALG_3:def 10 ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ); end; :: deftheorem Def10 defines is_isomorphism MSUALG_3:def_10_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_isomorphism U1,U2 iff ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) ); theorem Th13: :: MSUALG_3:13 for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being MSAlgebra over S for F being ManySortedFunction of U1,U2 holds ( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ) let U1, U2 be MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 holds ( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ) let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ) thus ( F is_isomorphism U1,U2 implies ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ) ::_thesis: ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" implies F is_isomorphism U1,U2 ) proof assume F is_isomorphism U1,U2 ; ::_thesis: ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) then ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) by Def10; hence ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) by Def8, Def9; ::_thesis: verum end; assume ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ; ::_thesis: F is_isomorphism U1,U2 then ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) by Def8, Def9; hence F is_isomorphism U1,U2 by Def10; ::_thesis: verum end; Lm2: for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds H "" is_homomorphism U2,U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds H "" is_homomorphism U2,U1 let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds H "" is_homomorphism U2,U1 let H be ManySortedFunction of U1,U2; ::_thesis: ( H is_isomorphism U1,U2 implies H "" is_homomorphism U2,U1 ) set F = H "" ; assume A1: H is_isomorphism U1,U2 ; ::_thesis: H "" is_homomorphism U2,U1 then A2: H is "onto" by Th13; A3: H is "1-1" by A1, Th13; A4: H is_homomorphism U1,U2 by A1, Th13; for o being OperSymbol of S st Args (o,U2) <> {} holds for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) proof let o be OperSymbol of S; ::_thesis: ( Args (o,U2) <> {} implies for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) ) assume Args (o,U2) <> {} ; ::_thesis: for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) let x be Element of Args (o,U2); ::_thesis: ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) set r = the_result_sort_of o; deffunc H1( set ) -> set = ((H "") # x) . \$1; consider f being Function such that A5: ( dom f = dom (the_arity_of o) & ( for n being set st n in dom (the_arity_of o) holds f . n = H1(n) ) ) from FUNCT_1:sch_3(); A6: dom ((H "") # x) = dom (the_arity_of o) by Th6; then A7: f = (H "") # x by A5, FUNCT_1:2; the_result_sort_of o in the carrier of S ; then the_result_sort_of o in dom H by PARTFUN1:def_2; then A8: H . (the_result_sort_of o) is one-to-one by A3, Def2; ( dom (H . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) & (H "") . (the_result_sort_of o) = (H . (the_result_sort_of o)) " ) by A2, A3, Def4, FUNCT_2:def_1; then A9: ((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o)) = id ( the Sorts of U1 . (the_result_sort_of o)) by A8, FUNCT_1:39; A10: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; then A11: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2; A12: Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5 .= the Sorts of U1 . ( the ResultSort of S . o) by A10, A11, FUNCT_1:12 .= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ; reconsider f = f as Element of Args (o,U1) by A5, A6, FUNCT_1:2; A13: dom (((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o))) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def_1; (H . (the_result_sort_of o)) . ((Den (o,U1)) . f) = (Den (o,U2)) . (H # ((H "") # x)) by A4, A7, Def7 .= (Den (o,U2)) . ((H ** (H "")) # x) by Th8 .= (Den (o,U2)) . ((id the Sorts of U2) # x) by A2, A3, Th5 .= (Den (o,U2)) . x by Th7 ; then ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o))) . ((Den (o,U1)) . ((H "") # x)) by A7, A13, A12, FUNCT_1:12 .= (Den (o,U1)) . ((H "") # x) by A12, A9, FUNCT_1:18 ; hence ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) ; ::_thesis: verum end; hence H "" is_homomorphism U2,U1 by Def7; ::_thesis: verum end; theorem Th14: :: MSUALG_3:14 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for H being ManySortedFunction of U1,U2 for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds H1 is_isomorphism U2,U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for H being ManySortedFunction of U1,U2 for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds H1 is_isomorphism U2,U1 let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for H being ManySortedFunction of U1,U2 for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds H1 is_isomorphism U2,U1 let H be ManySortedFunction of U1,U2; ::_thesis: for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds H1 is_isomorphism U2,U1 let H1 be ManySortedFunction of U2,U1; ::_thesis: ( H is_isomorphism U1,U2 & H1 = H "" implies H1 is_isomorphism U2,U1 ) assume that A1: H is_isomorphism U1,U2 and A2: H1 = H "" ; ::_thesis: H1 is_isomorphism U2,U1 A3: H1 is_homomorphism U2,U1 by A1, A2, Lm2; H is_monomorphism U1,U2 by A1, Def10; then A4: H is "1-1" by Def9; H is_epimorphism U1,U2 by A1, Def10; then A5: H is "onto" by Def8; for i being set for g being Function st i in dom H1 & g = H1 . i holds g is one-to-one proof let i be set ; ::_thesis: for g being Function st i in dom H1 & g = H1 . i holds g is one-to-one let g be Function; ::_thesis: ( i in dom H1 & g = H1 . i implies g is one-to-one ) assume that A6: i in dom H1 and A7: g = H1 . i ; ::_thesis: g is one-to-one A8: i in the carrier of S by A6, PARTFUN1:def_2; then reconsider f = H . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15; i in dom H by A8, PARTFUN1:def_2; then f is one-to-one by A4, Def2; then f " is one-to-one ; hence g is one-to-one by A2, A4, A5, A7, A8, Def4; ::_thesis: verum end; then H1 is "1-1" by Def2; then A9: H1 is_monomorphism U2,U1 by A3, Def9; for i being set st i in the carrier of S holds rng (H1 . i) = the Sorts of U1 . i proof let i be set ; ::_thesis: ( i in the carrier of S implies rng (H1 . i) = the Sorts of U1 . i ) assume A10: i in the carrier of S ; ::_thesis: rng (H1 . i) = the Sorts of U1 . i then reconsider f = H . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15; i in dom H by A10, PARTFUN1:def_2; then f is one-to-one by A4, Def2; then rng (f ") = dom f by FUNCT_1:33; then rng (f ") = the Sorts of U1 . i by A10, FUNCT_2:def_1; hence rng (H1 . i) = the Sorts of U1 . i by A2, A4, A5, A10, Def4; ::_thesis: verum end; then H1 is "onto" by Def3; then H1 is_epimorphism U2,U1 by A3, Def8; hence H1 is_isomorphism U2,U1 by A9, Def10; ::_thesis: verum end; theorem Th15: :: MSUALG_3:15 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S for H being ManySortedFunction of U1,U2 for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds H1 ** H is_isomorphism U1,U3 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S for H being ManySortedFunction of U1,U2 for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds H1 ** H is_isomorphism U1,U3 let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for H being ManySortedFunction of U1,U2 for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds H1 ** H is_isomorphism U1,U3 let H be ManySortedFunction of U1,U2; ::_thesis: for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds H1 ** H is_isomorphism U1,U3 let H1 be ManySortedFunction of U2,U3; ::_thesis: ( H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 implies H1 ** H is_isomorphism U1,U3 ) assume A1: ( H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 ) ; ::_thesis: H1 ** H is_isomorphism U1,U3 then ( H is_epimorphism U1,U2 & H1 is_epimorphism U2,U3 ) by Def10; then A2: H1 ** H is_epimorphism U1,U3 by Th11; ( H is_monomorphism U1,U2 & H1 is_monomorphism U2,U3 ) by A1, Def10; then H1 ** H is_monomorphism U1,U3 by Th12; hence H1 ** H is_isomorphism U1,U3 by A2, Def10; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; predU1,U2 are_isomorphic means :Def11: :: MSUALG_3:def 11 ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2; end; :: deftheorem Def11 defines are_isomorphic MSUALG_3:def_11_:_ for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S holds ( U1,U2 are_isomorphic iff ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2 ); theorem Th16: :: MSUALG_3:16 for S being non empty non void ManySortedSign for U1 being MSAlgebra over S holds ( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being MSAlgebra over S holds ( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic ) let U1 be MSAlgebra over S; ::_thesis: ( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic ) A1: id the Sorts of U1 is_homomorphism U1,U1 by Th9; for i being set for f being Function st i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f holds f is one-to-one proof let i be set ; ::_thesis: for f being Function st i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f holds f is one-to-one let f be Function; ::_thesis: ( i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f implies f is one-to-one ) assume that A2: i in dom (id the Sorts of U1) and A3: (id the Sorts of U1) . i = f ; ::_thesis: f is one-to-one i in the carrier of S by A2, PARTFUN1:def_2; then f = id ( the Sorts of U1 . i) by A3, Def1; hence f is one-to-one ; ::_thesis: verum end; then id the Sorts of U1 is "1-1" by Def2; then A4: id the Sorts of U1 is_monomorphism U1,U1 by A1, Def9; for i being set st i in the carrier of S holds rng ((id the Sorts of U1) . i) = the Sorts of U1 . i proof let i be set ; ::_thesis: ( i in the carrier of S implies rng ((id the Sorts of U1) . i) = the Sorts of U1 . i ) assume i in the carrier of S ; ::_thesis: rng ((id the Sorts of U1) . i) = the Sorts of U1 . i then (id the Sorts of U1) . i = id ( the Sorts of U1 . i) by Def1; hence rng ((id the Sorts of U1) . i) = the Sorts of U1 . i by RELAT_1:45; ::_thesis: verum end; then id the Sorts of U1 is "onto" by Def3; then A5: id the Sorts of U1 is_epimorphism U1,U1 by A1, Def8; hence id the Sorts of U1 is_isomorphism U1,U1 by A4, Def10; ::_thesis: U1,U1 are_isomorphic take id the Sorts of U1 ; :: according to MSUALG_3:def_11 ::_thesis: id the Sorts of U1 is_isomorphism U1,U1 thus id the Sorts of U1 is_isomorphism U1,U1 by A4, A5, Def10; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be MSAlgebra over S; :: original: are_isomorphic redefine predU1,U2 are_isomorphic ; reflexivity for U1 being MSAlgebra over S holds (S,b1,b1) by Th16; end; theorem :: MSUALG_3:17 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S st U1,U2 are_isomorphic holds U2,U1 are_isomorphic proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S st U1,U2 are_isomorphic holds U2,U1 are_isomorphic let U1, U2 be non-empty MSAlgebra over S; ::_thesis: ( U1,U2 are_isomorphic implies U2,U1 are_isomorphic ) assume U1,U2 are_isomorphic ; ::_thesis: U2,U1 are_isomorphic then consider F being ManySortedFunction of U1,U2 such that A1: F is_isomorphism U1,U2 by Def11; reconsider G = F "" as ManySortedFunction of U2,U1 ; G is_isomorphism U2,U1 by A1, Th14; hence U2,U1 are_isomorphic by Def11; ::_thesis: verum end; theorem :: MSUALG_3:18 for S being non empty non void ManySortedSign for U1, U2, U3 being non-empty MSAlgebra over S st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds U1,U3 are_isomorphic proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds U1,U3 are_isomorphic let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: ( U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic ) assume that A1: U1,U2 are_isomorphic and A2: U2,U3 are_isomorphic ; ::_thesis: U1,U3 are_isomorphic consider F being ManySortedFunction of U1,U2 such that A3: F is_isomorphism U1,U2 by A1, Def11; consider G being ManySortedFunction of U2,U3 such that A4: G is_isomorphism U2,U3 by A2, Def11; reconsider H = G ** F as ManySortedFunction of U1,U3 ; H is_isomorphism U1,U3 by A3, A4, Th15; hence U1,U3 are_isomorphic by Def11; ::_thesis: verum end; definition let S be non empty non void ManySortedSign ; let U1, U2 be non-empty MSAlgebra over S; let F be ManySortedFunction of U1,U2; assume A1: F is_homomorphism U1,U2 ; func Image F -> strict non-empty MSSubAlgebra of U2 means :Def12: :: MSUALG_3:def 12 the Sorts of it = F .:.: the Sorts of U1; existence ex b1 being strict non-empty MSSubAlgebra of U2 st the Sorts of b1 = F .:.: the Sorts of U1 proof set u2 = F .:.: the Sorts of U1; A2: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ not_(F_.:.:_the_Sorts_of_U1)_._i_is_empty let i be set ; ::_thesis: ( i in the carrier of S implies not (F .:.: the Sorts of U1) . i is empty ) reconsider f = F . i as Function ; assume A3: i in the carrier of S ; ::_thesis: not (F .:.: the Sorts of U1) . i is empty then A4: (F .:.: the Sorts of U1) . i = f .: ( the Sorts of U1 . i) by PBOOLE:def_20; reconsider f = f as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A3, PBOOLE:def_15; dom f = the Sorts of U1 . i by A3, FUNCT_2:def_1; hence not (F .:.: the Sorts of U1) . i is empty by A3, A4, RELAT_1:119; ::_thesis: verum end; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (F_.:.:_the_Sorts_of_U1)_._i_c=_the_Sorts_of_U2_._i let i be set ; ::_thesis: ( i in the carrier of S implies (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i ) reconsider f = F . i as Function ; assume A5: i in the carrier of S ; ::_thesis: (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i then A6: (F .:.: the Sorts of U1) . i = f .: ( the Sorts of U1 . i) by PBOOLE:def_20; reconsider f = f as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A5, PBOOLE:def_15; A7: rng f c= the Sorts of U2 . i by RELAT_1:def_19; dom f = the Sorts of U1 . i by A5, FUNCT_2:def_1; hence (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i by A6, A7, RELAT_1:113; ::_thesis: verum end; then F .:.: the Sorts of U1 c= the Sorts of U2 by PBOOLE:def_2; then reconsider u2 = F .:.: the Sorts of U1 as V2() MSSubset of U2 by A2, PBOOLE:def_13, PBOOLE:def_18; set M = GenMSAlg u2; reconsider M9 = MSAlgebra(# u2,(Opers (U2,u2)) #) as non-empty MSAlgebra over S by MSUALG_1:def_3; take GenMSAlg u2 ; ::_thesis: the Sorts of (GenMSAlg u2) = F .:.: the Sorts of U1 u2 is opers_closed proof let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: u2 is_closed_on o thus rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o :: according to MSUALG_2:def_5 ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) or x in (u2 * the ResultSort of S) . o ) set D = Den (o,U2); set X = ((u2 #) * the Arity of S) . o; set ao = the_arity_of o; set ro = the_result_sort_of o; set ut = u2 * (the_arity_of o); set S1 = the Sorts of U1; A8: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4; A9: dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then dom ((u2 #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2; then A10: ((u2 #) * the Arity of S) . o = (u2 #) . ( the Arity of S . o) by A9, FUNCT_1:12 .= (u2 #) . (the_arity_of o) by MSUALG_1:def_1 .= product (u2 * (the_arity_of o)) by FINSEQ_2:def_5 ; assume x in rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) ; ::_thesis: x in (u2 * the ResultSort of S) . o then consider a being set such that A11: a in dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) and A12: x = ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) . a by FUNCT_1:def_3; A13: x = (Den (o,U2)) . a by A11, A12, FUNCT_1:47; dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= dom (Den (o,U2)) by RELAT_1:60; then reconsider a = a as Element of Args (o,U2) by A11, FUNCT_2:def_1; defpred S1[ set , set ] means for s being SortSymbol of S st s = (the_arity_of o) . \$1 holds ( \$2 in the Sorts of U1 . s & a . \$1 = (F . s) . \$2 ); A14: dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= ((u2 #) * the Arity of S) . o by RELAT_1:58; then A15: dom a = dom (u2 * (the_arity_of o)) by A11, A10, CARD_3:9; A16: dom u2 = the carrier of S by PARTFUN1:def_2; A17: for y being set st y in dom a holds ex i being set st S1[y,i] proof let y be set ; ::_thesis: ( y in dom a implies ex i being set st S1[y,i] ) assume A18: y in dom a ; ::_thesis: ex i being set st S1[y,i] then A19: a . y in (u2 * (the_arity_of o)) . y by A11, A14, A10, A15, CARD_3:9; dom (u2 * (the_arity_of o)) = dom (the_arity_of o) by A16, A8, RELAT_1:27; then (the_arity_of o) . y in rng (the_arity_of o) by A15, A18, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8; A20: dom (F . s) = the Sorts of U1 . s by FUNCT_2:def_1; (u2 * (the_arity_of o)) . y = u2 . ((the_arity_of o) . y) by A15, A18, FUNCT_1:12 .= (F . s) .: ( the Sorts of U1 . s) by PBOOLE:def_20 .= rng (F . s) by A20, RELAT_1:113 ; then consider i being set such that A21: ( i in the Sorts of U1 . s & a . y = (F . s) . i ) by A20, A19, FUNCT_1:def_3; take i ; ::_thesis: S1[y,i] thus S1[y,i] by A21; ::_thesis: verum end; consider f being Function such that A22: ( dom f = dom a & ( for y being set st y in dom a holds S1[y,f . y] ) ) from CLASSES1:sch_1(A17); dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2; then A23: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by A8, RELAT_1:27; A24: dom f = dom (the_arity_of o) by A15, A16, A8, A22, RELAT_1:27; A25: for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds f . y in ( the Sorts of U1 * (the_arity_of o)) . y proof let y be set ; ::_thesis: ( y in dom ( the Sorts of U1 * (the_arity_of o)) implies f . y in ( the Sorts of U1 * (the_arity_of o)) . y ) assume A26: y in dom ( the Sorts of U1 * (the_arity_of o)) ; ::_thesis: f . y in ( the Sorts of U1 * (the_arity_of o)) . y then (the_arity_of o) . y in rng (the_arity_of o) by A23, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8; f . y in the Sorts of U1 . s by A22, A24, A23, A26; hence f . y in ( the Sorts of U1 * (the_arity_of o)) . y by A26, FUNCT_1:12; ::_thesis: verum end; Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3; then reconsider a1 = f as Element of Args (o,U1) by A24, A23, A25, CARD_3:9; A27: dom a1 = dom (the_arity_of o) by Th6; A28: now__::_thesis:_for_y_being_set_st_y_in_dom_(the_arity_of_o)_holds_ (F_#_a1)_._y_=_a_._y let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies (F # a1) . y = a . y ) assume A29: y in dom (the_arity_of o) ; ::_thesis: (F # a1) . y = a . y then reconsider n = y as Nat ; (the_arity_of o) . y in rng (the_arity_of o) by A29, FUNCT_1:def_3; then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8; (F # a1) . n = (F . ((the_arity_of o) /. n)) . (a1 . n) by A27, A29, Def6 .= (F . s) . (a1 . n) by A29, PARTFUN1:def_6 ; hence (F # a1) . y = a . y by A22, A27, A29; ::_thesis: verum end; ( dom (F # a1) = dom (the_arity_of o) & dom a = dom (the_arity_of o) ) by Th6; then F # a1 = a by A28, FUNCT_1:2; then A30: (F . (the_result_sort_of o)) . ((Den (o,U1)) . a1) = x by A1, A13, Def7; reconsider g = F . (the_result_sort_of o) as Function ; A31: dom (F . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def_1; A32: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; then A33: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2; Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5 .= the Sorts of U1 . ( the ResultSort of S . o) by A32, A33, FUNCT_1:12 .= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ; then (Den (o,U1)) . a1 in the Sorts of U1 . (the_result_sort_of o) ; then A34: (Den (o,U1)) . a1 in dom (F . (the_result_sort_of o)) by FUNCT_2:def_1; dom (u2 * the ResultSort of S) = dom the ResultSort of S by A32, PARTFUN1:def_2; then (u2 * the ResultSort of S) . o = u2 . ( the ResultSort of S . o) by A32, FUNCT_1:12 .= u2 . (the_result_sort_of o) by MSUALG_1:def_2 .= g .: ( the Sorts of U1 . (the_result_sort_of o)) by PBOOLE:def_20 .= rng g by A31, RELAT_1:113 ; hence x in (u2 * the ResultSort of S) . o by A30, A34, FUNCT_1:def_3; ::_thesis: verum end; end; then for B being MSSubset of U2 st B = the Sorts of M9 holds ( B is opers_closed & the Charact of M9 = Opers (U2,B) ) ; then A35: M9 is MSSubAlgebra of U2 by MSUALG_2:def_9; u2 is MSSubset of M9 by PBOOLE:def_18; then GenMSAlg u2 is MSSubAlgebra of M9 by A35, MSUALG_2:def_17; then the Sorts of (GenMSAlg u2) is MSSubset of M9 by MSUALG_2:def_9; then A36: the Sorts of (GenMSAlg u2) c= u2 by PBOOLE:def_18; u2 is MSSubset of (GenMSAlg u2) by MSUALG_2:def_17; then u2 c= the Sorts of (GenMSAlg u2) by PBOOLE:def_18; hence the Sorts of (GenMSAlg u2) = F .:.: the Sorts of U1 by A36, PBOOLE:146; ::_thesis: verum end; uniqueness for b1, b2 being strict non-empty MSSubAlgebra of U2 st the Sorts of b1 = F .:.: the Sorts of U1 & the Sorts of b2 = F .:.: the Sorts of U1 holds b1 = b2 by MSUALG_2:9; end; :: deftheorem Def12 defines Image MSUALG_3:def_12_:_ for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds for b5 being strict non-empty MSSubAlgebra of U2 holds ( b5 = Image F iff the Sorts of b5 = F .:.: the Sorts of U1 ); theorem :: MSUALG_3:19 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 implies ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) ) set FF = F .:.: the Sorts of U1; assume A1: F is_homomorphism U1,U2 ; ::_thesis: ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) thus ( F is_epimorphism U1,U2 implies Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) ::_thesis: ( Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) implies F is_epimorphism U1,U2 ) proof assume F is_epimorphism U1,U2 ; ::_thesis: Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) then A2: F is "onto" by Def8; now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ (F_.:.:_the_Sorts_of_U1)_._i_=_the_Sorts_of_U2_._i let i be set ; ::_thesis: ( i in the carrier of S implies (F .:.: the Sorts of U1) . i = the Sorts of U2 . i ) assume A3: i in the carrier of S ; ::_thesis: (F .:.: the Sorts of U1) . 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; A4: rng f = the Sorts of U2 . i by A2, A3, Def3; reconsider f = f as Function ; ( (F .:.: the Sorts of U1) . i = f .: ( the Sorts of U1 . i) & dom f = the Sorts of U1 . i ) by A3, FUNCT_2:def_1, PBOOLE:def_20; hence (F .:.: the Sorts of U1) . i = the Sorts of U2 . i by A4, RELAT_1:113; ::_thesis: verum end; then A5: F .:.: the Sorts of U1 = the Sorts of U2 by PBOOLE:3; MSAlgebra(# the Sorts of U2, the Charact of U2 #) is strict MSSubAlgebra of U2 by MSUALG_2:5; hence Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by A1, A5, Def12; ::_thesis: verum end; assume Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ; ::_thesis: F is_epimorphism U1,U2 then A6: F .:.: the Sorts of U1 = the Sorts of U2 by A1, Def12; for i being set st i in the carrier of S holds rng (F . i) = the Sorts of U2 . i proof let i be set ; ::_thesis: ( i in the carrier of S implies rng (F . i) = the Sorts of U2 . i ) assume i in the carrier of S ; ::_thesis: rng (F . i) = the Sorts of U2 . i then reconsider i = i as Element of S ; reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) ; ( f .: ( the Sorts of U1 . i) = the Sorts of U2 . i & dom f = the Sorts of U1 . i ) by A6, FUNCT_2:def_1, PBOOLE:def_20; hence rng (F . i) = the Sorts of U2 . i by RELAT_1:113; ::_thesis: verum end; then F is "onto" by Def3; hence F is_epimorphism U1,U2 by A1, Def8; ::_thesis: verum end; Lm3: for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds F is ManySortedFunction of U1,(Image F) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds F is ManySortedFunction of U1,(Image F) let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds F is ManySortedFunction of U1,(Image F) let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 implies F is ManySortedFunction of U1,(Image F) ) assume A1: F is_homomorphism U1,U2 ; ::_thesis: F is ManySortedFunction of U1,(Image F) for i being set st i in the carrier of S holds F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i) proof let i be set ; ::_thesis: ( i in the carrier of S implies F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i) ) assume A2: i in the carrier of S ; ::_thesis: F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i) then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15; A3: dom f = the Sorts of U1 . i by A2, FUNCT_2:def_1; the Sorts of (Image F) = F .:.: the Sorts of U1 by A1, Def12; then the Sorts of (Image F) . i = f .: ( the Sorts of U1 . i) by A2, PBOOLE:def_20 .= rng f by A3, RELAT_1:113 ; hence F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i) by A3, FUNCT_2:1; ::_thesis: verum end; hence F is ManySortedFunction of U1,(Image F) by PBOOLE:def_15; ::_thesis: verum end; theorem Th20: :: MSUALG_3:20 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds G is_epimorphism U1, Image F proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds G is_epimorphism U1, Image F let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds G is_epimorphism U1, Image F let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds G is_epimorphism U1, Image F let G be ManySortedFunction of U1,(Image F); ::_thesis: ( F = G & F is_homomorphism U1,U2 implies G is_epimorphism U1, Image F ) assume that A1: F = G and A2: F is_homomorphism U1,U2 ; ::_thesis: G is_epimorphism U1, Image F for o being OperSymbol of S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x) proof set IF = Image F; reconsider SIF = the Sorts of (Image F) as V2() MSSubset of U2 by MSUALG_2:def_9; reconsider G1 = G as ManySortedFunction of U1,U2 by A1; let o be OperSymbol of S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x) ) assume Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x) let x be Element of Args (o,U1); ::_thesis: (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x) set SIFo = SIF * (the_arity_of o); set Uo = the Sorts of U2 * (the_arity_of o); set ao = the_arity_of o; A3: dom (Den (o,U2)) = Args (o,U2) by FUNCT_2:def_1; A4: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4; then rng (the_arity_of o) c= dom SIF by PARTFUN1:def_2; then A5: dom (SIF * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27; rng (the_arity_of o) c= dom the Sorts of U2 by A4, PARTFUN1:def_2; then A6: dom (SIF * (the_arity_of o)) = dom ( the Sorts of U2 * (the_arity_of o)) by A5, RELAT_1:27; A7: for x being set st x in dom (SIF * (the_arity_of o)) holds (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x proof let x be set ; ::_thesis: ( x in dom (SIF * (the_arity_of o)) implies (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x ) assume A8: x in dom (SIF * (the_arity_of o)) ; ::_thesis: (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x then (the_arity_of o) . x in rng (the_arity_of o) by A5, FUNCT_1:def_3; then reconsider k = (the_arity_of o) . x as Element of S by A4; set f = F . k; A9: dom (F . k) = the Sorts of U1 . k by FUNCT_2:def_1; A10: rng (F . k) c= the Sorts of U2 . k by RELAT_1:def_19; SIF = F .:.: the Sorts of U1 by A2, Def12; then (SIF * (the_arity_of o)) . x = (F .:.: the Sorts of U1) . k by A8, FUNCT_1:12 .= (F . k) .: ( the Sorts of U1 . k) by PBOOLE:def_20 .= rng (F . k) by A9, RELAT_1:113 ; hence (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x by A6, A8, A10, FUNCT_1:12; ::_thesis: verum end; A11: dom x = dom (the_arity_of o) by Th6; A12: now__::_thesis:_for_a_being_set_st_a_in_dom_(the_arity_of_o)_holds_ (G_#_x)_._a_=_(G1_#_x)_._a let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies (G # x) . a = (G1 # x) . a ) assume A13: a in dom (the_arity_of o) ; ::_thesis: (G # x) . a = (G1 # x) . a then reconsider n = a as Nat ; (G # x) . n = (G . ((the_arity_of o) /. n)) . (x . n) by A11, A13, Def6; hence (G # x) . a = (G1 # x) . a by A11, A13, Def6; ::_thesis: verum end; ( dom (G # x) = dom (the_arity_of o) & dom (G1 # x) = dom (the_arity_of o) ) by Th6; then G # x = G1 # x by A12, FUNCT_1:2; then A14: (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (G # x) by A1, A2, Def7; SIF is opers_closed by MSUALG_2:def_9; then A15: SIF is_closed_on o by MSUALG_2:def_6; ( Args (o,(Image F)) = product (SIF * (the_arity_of o)) & Args (o,U2) = product ( the Sorts of U2 * (the_arity_of o)) ) by PRALG_2:3; then Args (o,(Image F)) c= Args (o,U2) by A6, A7, CARD_3:27; then G # x in dom (Den (o,U2)) by A3, TARSKI:def_3; then A16: ( ((SIF #) * the Arity of S) . o = Args (o,(Image F)) & G # x in (dom (Den (o,U2))) /\ (Args (o,(Image F))) ) by MSUALG_1:def_4, XBOOLE_0:def_4; the Charact of (Image F) = Opers (U2,SIF) by MSUALG_2:def_9; then Den (o,(Image F)) = (Opers (U2,SIF)) . o by MSUALG_1:def_6 .= o /. SIF by MSUALG_2:def_8 .= (Den (o,U2)) | (((SIF #) * the Arity of S) . o) by A15, MSUALG_2:def_7 ; hence (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x) by A14, A16, FUNCT_1:48; ::_thesis: verum end; then A17: G is_homomorphism U1, Image F by Def7; for i being set st i in the carrier of S holds rng (G . i) = the Sorts of (Image F) . i proof let i be set ; ::_thesis: ( i in the carrier of S implies rng (G . i) = the Sorts of (Image F) . i ) assume i in the carrier of S ; ::_thesis: rng (G . i) = the Sorts of (Image F) . i then reconsider i = i as Element of S ; set g = G . i; the Sorts of (Image F) = G .:.: the Sorts of U1 by A1, A2, Def12; then A18: the Sorts of (Image F) . i = (G . i) .: ( the Sorts of U1 . i) by PBOOLE:def_20; dom (G . i) = the Sorts of U1 . i by FUNCT_2:def_1; hence rng (G . i) = the Sorts of (Image F) . i by A18, RELAT_1:113; ::_thesis: verum end; then G is "onto" by Def3; hence G is_epimorphism U1, Image F by A17, Def8; ::_thesis: verum end; theorem :: MSUALG_3:21 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds ex G being ManySortedFunction of U1,(Image F) st ( F = G & G is_epimorphism U1, Image F ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds ex G being ManySortedFunction of U1,(Image F) st ( F = G & G is_epimorphism U1, Image F ) let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds ex G being ManySortedFunction of U1,(Image F) st ( F = G & G is_epimorphism U1, Image F ) let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 implies ex G being ManySortedFunction of U1,(Image F) st ( F = G & G is_epimorphism U1, Image F ) ) assume A1: F is_homomorphism U1,U2 ; ::_thesis: ex G being ManySortedFunction of U1,(Image F) st ( F = G & G is_epimorphism U1, Image F ) then reconsider G = F as ManySortedFunction of U1,(Image F) by Lm3; take G ; ::_thesis: ( F = G & G is_epimorphism U1, Image F ) thus ( F = G & G is_epimorphism U1, Image F ) by A1, Th20; ::_thesis: verum end; Lm4: for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for U3 being non-empty MSSubAlgebra of U2 for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds F is_homomorphism U1,U2 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for U3 being non-empty MSSubAlgebra of U2 for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds F is_homomorphism U1,U2 let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for U3 being non-empty MSSubAlgebra of U2 for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds F is_homomorphism U1,U2 let U3 be non-empty MSSubAlgebra of U2; ::_thesis: for F being ManySortedFunction of U1,U2 for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds F is_homomorphism U1,U2 let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds F is_homomorphism U1,U2 let G be ManySortedFunction of U1,U3; ::_thesis: ( F = G & G is_homomorphism U1,U3 implies F is_homomorphism U1,U2 ) assume that A1: F = G and A2: G is_homomorphism U1,U3 ; ::_thesis: F is_homomorphism U1,U2 for o being OperSymbol of S st Args (o,U1) <> {} holds for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) proof reconsider S3 = the Sorts of U3 as V2() MSSubset of U2 by MSUALG_2:def_9; let o be OperSymbol of S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) ) assume Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) let x be Element of Args (o,U1); ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) for i being set st i in the carrier of S holds G . i is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) proof reconsider S3 = the Sorts of U3 as V2() MSSubset of U2 by MSUALG_2:def_9; let i be set ; ::_thesis: ( i in the carrier of S implies G . i is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) ) assume A3: i in the carrier of S ; ::_thesis: G . i is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) then reconsider g = G . i as Function of ( the Sorts of U1 . i),( the Sorts of U3 . i) by PBOOLE:def_15; the Sorts of U3 is MSSubset of U2 by MSUALG_2:def_9; then the Sorts of U3 c= the Sorts of U2 by PBOOLE:def_18; then S3 . i c= the Sorts of U2 . i by A3, PBOOLE:def_2; then g is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A3, FUNCT_2:7; hence G . i is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) ; ::_thesis: verum end; then reconsider G1 = G as ManySortedFunction of U1,U2 by PBOOLE:def_15; S3 is opers_closed by MSUALG_2:def_9; then A4: S3 is_closed_on o by MSUALG_2:def_6; the Charact of U3 = Opers (U2,S3) by MSUALG_2:def_9; then A5: Den (o,U3) = (Opers (U2,S3)) . o by MSUALG_1:def_6 .= o /. S3 by MSUALG_2:def_8 .= (Den (o,U2)) | (((S3 #) * the Arity of S) . o) by A4, MSUALG_2:def_7 ; A6: dom x = dom (the_arity_of o) by Th6; A7: now__::_thesis:_for_a_being_set_st_a_in_dom_(the_arity_of_o)_holds_ (G_#_x)_._a_=_(G1_#_x)_._a let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies (G # x) . a = (G1 # x) . a ) assume A8: a in dom (the_arity_of o) ; ::_thesis: (G # x) . a = (G1 # x) . a then reconsider n = a as Nat ; (G # x) . n = (G . ((the_arity_of o) /. n)) . (x . n) by A6, A8, Def6; hence (G # x) . a = (G1 # x) . a by A6, A8, Def6; ::_thesis: verum end; ( dom (G # x) = dom (the_arity_of o) & dom (G1 # x) = dom (the_arity_of o) ) by Th6; then A9: G # x = G1 # x by A7, FUNCT_1:2; dom (Den (o,U2)) = Args (o,U2) by FUNCT_2:def_1; then A10: ( ((S3 #) * the Arity of S) . o = Args (o,U3) & F # x in (dom (Den (o,U2))) /\ (Args (o,U3)) ) by A1, A9, MSUALG_1:def_4, XBOOLE_0:def_4; (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (F # x) by A1, A2, A9, Def7; hence (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) by A5, A10, FUNCT_1:48; ::_thesis: verum end; hence F is_homomorphism U1,U2 by Def7; ::_thesis: verum end; theorem Th22: :: MSUALG_3:22 for S being non empty non void ManySortedSign for U1 being non-empty MSAlgebra over S for U2 being non-empty MSSubAlgebra of U1 for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds G is_monomorphism U2,U1 proof let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S for U2 being non-empty MSSubAlgebra of U1 for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds G is_monomorphism U2,U1 let U1 be non-empty MSAlgebra over S; ::_thesis: for U2 being non-empty MSSubAlgebra of U1 for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds G is_monomorphism U2,U1 let U2 be non-empty MSSubAlgebra of U1; ::_thesis: for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds G is_monomorphism U2,U1 let G be ManySortedFunction of U2,U1; ::_thesis: ( G = id the Sorts of U2 implies G is_monomorphism U2,U1 ) set F = id the Sorts of U2; assume A1: G = id the Sorts of U2 ; ::_thesis: G is_monomorphism U2,U1 for i being set st i in the carrier of S holds G . i is one-to-one proof let i be set ; ::_thesis: ( i in the carrier of S implies G . i is one-to-one ) assume A2: i in the carrier of S ; ::_thesis: G . i is one-to-one then reconsider f = (id the Sorts of U2) . i as Function of ( the Sorts of U2 . i),( the Sorts of U2 . i) by PBOOLE:def_15; f = id ( the Sorts of U2 . i) by A2, Def1; hence G . i is one-to-one by A1; ::_thesis: verum end; then A3: G is "1-1" by Th1; G is_homomorphism U2,U1 by A1, Lm4, Th9; hence G is_monomorphism U2,U1 by A3, Def9; ::_thesis: verum end; theorem :: MSUALG_3:23 for S being non empty non void ManySortedSign for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 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 ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 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 ) let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 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 ) let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 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 ) ) assume A1: F is_homomorphism U1,U2 ; ::_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 ) then reconsider F1 = F as ManySortedFunction of U1,(Image F) by Lm3; 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 S 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 S implies H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) ) assume A2: i in the carrier of S ; ::_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; A3: dom f = the Sorts of U1 . i by A2, FUNCT_2:def_1; reconsider h = H . i as Function of ( the Sorts of (Image F) . i),( the Sorts of (Image F) . i) by A2, PBOOLE:def_15; A4: rng f c= the Sorts of U2 . i by RELAT_1:def_19; the Sorts of (Image F) = F .:.: the Sorts of U1 by A1, Def12; then the Sorts of (Image F) . i = f .: ( the Sorts of U1 . i) by A2, PBOOLE:def_20 .= rng f by A3, RELAT_1:113 ; then h is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) by A4, 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 ; 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 ) take F2 ; ::_thesis: ( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 ) thus F1 is_epimorphism U1, Image F by A1, Th20; ::_thesis: ( F2 is_monomorphism Image F,U2 & F = F2 ** F1 ) thus F2 is_monomorphism Image F,U2 by Th22; ::_thesis: F = F2 ** F1 thus F = F2 ** F1 by Th4; ::_thesis: verum end; theorem :: MSUALG_3:24 for S being non empty non void ManySortedSign for U1, U2 being MSAlgebra over S for o being OperSymbol of S for F being ManySortedFunction of U1,U2 for x being Element of Args (o,U1) for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds ( u = F # x iff for n being Nat st n in dom f holds u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) by Lm1;