:: INSTALG1 semantic presentation begin theorem Th1: :: INSTALG1:1 for S being non empty non void ManySortedSign for o being OperSymbol of S for V being V16() ManySortedSet of the carrier of S for x being set holds ( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) ) proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for V being V16() ManySortedSet of the carrier of S for x being set holds ( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) ) let o be OperSymbol of S; ::_thesis: for V being V16() ManySortedSet of the carrier of S for x being set holds ( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) ) let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being set holds ( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) ) let x be set ; ::_thesis: ( x is ArgumentSeq of Sym (o,V) iff x is Element of Args (o,(FreeMSA V)) ) A1: TS (DTConMSA V) = S -Terms V by MSATERM:def_1; A2: FreeMSA V = MSAlgebra(# (FreeSort V),(FreeOper V) #) by MSAFREE:def_14; hereby ::_thesis: ( x is Element of Args (o,(FreeMSA V)) implies x is ArgumentSeq of Sym (o,V) ) assume x is ArgumentSeq of Sym (o,V) ; ::_thesis: x is Element of Args (o,(FreeMSA V)) then reconsider p = x as ArgumentSeq of Sym (o,V) ; reconsider p = p as FinSequence of TS (DTConMSA V) by MSATERM:def_1; Sym (o,V) ==> roots p by MSATERM:21; hence x is Element of Args (o,(FreeMSA V)) by A2, MSAFREE:10; ::_thesis: verum end; assume x is Element of Args (o,(FreeMSA V)) ; ::_thesis: x is ArgumentSeq of Sym (o,V) then reconsider x = x as Element of Args (o,(FreeMSA V)) ; rng x c= TS (DTConMSA V) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng x or y in TS (DTConMSA V) ) assume y in rng x ; ::_thesis: y in TS (DTConMSA V) then consider z being set such that A3: z in dom x and A4: y = x . z by FUNCT_1:def_3; reconsider z = z as Element of NAT by A3; A5: (FreeSort V) . ((the_arity_of o) /. z) = FreeSort (V,((the_arity_of o) /. z)) by MSAFREE:def_11; dom x = dom (the_arity_of o) by MSUALG_6:2; then y in (FreeSort V) . ((the_arity_of o) /. z) by A2, A3, A4, MSUALG_6:2; hence y in TS (DTConMSA V) by A5; ::_thesis: verum end; then reconsider x = x as FinSequence of TS (DTConMSA V) by FINSEQ_1:def_4; Sym (o,V) ==> roots x by A2, MSAFREE:10; hence x is ArgumentSeq of Sym (o,V) by A1, MSATERM:21; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let V be V16() ManySortedSet of the carrier of S; let o be OperSymbol of S; cluster -> DTree-yielding for Element of Args (o,(FreeMSA V)); coherence for b1 being Element of Args (o,(FreeMSA V)) holds b1 is DTree-yielding by Th1; end; theorem Th2: :: INSTALG1:2 for S being non empty non void ManySortedSign for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for o being OperSymbol of S st Args (o,A1) <> {} holds Args (o,A2) <> {} proof let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for o being OperSymbol of S st Args (o,A1) <> {} holds Args (o,A2) <> {} let A1, A2 be MSAlgebra over S; ::_thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for o being OperSymbol of S st Args (o,A1) <> {} holds Args (o,A2) <> {} ) assume A1: for i being set st i in the carrier of S & the Sorts of A2 . i = {} holds the Sorts of A1 . i = {} ; :: according to PZFMISC1:def_3 ::_thesis: for o being OperSymbol of S st Args (o,A1) <> {} holds Args (o,A2) <> {} let o be OperSymbol of S; ::_thesis: ( Args (o,A1) <> {} implies Args (o,A2) <> {} ) assume A2: Args (o,A1) <> {} ; ::_thesis: Args (o,A2) <> {} now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(the_arity_of_o)_holds_ the_Sorts_of_A2_._((the_arity_of_o)_/._i)_<>_{} let i be Element of NAT ; ::_thesis: ( i in dom (the_arity_of o) implies the Sorts of A2 . ((the_arity_of o) /. i) <> {} ) assume i in dom (the_arity_of o) ; ::_thesis: the Sorts of A2 . ((the_arity_of o) /. i) <> {} then the Sorts of A1 . ((the_arity_of o) /. i) <> {} by A2, MSUALG_6:3; hence the Sorts of A2 . ((the_arity_of o) /. i) <> {} by A1; ::_thesis: verum end; hence Args (o,A2) <> {} by MSUALG_6:3; ::_thesis: verum end; theorem Th3: :: INSTALG1:3 for S being non empty non void ManySortedSign for o being OperSymbol of S for V being V16() ManySortedSet of the carrier of S for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x proof let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S for V being V16() ManySortedSet of the carrier of S for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x let o be OperSymbol of S; ::_thesis: for V being V16() ManySortedSet of the carrier of S for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x let V be V16() ManySortedSet of the carrier of S; ::_thesis: for x being Element of Args (o,(FreeMSA V)) holds (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x let x be Element of Args (o,(FreeMSA V)); ::_thesis: (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x A1: FreeMSA V = MSAlgebra(# (FreeSort V),(FreeOper V) #) by MSAFREE:def_14; reconsider p = x as ArgumentSeq of Sym (o,V) by Th1; A2: Sym (o,V) = [o, the carrier of S] by MSAFREE:def_9; ( p is FinSequence of TS (DTConMSA V) & Sym (o,V) ==> roots p ) by MSATERM:21, MSATERM:def_1; then (DenOp (o,V)) . x = [o, the carrier of S] -tree x by A2, MSAFREE:def_12; hence (Den (o,(FreeMSA V))) . x = [o, the carrier of S] -tree x by A1, MSAFREE:def_13; ::_thesis: verum end; theorem :: INSTALG1:4 for S being non empty non void ManySortedSign for A, B being MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds for o being OperSymbol of S holds Den (o,A) = Den (o,B) ; theorem Th5: :: INSTALG1:5 for S being non empty non void ManySortedSign for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds for f being ManySortedFunction of A1,A2 for g being ManySortedFunction of B1,B2 st f = g holds for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for x being Element of Args (o,A1) for y being Element of Args (o,B1) st x = y holds f # x = g # y proof let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds for f being ManySortedFunction of A1,A2 for g being ManySortedFunction of B1,B2 st f = g holds for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for x being Element of Args (o,A1) for y being Element of Args (o,B1) st x = y holds f # x = g # y let A1, A2, B1, B2 be MSAlgebra over S; ::_thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) implies for f being ManySortedFunction of A1,A2 for g being ManySortedFunction of B1,B2 st f = g holds for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for x being Element of Args (o,A1) for y being Element of Args (o,B1) st x = y holds f # x = g # y ) assume A1: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) ) ; ::_thesis: for f being ManySortedFunction of A1,A2 for g being ManySortedFunction of B1,B2 st f = g holds for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for x being Element of Args (o,A1) for y being Element of Args (o,B1) st x = y holds f # x = g # y let f be ManySortedFunction of A1,A2; ::_thesis: for g being ManySortedFunction of B1,B2 st f = g holds for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for x being Element of Args (o,A1) for y being Element of Args (o,B1) st x = y holds f # x = g # y let g be ManySortedFunction of B1,B2; ::_thesis: ( f = g implies for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for x being Element of Args (o,A1) for y being Element of Args (o,B1) st x = y holds f # x = g # y ) assume A2: f = g ; ::_thesis: for o being OperSymbol of S st Args (o,A1) <> {} & Args (o,A2) <> {} holds for x being Element of Args (o,A1) for y being Element of Args (o,B1) st x = y holds f # x = g # y let o be OperSymbol of S; ::_thesis: ( Args (o,A1) <> {} & Args (o,A2) <> {} implies for x being Element of Args (o,A1) for y being Element of Args (o,B1) st x = y holds f # x = g # y ) assume A3: ( Args (o,A1) <> {} & Args (o,A2) <> {} ) ; ::_thesis: for x being Element of Args (o,A1) for y being Element of Args (o,B1) st x = y holds f # x = g # y let x be Element of Args (o,A1); ::_thesis: for y being Element of Args (o,B1) st x = y holds f # x = g # y let y be Element of Args (o,B1); ::_thesis: ( x = y implies f # x = g # y ) assume A4: x = y ; ::_thesis: f # x = g # y f # x = (Frege (f * (the_arity_of o))) . x by A3, MSUALG_3:def_5; hence f # x = g # y by A1, A2, A3, A4, MSUALG_3:def_5; ::_thesis: verum end; theorem :: INSTALG1:6 for S being non empty non void ManySortedSign for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) & the Sorts of A1 is_transformable_to the Sorts of A2 holds for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds ex h9 being ManySortedFunction of B1,B2 st ( h9 = h & h9 is_homomorphism B1,B2 ) proof let S be non empty non void ManySortedSign ; ::_thesis: for A1, A2, B1, B2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) & the Sorts of A1 is_transformable_to the Sorts of A2 holds for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds ex h9 being ManySortedFunction of B1,B2 st ( h9 = h & h9 is_homomorphism B1,B2 ) let A1, A2, B1, B2 be MSAlgebra over S; ::_thesis: ( MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) & MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) & the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds ex h9 being ManySortedFunction of B1,B2 st ( h9 = h & h9 is_homomorphism B1,B2 ) ) assume that A1: MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) and A2: MSAlgebra(# the Sorts of A2, the Charact of A2 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) and A3: the Sorts of A1 is_transformable_to the Sorts of A2 ; ::_thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds ex h9 being ManySortedFunction of B1,B2 st ( h9 = h & h9 is_homomorphism B1,B2 ) let h be ManySortedFunction of A1,A2; ::_thesis: ( h is_homomorphism A1,A2 implies ex h9 being ManySortedFunction of B1,B2 st ( h9 = h & h9 is_homomorphism B1,B2 ) ) assume A4: h is_homomorphism A1,A2 ; ::_thesis: ex h9 being ManySortedFunction of B1,B2 st ( h9 = h & h9 is_homomorphism B1,B2 ) reconsider h9 = h as ManySortedFunction of B1,B2 by A1, A2; take h9 ; ::_thesis: ( h9 = h & h9 is_homomorphism B1,B2 ) thus h9 = h ; ::_thesis: h9 is_homomorphism B1,B2 let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,B1) = {} or for b1 being Element of Args (o,B1) holds (h9 . (the_result_sort_of o)) . ((Den (o,B1)) . b1) = (Den (o,B2)) . (h9 # b1) ) assume A5: Args (o,B1) <> {} ; ::_thesis: for b1 being Element of Args (o,B1) holds (h9 . (the_result_sort_of o)) . ((Den (o,B1)) . b1) = (Den (o,B2)) . (h9 # b1) then A6: Args (o,B2) <> {} by A1, A2, A3, Th2; let x be Element of Args (o,B1); ::_thesis: (h9 . (the_result_sort_of o)) . ((Den (o,B1)) . x) = (Den (o,B2)) . (h9 # x) reconsider y = x as Element of Args (o,A1) by A1; thus (h9 . (the_result_sort_of o)) . ((Den (o,B1)) . x) = (h . (the_result_sort_of o)) . ((Den (o,A1)) . y) by A1 .= (Den (o,A2)) . (h # y) by A1, A4, A5, MSUALG_3:def_7 .= (Den (o,B2)) . (h9 # x) by A1, A2, A5, A6, Th5 ; ::_thesis: verum end; definition let S be ManySortedSign ; attrS is feasible means :Def1: :: INSTALG1:def 1 ( the carrier of S = {} implies the carrier' of S = {} ); end; :: deftheorem Def1 defines feasible INSTALG1:def_1_:_ for S being ManySortedSign holds ( S is feasible iff ( the carrier of S = {} implies the carrier' of S = {} ) ); theorem Th7: :: INSTALG1:7 for S being ManySortedSign holds ( S is feasible iff dom the ResultSort of S = the carrier' of S ) proof let S be ManySortedSign ; ::_thesis: ( S is feasible iff dom the ResultSort of S = the carrier' of S ) hereby ::_thesis: ( dom the ResultSort of S = the carrier' of S implies S is feasible ) assume S is feasible ; ::_thesis: dom the ResultSort of S = the carrier' of S then ( the carrier of S = {} implies the carrier' of S = {} ) by Def1; hence dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; ::_thesis: verum end; assume ( dom the ResultSort of S = the carrier' of S & the carrier of S = {} & the carrier' of S <> {} ) ; :: according to INSTALG1:def_1 ::_thesis: contradiction hence contradiction ; ::_thesis: verum end; registration cluster non empty -> feasible for ManySortedSign ; coherence for b1 being ManySortedSign st not b1 is empty holds b1 is feasible proof let S be ManySortedSign ; ::_thesis: ( not S is empty implies S is feasible ) assume ( not the carrier of S is empty & the carrier of S = {} ) ; :: according to STRUCT_0:def_1,INSTALG1:def_1 ::_thesis: the carrier' of S = {} hence the carrier' of S = {} ; ::_thesis: verum end; cluster void -> feasible for ManySortedSign ; coherence for b1 being ManySortedSign st b1 is void holds b1 is feasible proof let S be ManySortedSign ; ::_thesis: ( S is void implies S is feasible ) assume that A1: S is void and the carrier of S = {} ; :: according to INSTALG1:def_1 ::_thesis: the carrier' of S = {} thus the carrier' of S = {} by A1; ::_thesis: verum end; cluster empty feasible -> void for ManySortedSign ; coherence for b1 being ManySortedSign st b1 is empty & b1 is feasible holds b1 is void proof let S be ManySortedSign ; ::_thesis: ( S is empty & S is feasible implies S is void ) assume A2: the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( not S is feasible or S is void ) assume ( the carrier of S = {} implies the carrier' of S = {} ) ; :: according to INSTALG1:def_1 ::_thesis: S is void hence S is void by A2; ::_thesis: verum end; cluster non void feasible -> non empty for ManySortedSign ; coherence for b1 being ManySortedSign st not b1 is void & b1 is feasible holds not b1 is empty ; end; registration cluster non empty non void for ManySortedSign ; existence ex b1 being ManySortedSign st ( not b1 is void & not b1 is empty ) proof set S = the non empty non void ManySortedSign ; take the non empty non void ManySortedSign ; ::_thesis: ( not the non empty non void ManySortedSign is void & not the non empty non void ManySortedSign is empty ) thus ( not the non empty non void ManySortedSign is void & not the non empty non void ManySortedSign is empty ) ; ::_thesis: verum end; end; theorem Th8: :: INSTALG1:8 for S being feasible ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S proof let S be feasible ManySortedSign ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S percases ( S is void or not S is void ) ; suppose S is void ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S hence id the carrier of S, id the carrier' of S form_morphism_between S,S by MSALIMIT:6; ::_thesis: verum end; suppose not S is void ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S then reconsider S = S as non void feasible ManySortedSign ; not S is empty ; hence id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:28; ::_thesis: verum end; end; end; theorem Th9: :: INSTALG1:9 for S1, S2 being ManySortedSign for f, g being Function st f,g form_morphism_between S1,S2 holds ( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 ) proof let S1, S2 be ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds ( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 ) let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies ( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 ) ) assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: ( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 ) then A2: ( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by PUA2MSS1:def_12; ( dom g = the carrier' of S1 & rng g c= the carrier' of S2 ) by A1, PUA2MSS1:def_12; hence ( f is Function of the carrier of S1, the carrier of S2 & g is Function of the carrier' of S1, the carrier' of S2 ) by A2, FUNCT_2:2; ::_thesis: verum end; begin definition let S be feasible ManySortedSign ; mode Subsignature of S -> ManySortedSign means :Def2: :: INSTALG1:def 2 id the carrier of it, id the carrier' of it form_morphism_between it,S; existence ex b1 being ManySortedSign st id the carrier of b1, id the carrier' of b1 form_morphism_between b1,S proof take S ; ::_thesis: id the carrier of S, id the carrier' of S form_morphism_between S,S thus id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8; ::_thesis: verum end; end; :: deftheorem Def2 defines Subsignature INSTALG1:def_2_:_ for S being feasible ManySortedSign for b2 being ManySortedSign holds ( b2 is Subsignature of S iff id the carrier of b2, id the carrier' of b2 form_morphism_between b2,S ); theorem Th10: :: INSTALG1:10 for S being feasible ManySortedSign for T being Subsignature of S holds ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S ) proof let S be feasible ManySortedSign ; ::_thesis: for T being Subsignature of S holds ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S ) let T be Subsignature of S; ::_thesis: ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S ) set g = id the carrier' of T; id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2; then ( rng (id the carrier of T) c= the carrier of S & rng (id the carrier' of T) c= the carrier' of S ) by PUA2MSS1:def_12; hence ( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S ) ; ::_thesis: verum end; registration let S be feasible ManySortedSign ; cluster -> feasible for Subsignature of S; coherence for b1 being Subsignature of S holds b1 is feasible proof let T be Subsignature of S; ::_thesis: T is feasible set f = id the carrier of T; set g = id the carrier' of T; A1: dom (id the carrier' of T) = the carrier' of T ; id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2; then A2: (id the carrier of T) * the ResultSort of T = the ResultSort of S * (id the carrier' of T) by PUA2MSS1:def_12; assume the carrier of T = {} ; :: according to INSTALG1:def_1 ::_thesis: the carrier' of T = {} then A3: {} = the ResultSort of S * (id the carrier' of T) by A2; ( the carrier' of S = dom the ResultSort of S & rng (id the carrier' of T) = the carrier' of T ) by Th7; hence the carrier' of T = {} by A3, A1, Th10, RELAT_1:27, RELAT_1:38; ::_thesis: verum end; end; theorem Th11: :: INSTALG1:11 for S being feasible ManySortedSign for T being Subsignature of S holds ( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S ) proof let S be feasible ManySortedSign ; ::_thesis: for T being Subsignature of S holds ( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S ) let T be Subsignature of S; ::_thesis: ( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S ) set f = id the carrier of T; set g = id the carrier' of T; A1: dom the Arity of T = the carrier' of T by FUNCT_2:def_1; A2: id the carrier of T, id the carrier' of T form_morphism_between T,S by Def2; A3: now__::_thesis:_for_x_being_set_st_x_in_dom_the_Arity_of_T_holds_ the_Arity_of_T_._x_=_the_Arity_of_S_._x let x be set ; ::_thesis: ( x in dom the Arity of T implies the Arity of T . x = the Arity of S . x ) A4: rng the Arity of T c= the carrier of T * by RELAT_1:def_19; assume A5: x in dom the Arity of T ; ::_thesis: the Arity of T . x = the Arity of S . x then the Arity of T . x in rng the Arity of T by FUNCT_1:def_3; then reconsider p = the Arity of T . x as Element of the carrier of T * by A4; (id the carrier' of T) . x = x by A1, A5, FUNCT_1:17; then ( rng p c= the carrier of T & (id the carrier of T) * p = the Arity of S . x ) by A2, A1, A5, FINSEQ_1:def_4, PUA2MSS1:def_12; hence the Arity of T . x = the Arity of S . x by RELAT_1:53; ::_thesis: verum end; the ResultSort of T = (id the carrier of T) * the ResultSort of T by FUNCT_2:17 .= the ResultSort of S * (id the carrier' of T) by A2, PUA2MSS1:def_12 ; hence the ResultSort of T c= the ResultSort of S by RELAT_1:50; ::_thesis: the Arity of T c= the Arity of S dom the Arity of S = the carrier' of S by FUNCT_2:def_1; then dom the Arity of T c= dom the Arity of S by A1, Th10; hence the Arity of T c= the Arity of S by A3, GRFUNC_1:2; ::_thesis: verum end; theorem Th12: :: INSTALG1:12 for S being feasible ManySortedSign for T being Subsignature of S holds ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T ) proof let S be feasible ManySortedSign ; ::_thesis: for T being Subsignature of S holds ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T ) let T be Subsignature of S; ::_thesis: ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T ) A1: the Arity of T c= the Arity of S by Th11; ( the carrier of T = {} implies the carrier' of T = {} ) by Def1; then A2: dom the ResultSort of T = the carrier' of T by FUNCT_2:def_1; ( dom the Arity of T = the carrier' of T & the ResultSort of T c= the ResultSort of S ) by Th11, FUNCT_2:def_1; hence ( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T ) by A2, A1, GRFUNC_1:23; ::_thesis: verum end; theorem Th13: :: INSTALG1:13 for S, T being feasible ManySortedSign st the carrier of T c= the carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the ResultSort of S holds T is Subsignature of S proof let S, T be feasible ManySortedSign ; ::_thesis: ( the carrier of T c= the carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the ResultSort of S implies T is Subsignature of S ) assume that A1: the carrier of T c= the carrier of S and A2: the Arity of T c= the Arity of S and A3: the ResultSort of T c= the ResultSort of S ; ::_thesis: T is Subsignature of S set f = id the carrier of T; set g = id the carrier' of T; thus ( dom (id the carrier of T) = the carrier of T & dom (id the carrier' of T) = the carrier' of T ) ; :: according to PUA2MSS1:def_12,INSTALG1:def_2 ::_thesis: ( rng (id the carrier of T) c= the carrier of S & rng (id the carrier' of T) c= the carrier' of S & the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b1 being set for b2 being set holds ( not b1 in the carrier' of T or not b2 = the Arity of T . b1 or b2 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b1) ) ) ) thus rng (id the carrier of T) c= the carrier of S by A1; ::_thesis: ( rng (id the carrier' of T) c= the carrier' of S & the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b1 being set for b2 being set holds ( not b1 in the carrier' of T or not b2 = the Arity of T . b1 or b2 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b1) ) ) ) A4: dom the Arity of T = the carrier' of T by FUNCT_2:def_1; ( dom the Arity of S = the carrier' of S & rng (id the carrier' of T) = the carrier' of T ) by FUNCT_2:def_1; hence rng (id the carrier' of T) c= the carrier' of S by A2, A4, GRFUNC_1:2; ::_thesis: ( the ResultSort of T * (id the carrier of T) = (id the carrier' of T) * the ResultSort of S & ( for b1 being set for b2 being set holds ( not b1 in the carrier' of T or not b2 = the Arity of T . b1 or b2 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b1) ) ) ) A5: dom the ResultSort of T = the carrier' of T by Th7; rng the ResultSort of T c= the carrier of T by RELAT_1:def_19; hence (id the carrier of T) * the ResultSort of T = the ResultSort of T by RELAT_1:53 .= the ResultSort of S | the carrier' of T by A3, A5, GRFUNC_1:23 .= the ResultSort of S * (id the carrier' of T) by RELAT_1:65 ; ::_thesis: for b1 being set for b2 being set holds ( not b1 in the carrier' of T or not b2 = the Arity of T . b1 or b2 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . b1) ) let o be set ; ::_thesis: for b1 being set holds ( not o in the carrier' of T or not b1 = the Arity of T . o or b1 * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o) ) let p be Function; ::_thesis: ( not o in the carrier' of T or not p = the Arity of T . o or p * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o) ) assume that A6: o in the carrier' of T and A7: p = the Arity of T . o ; ::_thesis: p * (id the carrier of T) = the Arity of S . ((id the carrier' of T) . o) reconsider q = p as Element of the carrier of T * by A6, A7, FUNCT_2:5; rng q c= the carrier of T by FINSEQ_1:def_4; hence (id the carrier of T) * p = p by RELAT_1:53 .= the Arity of S . o by A2, A4, A6, A7, GRFUNC_1:2 .= the Arity of S . ((id the carrier' of T) . o) by A6, FUNCT_1:17 ; ::_thesis: verum end; theorem :: INSTALG1:14 for S, T being feasible ManySortedSign st the carrier of T c= the carrier of S & the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T holds T is Subsignature of S proof let S, T be feasible ManySortedSign ; ::_thesis: ( the carrier of T c= the carrier of S & the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T implies T is Subsignature of S ) assume A1: the carrier of T c= the carrier of S ; ::_thesis: ( not the Arity of T = the Arity of S | the carrier' of T or not the ResultSort of T = the ResultSort of S | the carrier' of T or T is Subsignature of S ) assume that A2: the Arity of T = the Arity of S | the carrier' of T and A3: the ResultSort of T = the ResultSort of S | the carrier' of T ; ::_thesis: T is Subsignature of S the Arity of T c= the Arity of S by A2, RELAT_1:59; hence T is Subsignature of S by A1, A3, Th13, RELAT_1:59; ::_thesis: verum end; theorem Th15: :: INSTALG1:15 for S being feasible ManySortedSign holds S is Subsignature of S proof let S be feasible ManySortedSign ; ::_thesis: S is Subsignature of S thus id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8; :: according to INSTALG1:def_2 ::_thesis: verum end; theorem :: INSTALG1:16 for S1 being feasible ManySortedSign for S2 being Subsignature of S1 for S3 being Subsignature of S2 holds S3 is Subsignature of S1 proof let S1 be feasible ManySortedSign ; ::_thesis: for S2 being Subsignature of S1 for S3 being Subsignature of S2 holds S3 is Subsignature of S1 let S2 be Subsignature of S1; ::_thesis: for S3 being Subsignature of S2 holds S3 is Subsignature of S1 let S3 be Subsignature of S2; ::_thesis: S3 is Subsignature of S1 rng (id the carrier of S3) = the carrier of S3 ; then A1: (id the carrier of S2) * (id the carrier of S3) = id the carrier of S3 by Th10, RELAT_1:53; rng (id the carrier' of S3) = the carrier' of S3 ; then A2: (id the carrier' of S2) * (id the carrier' of S3) = id the carrier' of S3 by Th10, RELAT_1:53; ( id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S2 & id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 ) by Def2; hence id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S1 by A1, A2, PUA2MSS1:29; :: according to INSTALG1:def_2 ::_thesis: verum end; theorem :: INSTALG1:17 for S1 being feasible ManySortedSign for S2 being Subsignature of S1 st S1 is Subsignature of S2 holds ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) proof let S1 be feasible ManySortedSign ; ::_thesis: for S2 being Subsignature of S1 st S1 is Subsignature of S2 holds ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) let S2 be Subsignature of S1; ::_thesis: ( S1 is Subsignature of S2 implies ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) ) A1: the carrier of S2 c= the carrier of S1 by Th10; assume A2: S1 is Subsignature of S2 ; ::_thesis: ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) then the carrier of S1 c= the carrier of S2 by Th10; then A3: the carrier of S1 = the carrier of S2 by A1, XBOOLE_0:def_10; A4: the carrier' of S2 c= the carrier' of S1 by Th10; the carrier' of S1 c= the carrier' of S2 by A2, Th10; then A5: the carrier' of S1 = the carrier' of S2 by A4, XBOOLE_0:def_10; A6: the Arity of S2 c= the Arity of S1 by Th11; A7: the ResultSort of S2 c= the ResultSort of S1 by Th11; the ResultSort of S1 c= the ResultSort of S2 by A2, Th11; then A8: the ResultSort of S1 = the ResultSort of S2 by A7, XBOOLE_0:def_10; the Arity of S1 c= the Arity of S2 by A2, Th11; hence ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) by A6, A3, A5, A8, XBOOLE_0:def_10; ::_thesis: verum end; registration let S be non empty ManySortedSign ; cluster non empty feasible for Subsignature of S; existence not for b1 being Subsignature of S holds b1 is empty proof reconsider T = S as Subsignature of S by Th15; take T ; ::_thesis: not T is empty thus not T is empty ; ::_thesis: verum end; end; registration let S be non void feasible ManySortedSign ; cluster non void feasible for Subsignature of S; existence not for b1 being Subsignature of S holds b1 is void proof reconsider T = S as Subsignature of S by Th15; take T ; ::_thesis: not T is void thus not T is void ; ::_thesis: verum end; end; theorem :: INSTALG1:18 for S being feasible ManySortedSign for S9 being Subsignature of S for T being ManySortedSign for f, g being Function st f,g form_morphism_between S,T holds f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T proof let S be feasible ManySortedSign ; ::_thesis: for S9 being Subsignature of S for T being ManySortedSign for f, g being Function st f,g form_morphism_between S,T holds f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T let S9 be Subsignature of S; ::_thesis: for T being ManySortedSign for f, g being Function st f,g form_morphism_between S,T holds f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T let T be ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S,T holds f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T let f, g be Function; ::_thesis: ( f,g form_morphism_between S,T implies f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T ) A1: g | the carrier' of S9 = g * (id the carrier' of S9) by RELAT_1:65; ( id the carrier of S9, id the carrier' of S9 form_morphism_between S9,S & f | the carrier of S9 = f * (id the carrier of S9) ) by Def2, RELAT_1:65; hence ( f,g form_morphism_between S,T implies f | the carrier of S9,g | the carrier' of S9 form_morphism_between S9,T ) by A1, PUA2MSS1:29; ::_thesis: verum end; theorem :: INSTALG1:19 for S being ManySortedSign for T being feasible ManySortedSign for T9 being Subsignature of T for f, g being Function st f,g form_morphism_between S,T9 holds f,g form_morphism_between S,T proof let S be ManySortedSign ; ::_thesis: for T being feasible ManySortedSign for T9 being Subsignature of T for f, g being Function st f,g form_morphism_between S,T9 holds f,g form_morphism_between S,T let T be feasible ManySortedSign ; ::_thesis: for T9 being Subsignature of T for f, g being Function st f,g form_morphism_between S,T9 holds f,g form_morphism_between S,T let T9 be Subsignature of T; ::_thesis: for f, g being Function st f,g form_morphism_between S,T9 holds f,g form_morphism_between S,T let f, g be Function; ::_thesis: ( f,g form_morphism_between S,T9 implies f,g form_morphism_between S,T ) assume A1: f,g form_morphism_between S,T9 ; ::_thesis: f,g form_morphism_between S,T rng f c= the carrier of T9 by A1, PUA2MSS1:def_12; then A2: (id the carrier of T9) * f = f by RELAT_1:53; rng g c= the carrier' of T9 by A1, PUA2MSS1:def_12; then A3: (id the carrier' of T9) * g = g by RELAT_1:53; id the carrier of T9, id the carrier' of T9 form_morphism_between T9,T by Def2; hence f,g form_morphism_between S,T by A1, A2, A3, PUA2MSS1:29; ::_thesis: verum end; theorem :: INSTALG1:20 for S being ManySortedSign for T being feasible ManySortedSign for T9 being Subsignature of T for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds f,g form_morphism_between S,T9 proof let S be ManySortedSign ; ::_thesis: for T being feasible ManySortedSign for T9 being Subsignature of T for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds f,g form_morphism_between S,T9 let T be feasible ManySortedSign ; ::_thesis: for T9 being Subsignature of T for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds f,g form_morphism_between S,T9 let T9 be Subsignature of T; ::_thesis: for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 holds f,g form_morphism_between S,T9 let f, g be Function; ::_thesis: ( f,g form_morphism_between S,T & rng f c= the carrier of T9 & rng g c= the carrier' of T9 implies f,g form_morphism_between S,T9 ) assume that A1: dom f = the carrier of S and A2: dom g = the carrier' of S and rng f c= the carrier of T and rng g c= the carrier' of T and A3: f * the ResultSort of S = the ResultSort of T * g and A4: for o being set for p being Function st o in the carrier' of S & p = the Arity of S . o holds f * p = the Arity of T . (g . o) and A5: rng f c= the carrier of T9 and A6: rng g c= the carrier' of T9 ; :: according to PUA2MSS1:def_12 ::_thesis: f,g form_morphism_between S,T9 thus ( dom f = the carrier of S & dom g = the carrier' of S ) by A1, A2; :: according to PUA2MSS1:def_12 ::_thesis: ( rng f c= the carrier of T9 & rng g c= the carrier' of T9 & the ResultSort of S * f = g * the ResultSort of T9 & ( for b1 being set for b2 being set holds ( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * f = the Arity of T9 . (g . b1) ) ) ) thus ( rng f c= the carrier of T9 & rng g c= the carrier' of T9 ) by A5, A6; ::_thesis: ( the ResultSort of S * f = g * the ResultSort of T9 & ( for b1 being set for b2 being set holds ( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * f = the Arity of T9 . (g . b1) ) ) ) thus f * the ResultSort of S = the ResultSort of T * ((id the carrier' of T9) * g) by A3, A6, RELAT_1:53 .= ( the ResultSort of T * (id the carrier' of T9)) * g by RELAT_1:36 .= ( the ResultSort of T | the carrier' of T9) * g by RELAT_1:65 .= the ResultSort of T9 * g by Th12 ; ::_thesis: for b1 being set for b2 being set holds ( not b1 in the carrier' of S or not b2 = the Arity of S . b1 or b2 * f = the Arity of T9 . (g . b1) ) let o be set ; ::_thesis: for b1 being set holds ( not o in the carrier' of S or not b1 = the Arity of S . o or b1 * f = the Arity of T9 . (g . o) ) let p be Function; ::_thesis: ( not o in the carrier' of S or not p = the Arity of S . o or p * f = the Arity of T9 . (g . o) ) assume that A7: o in the carrier' of S and A8: p = the Arity of S . o ; ::_thesis: p * f = the Arity of T9 . (g . o) A9: ( the Arity of T9 c= the Arity of T & dom the Arity of T9 = the carrier' of T9 ) by Th11, FUNCT_2:def_1; g . o in rng g by A2, A7, FUNCT_1:def_3; then the Arity of T9 . (g . o) = the Arity of T . (g . o) by A6, A9, GRFUNC_1:2; hence p * f = the Arity of T9 . (g . o) by A4, A7, A8; ::_thesis: verum end; begin definition let S1, S2 be non empty ManySortedSign ; let A be MSAlgebra over S2; let f, g be Function; assume B1: f,g form_morphism_between S1,S2 ; funcA | (S1,f,g) -> strict MSAlgebra over S1 means :Def3: :: INSTALG1:def 3 ( the Sorts of it = the Sorts of A * f & the Charact of it = the Charact of A * g ); existence ex b1 being strict MSAlgebra over S1 st ( the Sorts of b1 = the Sorts of A * f & the Charact of b1 = the Charact of A * g ) proof ( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by B1, PUA2MSS1:def_12; then reconsider f9 = f as Function of the carrier of S1, the carrier of S2 by FUNCT_2:def_1, RELSET_1:4; A1: rng g c= the carrier' of S2 by B1, PUA2MSS1:def_12; A2: dom g = the carrier' of S1 by B1, PUA2MSS1:def_12; then reconsider g9 = g as Function of the carrier' of S1, the carrier' of S2 by A1, FUNCT_2:2; dom the Charact of A = the carrier' of S2 by PARTFUN1:def_2; then dom ( the Charact of A * g9) = the carrier' of S1 by A2, A1, RELAT_1:27; then reconsider C = the Charact of A * g9 as ManySortedSet of the carrier' of S1 by PARTFUN1:def_2; C is ManySortedFunction of (( the Sorts of A * f9) #) * the Arity of S1,( the Sorts of A * f9) * the ResultSort of S1 proof let o be set ; :: according to PBOOLE:def_15 ::_thesis: ( not o in the carrier' of S1 or C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):] ) assume A3: o in the carrier' of S1 ; ::_thesis: C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):] then reconsider p1 = the Arity of S1 . o as Element of the carrier of S1 * by FUNCT_2:5; A4: g . o in rng g by A2, A3, FUNCT_1:def_3; then reconsider p2 = the Arity of S2 . (g . o) as Element of the carrier of S2 * by A1, FUNCT_2:5; reconsider o = o as OperSymbol of S1 by A3; A5: C . o = the Charact of A . (g9 . o) by A1, A3, A4, FUNCT_2:15; ( the Sorts of A * f9) * the ResultSort of S1 = the Sorts of A * (f9 * the ResultSort of S1) by RELAT_1:36 .= the Sorts of A * ( the ResultSort of S2 * g) by B1, PUA2MSS1:def_12 .= ( the Sorts of A * the ResultSort of S2) * g by RELAT_1:36 ; then A6: (( the Sorts of A * f9) * the ResultSort of S1) . o = ( the Sorts of A * the ResultSort of S2) . (g9 . o) by A1, A3, A4, FUNCT_2:15; A7: ( the Sorts of A * f9) * p1 = the Sorts of A * (f9 * p1) by RELAT_1:36 .= the Sorts of A * p2 by B1, A3, PUA2MSS1:def_12 ; ((( the Sorts of A * f9) #) * the Arity of S1) . o = (( the Sorts of A * f9) #) . p1 by A3, FUNCT_2:15 .= product (( the Sorts of A * f9) * p1) by FINSEQ_2:def_5 .= ( the Sorts of A #) . p2 by A7, FINSEQ_2:def_5 .= (( the Sorts of A #) * the Arity of S2) . (g9 . o) by A1, A4, FUNCT_2:15 ; hence C . o is Element of bool [:(((( the Sorts of A * f9) #) * the Arity of S1) . o),((( the Sorts of A * f9) * the ResultSort of S1) . o):] by A1, A4, A6, A5, PBOOLE:def_15; ::_thesis: verum end; then reconsider C = C as ManySortedFunction of (( the Sorts of A * f9) #) * the Arity of S1,( the Sorts of A * f9) * the ResultSort of S1 ; take MSAlgebra(# ( the Sorts of A * f9),C #) ; ::_thesis: ( the Sorts of MSAlgebra(# ( the Sorts of A * f9),C #) = the Sorts of A * f & the Charact of MSAlgebra(# ( the Sorts of A * f9),C #) = the Charact of A * g ) thus ( the Sorts of MSAlgebra(# ( the Sorts of A * f9),C #) = the Sorts of A * f & the Charact of MSAlgebra(# ( the Sorts of A * f9),C #) = the Charact of A * g ) ; ::_thesis: verum end; correctness uniqueness for b1, b2 being strict MSAlgebra over S1 st the Sorts of b1 = the Sorts of A * f & the Charact of b1 = the Charact of A * g & the Sorts of b2 = the Sorts of A * f & the Charact of b2 = the Charact of A * g holds b1 = b2; ; end; :: deftheorem Def3 defines | INSTALG1:def_3_:_ for S1, S2 being non empty ManySortedSign for A being MSAlgebra over S2 for f, g being Function st f,g form_morphism_between S1,S2 holds for b6 being strict MSAlgebra over S1 holds ( b6 = A | (S1,f,g) iff ( the Sorts of b6 = the Sorts of A * f & the Charact of b6 = the Charact of A * g ) ); definition let S2, S1 be non empty ManySortedSign ; let A be MSAlgebra over S2; funcA | S1 -> strict MSAlgebra over S1 equals :: INSTALG1:def 4 A | (S1,(id the carrier of S1),(id the carrier' of S1)); correctness coherence A | (S1,(id the carrier of S1),(id the carrier' of S1)) is strict MSAlgebra over S1; ; end; :: deftheorem defines | INSTALG1:def_4_:_ for S2, S1 being non empty ManySortedSign for A being MSAlgebra over S2 holds A | S1 = A | (S1,(id the carrier of S1),(id the carrier' of S1)); theorem :: INSTALG1:21 for S1, S2 being non empty ManySortedSign for A, B being MSAlgebra over S2 st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds for f, g being Function st f,g form_morphism_between S1,S2 holds A | (S1,f,g) = B | (S1,f,g) proof let S1, S2 be non empty ManySortedSign ; ::_thesis: for A, B being MSAlgebra over S2 st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds for f, g being Function st f,g form_morphism_between S1,S2 holds A | (S1,f,g) = B | (S1,f,g) let A, B be MSAlgebra over S2; ::_thesis: ( MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) implies for f, g being Function st f,g form_morphism_between S1,S2 holds A | (S1,f,g) = B | (S1,f,g) ) assume A1: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds A | (S1,f,g) = B | (S1,f,g) let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies A | (S1,f,g) = B | (S1,f,g) ) assume A2: f,g form_morphism_between S1,S2 ; ::_thesis: A | (S1,f,g) = B | (S1,f,g) then ( the Sorts of (A | (S1,f,g)) = the Sorts of A * f & the Charact of (A | (S1,f,g)) = the Charact of A * g ) by Def3; hence A | (S1,f,g) = B | (S1,f,g) by A1, A2, Def3; ::_thesis: verum end; theorem Th22: :: INSTALG1:22 for S1, S2 being non empty ManySortedSign for A being non-empty MSAlgebra over S2 for f, g being Function st f,g form_morphism_between S1,S2 holds A | (S1,f,g) is non-empty proof let S1, S2 be non empty ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S2 for f, g being Function st f,g form_morphism_between S1,S2 holds A | (S1,f,g) is non-empty let A be non-empty MSAlgebra over S2; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds A | (S1,f,g) is non-empty let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies A | (S1,f,g) is non-empty ) assume f,g form_morphism_between S1,S2 ; ::_thesis: A | (S1,f,g) is non-empty then the Sorts of (A | (S1,f,g)) = the Sorts of A * f by Def3; hence the Sorts of (A | (S1,f,g)) is V16() ; :: according to MSUALG_1:def_3 ::_thesis: verum end; registration let S2 be non empty ManySortedSign ; let S1 be non empty Subsignature of S2; let A be non-empty MSAlgebra over S2; clusterA | S1 -> strict non-empty ; coherence A | S1 is non-empty proof id the carrier of S1, id the carrier' of S1 form_morphism_between S1,S2 by Def2; hence A | S1 is non-empty by Th22; ::_thesis: verum end; end; theorem Th23: :: INSTALG1:23 for S1, S2 being non empty non void ManySortedSign for f, g being Function st f,g form_morphism_between S1,S2 holds for A being MSAlgebra over S2 for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds Den (o1,(A | (S1,f,g))) = Den (o2,A) proof let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds for A being MSAlgebra over S2 for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds Den (o1,(A | (S1,f,g))) = Den (o2,A) let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra over S2 for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds Den (o1,(A | (S1,f,g))) = Den (o2,A) ) assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A being MSAlgebra over S2 for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds Den (o1,(A | (S1,f,g))) = Den (o2,A) then reconsider g9 = g as Function of the carrier' of S1, the carrier' of S2 by Th9; let A be MSAlgebra over S2; ::_thesis: for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds Den (o1,(A | (S1,f,g))) = Den (o2,A) let o1 be OperSymbol of S1; ::_thesis: for o2 being OperSymbol of S2 st o2 = g . o1 holds Den (o1,(A | (S1,f,g))) = Den (o2,A) let o2 be OperSymbol of S2; ::_thesis: ( o2 = g . o1 implies Den (o1,(A | (S1,f,g))) = Den (o2,A) ) assume o2 = g . o1 ; ::_thesis: Den (o1,(A | (S1,f,g))) = Den (o2,A) then the Charact of A . o2 = ( the Charact of A * g9) . o1 by FUNCT_2:15 .= the Charact of (A | (S1,f,g)) . o1 by A1, Def3 ; hence Den (o1,(A | (S1,f,g))) = Den (o2,A) ; ::_thesis: verum end; theorem Th24: :: INSTALG1:24 for S1, S2 being non empty non void ManySortedSign for f, g being Function st f,g form_morphism_between S1,S2 holds for A being MSAlgebra over S2 for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) proof let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds for A being MSAlgebra over S2 for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra over S2 for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) ) assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A being MSAlgebra over S2 for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) A2: dom f = the carrier of S1 by A1, PUA2MSS1:def_12; let A be MSAlgebra over S2; ::_thesis: for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 holds ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) let o1 be OperSymbol of S1; ::_thesis: for o2 being OperSymbol of S2 st o2 = g . o1 holds ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) let o2 be OperSymbol of S2; ::_thesis: ( o2 = g . o1 implies ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) ) assume A3: o2 = g . o1 ; ::_thesis: ( Args (o2,A) = Args (o1,(A | (S1,f,g))) & Result (o1,(A | (S1,f,g))) = Result (o2,A) ) thus Args (o2,A) = product ( the Sorts of A * (the_arity_of o2)) by PRALG_2:3 .= product ( the Sorts of A * (f * (the_arity_of o1))) by A1, A3, PUA2MSS1:def_12 .= product (( the Sorts of A * f) * (the_arity_of o1)) by RELAT_1:36 .= product ( the Sorts of (A | (S1,f,g)) * (the_arity_of o1)) by A1, Def3 .= Args (o1,(A | (S1,f,g))) by PRALG_2:3 ; ::_thesis: Result (o1,(A | (S1,f,g))) = Result (o2,A) dom g = the carrier' of S1 by A1, PUA2MSS1:def_12; then the_result_sort_of o2 = ( the ResultSort of S2 * g) . o1 by A3, FUNCT_1:13 .= (f * the ResultSort of S1) . o1 by A1, PUA2MSS1:def_12 .= f . (the_result_sort_of o1) by FUNCT_2:15 ; hence Result (o2,A) = the Sorts of A . (f . (the_result_sort_of o1)) by PRALG_2:3 .= ( the Sorts of A * f) . (the_result_sort_of o1) by A2, FUNCT_1:13 .= the Sorts of (A | (S1,f,g)) . (the_result_sort_of o1) by A1, Def3 .= Result (o1,(A | (S1,f,g))) by PRALG_2:3 ; ::_thesis: verum end; theorem Th25: :: INSTALG1:25 for S being non empty ManySortedSign for A being MSAlgebra over S holds A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #) proof let S be non empty ManySortedSign ; ::_thesis: for A being MSAlgebra over S holds A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #) let A be MSAlgebra over S; ::_thesis: A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #) set f = id the carrier of S; set g = id the carrier' of S; dom the Charact of A = the carrier' of S by PARTFUN1:def_2; then A1: the Charact of MSAlgebra(# the Sorts of A, the Charact of A #) = the Charact of A * (id the carrier' of S) by RELAT_1:52; dom the Sorts of A = the carrier of S by PARTFUN1:def_2; then A2: the Sorts of MSAlgebra(# the Sorts of A, the Charact of A #) = the Sorts of A * (id the carrier of S) by RELAT_1:52; id the carrier of S, id the carrier' of S form_morphism_between S,S by Th8; hence A | (S,(id the carrier of S),(id the carrier' of S)) = MSAlgebra(# the Sorts of A, the Charact of A #) by A2, A1, Def3; ::_thesis: verum end; theorem :: INSTALG1:26 for S being non empty ManySortedSign for A being MSAlgebra over S holds A | S = MSAlgebra(# the Sorts of A, the Charact of A #) by Th25; theorem Th27: :: INSTALG1:27 for S1, S2, S3 being non empty ManySortedSign for f1, g1 being Function st f1,g1 form_morphism_between S1,S2 holds for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) proof let S1, S2, S3 be non empty ManySortedSign ; ::_thesis: for f1, g1 being Function st f1,g1 form_morphism_between S1,S2 holds for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) let f1, g1 be Function; ::_thesis: ( f1,g1 form_morphism_between S1,S2 implies for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) ) assume A1: f1,g1 form_morphism_between S1,S2 ; ::_thesis: for f2, g2 being Function st f2,g2 form_morphism_between S2,S3 holds for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) let f2, g2 be Function; ::_thesis: ( f2,g2 form_morphism_between S2,S3 implies for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) ) assume A2: f2,g2 form_morphism_between S2,S3 ; ::_thesis: for A being MSAlgebra over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) A3: f2 * f1,g2 * g1 form_morphism_between S1,S3 by A1, A2, PUA2MSS1:29; let A be MSAlgebra over S3; ::_thesis: A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) A4: the Charact of ((A | (S2,f2,g2)) | (S1,f1,g1)) = the Charact of (A | (S2,f2,g2)) * g1 by A1, Def3 .= ( the Charact of A * g2) * g1 by A2, Def3 .= the Charact of A * (g2 * g1) by RELAT_1:36 ; the Sorts of ((A | (S2,f2,g2)) | (S1,f1,g1)) = the Sorts of (A | (S2,f2,g2)) * f1 by A1, Def3 .= ( the Sorts of A * f2) * f1 by A2, Def3 .= the Sorts of A * (f2 * f1) by RELAT_1:36 ; hence A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1) by A3, A4, Def3; ::_thesis: verum end; theorem :: INSTALG1:28 for S1 being non empty feasible ManySortedSign for S2 being non empty Subsignature of S1 for S3 being non empty Subsignature of S2 for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3 proof let S1 be non empty feasible ManySortedSign ; ::_thesis: for S2 being non empty Subsignature of S1 for S3 being non empty Subsignature of S2 for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3 let S2 be non empty Subsignature of S1; ::_thesis: for S3 being non empty Subsignature of S2 for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3 let S3 be non empty Subsignature of S2; ::_thesis: for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3 let A be MSAlgebra over S1; ::_thesis: A | S3 = (A | S2) | S3 set f1 = id the carrier of S2; set g1 = id the carrier' of S2; set f2 = id the carrier of S3; set g2 = id the carrier' of S3; rng (id the carrier of S3) = the carrier of S3 ; then A1: (id the carrier of S2) * (id the carrier of S3) = id the carrier of S3 by Th10, RELAT_1:53; rng (id the carrier' of S3) = the carrier' of S3 ; then A2: (id the carrier' of S2) * (id the carrier' of S3) = id the carrier' of S3 by Th10, RELAT_1:53; ( id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 & id the carrier of S3, id the carrier' of S3 form_morphism_between S3,S2 ) by Def2; hence A | S3 = (A | S2) | S3 by A1, A2, Th27; ::_thesis: verum end; theorem Th29: :: INSTALG1:29 for S1, S2 being non empty ManySortedSign for f being Function of the carrier of S1, the carrier of S2 for g being Function st f,g form_morphism_between S1,S2 holds for A1, A2 being MSAlgebra over S2 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) proof let S1, S2 be non empty ManySortedSign ; ::_thesis: for f being Function of the carrier of S1, the carrier of S2 for g being Function st f,g form_morphism_between S1,S2 holds for A1, A2 being MSAlgebra over S2 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) let f be Function of the carrier of S1, the carrier of S2; ::_thesis: for g being Function st f,g form_morphism_between S1,S2 holds for A1, A2 being MSAlgebra over S2 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) let g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A1, A2 being MSAlgebra over S2 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) ) assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A1, A2 being MSAlgebra over S2 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) let A1, A2 be MSAlgebra over S2; ::_thesis: for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) let h be ManySortedFunction of the Sorts of A1, the Sorts of A2; ::_thesis: h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g)) set B1 = A1 | (S1,f,g); set B2 = A2 | (S1,f,g); let x be set ; :: according to PBOOLE:def_15 ::_thesis: ( not x in the carrier of S1 or (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):] ) assume x in the carrier of S1 ; ::_thesis: (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):] then reconsider s = x as SortSymbol of S1 ; reconsider fs = f . s as SortSymbol of S2 ; A2: ( (h * f) . s = h . fs & the Sorts of A1 . fs = ( the Sorts of A1 * f) . s ) by FUNCT_2:15; A3: the Sorts of A2 . fs = ( the Sorts of A2 * f) . s by FUNCT_2:15; ( the Sorts of A1 * f = the Sorts of (A1 | (S1,f,g)) & the Sorts of A2 * f = the Sorts of (A2 | (S1,f,g)) ) by A1, Def3; hence (h * f) . x is Element of bool [:( the Sorts of (A1 | (S1,f,g)) . x),( the Sorts of (A2 | (S1,f,g)) . x):] by A2, A3; ::_thesis: verum end; theorem :: INSTALG1:30 for S1 being non empty ManySortedSign for S2 being non empty Subsignature of S1 for A1, A2 being MSAlgebra over S1 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2) proof let S1 be non empty ManySortedSign ; ::_thesis: for S2 being non empty Subsignature of S1 for A1, A2 being MSAlgebra over S1 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2) let S2 be non empty Subsignature of S1; ::_thesis: for A1, A2 being MSAlgebra over S1 for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2) set f = id the carrier of S2; set g = id the carrier' of S2; let A1, A2 be MSAlgebra over S1; ::_thesis: for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2) let h be ManySortedFunction of the Sorts of A1, the Sorts of A2; ::_thesis: h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2) A1: id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 by Def2; then reconsider f = id the carrier of S2 as Function of the carrier of S2, the carrier of S1 by Th9; h * f is ManySortedFunction of the Sorts of (A1 | (S2,f,(id the carrier' of S2))), the Sorts of (A2 | (S2,f,(id the carrier' of S2))) by A1, Th29; hence h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2) by RELAT_1:65; ::_thesis: verum end; theorem Th31: :: INSTALG1:31 for S1, S2 being non empty ManySortedSign for f, g being Function st f,g form_morphism_between S1,S2 holds for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g)) proof let S1, S2 be non empty ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g)) let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g)) ) assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g)) ( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by A1, PUA2MSS1:def_12; then reconsider f = f as Function of the carrier of S1, the carrier of S2 by FUNCT_2:def_1, RELSET_1:4; let A be MSAlgebra over S2; ::_thesis: (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g)) now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S1_holds_ ((id_the_Sorts_of_A)_*_f)_._i_=_(id_the_Sorts_of_(A_|_(S1,f,g)))_._i let i be set ; ::_thesis: ( i in the carrier of S1 implies ((id the Sorts of A) * f) . i = (id the Sorts of (A | (S1,f,g))) . i ) assume i in the carrier of S1 ; ::_thesis: ((id the Sorts of A) * f) . i = (id the Sorts of (A | (S1,f,g))) . i then reconsider s = i as SortSymbol of S1 ; thus ((id the Sorts of A) * f) . i = (id the Sorts of A) . (f . s) by FUNCT_2:15 .= id ( the Sorts of A . (f . s)) by MSUALG_3:def_1 .= id (( the Sorts of A * f) . s) by FUNCT_2:15 .= id ( the Sorts of (A | (S1,f,g)) . s) by A1, Def3 .= (id the Sorts of (A | (S1,f,g))) . i by MSUALG_3:def_1 ; ::_thesis: verum end; hence (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g)) by PBOOLE:3; ::_thesis: verum end; theorem :: INSTALG1:32 for S1 being non empty ManySortedSign for S2 being non empty Subsignature of S1 for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2) proof let S1 be non empty ManySortedSign ; ::_thesis: for S2 being non empty Subsignature of S1 for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2) let S2 be non empty Subsignature of S1; ::_thesis: for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2) set f = id the carrier of S2; set g = id the carrier' of S2; let A be MSAlgebra over S1; ::_thesis: (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2) id the carrier of S2, id the carrier' of S2 form_morphism_between S2,S1 by Def2; then (id the Sorts of A) * (id the carrier of S2) = id the Sorts of (A | S2) by Th31; hence (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2) by RELAT_1:65; ::_thesis: verum end; theorem Th33: :: INSTALG1:33 for S1, S2 being non empty non void ManySortedSign for f, g being Function st f,g form_morphism_between S1,S2 holds for A, B being MSAlgebra over S2 for h2 being ManySortedFunction of A,B for h1 being ManySortedFunction of (A | (S1,f,g)),(B | (S1,f,g)) st h1 = h2 * f holds for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A) <> {} & Args (o2,B) <> {} holds for x2 being Element of Args (o2,A) for x1 being Element of Args (o1,(A | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 proof let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds for A, B being MSAlgebra over S2 for h2 being ManySortedFunction of A,B for h1 being ManySortedFunction of (A | (S1,f,g)),(B | (S1,f,g)) st h1 = h2 * f holds for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A) <> {} & Args (o2,B) <> {} holds for x2 being Element of Args (o2,A) for x1 being Element of Args (o1,(A | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 let f, g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for A, B being MSAlgebra over S2 for h2 being ManySortedFunction of A,B for h1 being ManySortedFunction of (A | (S1,f,g)),(B | (S1,f,g)) st h1 = h2 * f holds for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A) <> {} & Args (o2,B) <> {} holds for x2 being Element of Args (o2,A) for x1 being Element of Args (o1,(A | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 ) assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for A, B being MSAlgebra over S2 for h2 being ManySortedFunction of A,B for h1 being ManySortedFunction of (A | (S1,f,g)),(B | (S1,f,g)) st h1 = h2 * f holds for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A) <> {} & Args (o2,B) <> {} holds for x2 being Element of Args (o2,A) for x1 being Element of Args (o1,(A | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 let A2, B2 be MSAlgebra over S2; ::_thesis: for h2 being ManySortedFunction of A2,B2 for h1 being ManySortedFunction of (A2 | (S1,f,g)),(B2 | (S1,f,g)) st h1 = h2 * f holds for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds for x2 being Element of Args (o2,A2) for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 set A1 = A2 | (S1,f,g); set B1 = B2 | (S1,f,g); let h2 be ManySortedFunction of A2,B2; ::_thesis: for h1 being ManySortedFunction of (A2 | (S1,f,g)),(B2 | (S1,f,g)) st h1 = h2 * f holds for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds for x2 being Element of Args (o2,A2) for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 let h1 be ManySortedFunction of (A2 | (S1,f,g)),(B2 | (S1,f,g)); ::_thesis: ( h1 = h2 * f implies for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds for x2 being Element of Args (o2,A2) for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 ) assume A2: h1 = h2 * f ; ::_thesis: for o1 being OperSymbol of S1 for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds for x2 being Element of Args (o2,A2) for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 let o1 be OperSymbol of S1; ::_thesis: for o2 being OperSymbol of S2 st o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} holds for x2 being Element of Args (o2,A2) for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 let o2 be OperSymbol of S2; ::_thesis: ( o2 = g . o1 & Args (o2,A2) <> {} & Args (o2,B2) <> {} implies for x2 being Element of Args (o2,A2) for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 ) assume A3: o2 = g . o1 ; ::_thesis: ( not Args (o2,A2) <> {} or not Args (o2,B2) <> {} or for x2 being Element of Args (o2,A2) for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 ) assume that A4: Args (o2,A2) <> {} and A5: Args (o2,B2) <> {} ; ::_thesis: for x2 being Element of Args (o2,A2) for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 let x2 be Element of Args (o2,A2); ::_thesis: for x1 being Element of Args (o1,(A2 | (S1,f,g))) st x2 = x1 holds h1 # x1 = h2 # x2 let x1 be Element of Args (o1,(A2 | (S1,f,g))); ::_thesis: ( x2 = x1 implies h1 # x1 = h2 # x2 ) assume A6: x2 = x1 ; ::_thesis: h1 # x1 = h2 # x2 then reconsider f1 = x1, f2 = x2, g2 = h2 # x2 as Function by A4, A5, MSUALG_6:1; A7: Args (o2,A2) = Args (o1,(A2 | (S1,f,g))) by A1, A3, Th24; then A8: dom f1 = dom (the_arity_of o1) by A4, MSUALG_3:6; A9: dom f2 = dom (the_arity_of o2) by A4, MSUALG_3:6; A10: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f1_holds_ g2_._i_=_(h1_._((the_arity_of_o1)_/._i))_._(f1_._i) let i be Nat; ::_thesis: ( i in dom f1 implies g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i) ) assume A11: i in dom f1 ; ::_thesis: g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i) dom f = the carrier of S1 by A1, PUA2MSS1:def_12; then h1 . ((the_arity_of o1) /. i) = h2 . (f . ((the_arity_of o1) /. i)) by A2, FUNCT_1:13 .= h2 . (f . ((the_arity_of o1) . i)) by A8, A11, PARTFUN1:def_6 .= h2 . ((f * (the_arity_of o1)) . i) by A8, A11, FUNCT_1:13 .= h2 . ((the_arity_of o2) . i) by A1, A3, PUA2MSS1:def_12 .= h2 . ((the_arity_of o2) /. i) by A6, A9, A11, PARTFUN1:def_6 ; hence g2 . i = (h1 . ((the_arity_of o1) /. i)) . (f1 . i) by A4, A5, A6, A11, MSUALG_3:24; ::_thesis: verum end; Args (o2,B2) = Args (o1,(B2 | (S1,f,g))) by A1, A3, Th24; hence h1 # x1 = h2 # x2 by A4, A5, A7, A10, MSUALG_3:24; ::_thesis: verum end; theorem Th34: :: INSTALG1:34 for S, S9 being non empty non void ManySortedSign for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) proof let S, S9 be non empty non void ManySortedSign ; ::_thesis: for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) let A1, A2 be MSAlgebra over S; ::_thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) ) assume A1: the Sorts of A1 is_transformable_to the Sorts of A2 ; ::_thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) let h be ManySortedFunction of A1,A2; ::_thesis: ( h is_homomorphism A1,A2 implies for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) ) assume A2: h is_homomorphism A1,A2 ; ::_thesis: for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) let f be Function of the carrier of S9, the carrier of S; ::_thesis: for g being Function st f,g form_morphism_between S9,S holds ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) let g be Function; ::_thesis: ( f,g form_morphism_between S9,S implies ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) ) assume A3: f,g form_morphism_between S9,S ; ::_thesis: ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) A4: ( dom g = the carrier' of S9 & rng g c= the carrier' of S ) by A3, PUA2MSS1:def_12; set B1 = A1 | (S9,f,g); set B2 = A2 | (S9,f,g); reconsider g = g as Function of the carrier' of S9, the carrier' of S by A4, FUNCT_2:def_1, RELSET_1:4; A5: f * the ResultSort of S9 = the ResultSort of S * g by A3, PUA2MSS1:def_12; reconsider h9 = h * f as ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) by A3, Th29; take h9 ; ::_thesis: ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) thus h9 = h * f ; ::_thesis: h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) let o be OperSymbol of S9; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,(A1 | (S9,f,g))) = {} or for b1 being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . b1) = (Den (o,(A2 | (S9,f,g)))) . (h9 # b1) ) set go = g . o; assume A6: Args (o,(A1 | (S9,f,g))) <> {} ; ::_thesis: for b1 being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . b1) = (Den (o,(A2 | (S9,f,g)))) . (h9 # b1) let x be Element of Args (o,(A1 | (S9,f,g))); ::_thesis: (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . x) = (Den (o,(A2 | (S9,f,g)))) . (h9 # x) reconsider y = x as Element of Args ((g . o),A1) by A3, Th24; A7: h9 . (the_result_sort_of o) = h . (f . (the_result_sort_of o)) by FUNCT_2:15 .= h . (( the ResultSort of S * g) . o) by A5, FUNCT_2:15 .= h . (the_result_sort_of (g . o)) by FUNCT_2:15 ; A8: ( Den (o,(A1 | (S9,f,g))) = Den ((g . o),A1) & Den (o,(A2 | (S9,f,g))) = Den ((g . o),A2) ) by A3, Th23; A9: Args (o,(A1 | (S9,f,g))) = Args ((g . o),A1) by A3, Th24; A10: Args (o,(A2 | (S9,f,g))) = Args ((g . o),A2) by A3, Th24; then Args (o,(A2 | (S9,f,g))) <> {} by A1, A6, A9, Th2; then h9 # x = h # y by A3, A6, A9, A10, Th33; hence (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . x) = (Den (o,(A2 | (S9,f,g)))) . (h9 # x) by A2, A6, A9, A8, A7, MSUALG_3:def_7; ::_thesis: verum end; theorem :: INSTALG1:35 for S being non void feasible ManySortedSign for S9 being non void Subsignature of S for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st ( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) proof let S be non void feasible ManySortedSign ; ::_thesis: for S9 being non void Subsignature of S for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st ( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) let S9 be non void Subsignature of S; ::_thesis: for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st ( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) let A1, A2 be MSAlgebra over S; ::_thesis: ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st ( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) ) assume A1: the Sorts of A1 is_transformable_to the Sorts of A2 ; ::_thesis: for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st ( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) set f = id the carrier of S9; set g = id the carrier' of S9; A2: id the carrier of S9, id the carrier' of S9 form_morphism_between S9,S by Def2; then reconsider f = id the carrier of S9 as Function of the carrier of S9, the carrier of S by Th9; let h be ManySortedFunction of A1,A2; ::_thesis: ( h is_homomorphism A1,A2 implies ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st ( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) ) assume h is_homomorphism A1,A2 ; ::_thesis: ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st ( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 ) then consider h9 being ManySortedFunction of (A1 | (S9,f,(id the carrier' of S9))),(A2 | (S9,f,(id the carrier' of S9))) such that A3: h9 = h * f and A4: h9 is_homomorphism A1 | (S9,f,(id the carrier' of S9)),A2 | (S9,f,(id the carrier' of S9)) by A1, A2, Th34; consider k being ManySortedFunction of (A1 | S9),(A2 | S9) such that A5: k = h9 and k is_homomorphism A1 | S9,A2 | S9 by A4; take k ; ::_thesis: ( k = h | the carrier of S9 & k is_homomorphism A1 | S9,A2 | S9 ) thus ( k = h | the carrier of S9 & k is_homomorphism A1 | S9,A2 | S9 ) by A3, A4, A5, RELAT_1:65; ::_thesis: verum end; theorem Th36: :: INSTALG1:36 for S, S9 being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 for t being Function st t is_e.translation_of B,s1,s2 holds t is_e.translation_of A,f . s1,f . s2 proof let S, S9 be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 for t being Function st t is_e.translation_of B,s1,s2 holds t is_e.translation_of A,f . s1,f . s2 let A be non-empty MSAlgebra over S; ::_thesis: for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 for t being Function st t is_e.translation_of B,s1,s2 holds t is_e.translation_of A,f . s1,f . s2 let f be Function of the carrier of S9, the carrier of S; ::_thesis: for g being Function st f,g form_morphism_between S9,S holds for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 for t being Function st t is_e.translation_of B,s1,s2 holds t is_e.translation_of A,f . s1,f . s2 let g be Function; ::_thesis: ( f,g form_morphism_between S9,S implies for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 for t being Function st t is_e.translation_of B,s1,s2 holds t is_e.translation_of A,f . s1,f . s2 ) assume A1: f,g form_morphism_between S9,S ; ::_thesis: for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 for t being Function st t is_e.translation_of B,s1,s2 holds t is_e.translation_of A,f . s1,f . s2 A2: ( dom g = the carrier' of S9 & rng g c= the carrier' of S ) by A1, PUA2MSS1:def_12; let B be non-empty MSAlgebra over S9; ::_thesis: ( B = A | (S9,f,g) implies for s1, s2 being SortSymbol of S9 for t being Function st t is_e.translation_of B,s1,s2 holds t is_e.translation_of A,f . s1,f . s2 ) assume A3: B = A | (S9,f,g) ; ::_thesis: for s1, s2 being SortSymbol of S9 for t being Function st t is_e.translation_of B,s1,s2 holds t is_e.translation_of A,f . s1,f . s2 reconsider g = g as Function of the carrier' of S9, the carrier' of S by A2, FUNCT_2:def_1, RELSET_1:4; let s1, s2 be SortSymbol of S9; ::_thesis: for t being Function st t is_e.translation_of B,s1,s2 holds t is_e.translation_of A,f . s1,f . s2 let t be Function; ::_thesis: ( t is_e.translation_of B,s1,s2 implies t is_e.translation_of A,f . s1,f . s2 ) given o being OperSymbol of S9 such that A4: the_result_sort_of o = s2 and A5: ex i being Element of NAT st ( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st ( a in Args (o,B) & t = transl (o,i,a,B) ) ) ; :: according to MSUALG_6:def_5 ::_thesis: t is_e.translation_of A,f . s1,f . s2 A6: f * (the_arity_of o) = the_arity_of (g . o) by A1, PUA2MSS1:def_12; take g . o ; :: according to MSUALG_6:def_5 ::_thesis: ( the_result_sort_of (g . o) = f . s2 & ex b1 being Element of NAT st ( b1 in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b1 = f . s1 & ex b2 being set st ( b2 in Args ((g . o),A) & t = transl ((g . o),b1,b2,A) ) ) ) f * the ResultSort of S9 = the ResultSort of S * g by A1, PUA2MSS1:def_12; hence the_result_sort_of (g . o) = (f * the ResultSort of S9) . o by FUNCT_2:15 .= f . s2 by A4, FUNCT_2:15 ; ::_thesis: ex b1 being Element of NAT st ( b1 in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b1 = f . s1 & ex b2 being set st ( b2 in Args ((g . o),A) & t = transl ((g . o),b1,b2,A) ) ) consider i being Element of NAT , a being Function such that A7: i in dom (the_arity_of o) and A8: (the_arity_of o) /. i = s1 and A9: a in Args (o,B) and A10: t = transl (o,i,a,B) by A5; take i ; ::_thesis: ( i in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. i = f . s1 & ex b1 being set st ( b1 in Args ((g . o),A) & t = transl ((g . o),i,b1,A) ) ) ( rng (the_arity_of o) c= the carrier of S9 & dom f = the carrier of S9 ) by FINSEQ_1:def_4, FUNCT_2:def_1; hence i in dom (the_arity_of (g . o)) by A7, A6, RELAT_1:27; ::_thesis: ( (the_arity_of (g . o)) /. i = f . s1 & ex b1 being set st ( b1 in Args ((g . o),A) & t = transl ((g . o),i,b1,A) ) ) hence A11: (the_arity_of (g . o)) /. i = (the_arity_of (g . o)) . i by PARTFUN1:def_6 .= f . ((the_arity_of o) . i) by A7, A6, FUNCT_1:13 .= f . s1 by A7, A8, PARTFUN1:def_6 ; ::_thesis: ex b1 being set st ( b1 in Args ((g . o),A) & t = transl ((g . o),i,b1,A) ) then A12: dom (transl ((g . o),i,a,A)) = the Sorts of A . (f . s1) by MSUALG_6:def_4; A13: the Sorts of B = the Sorts of A * f by A1, A3, Def3; then A14: the Sorts of B . s1 = the Sorts of A . (f . s1) by FUNCT_2:15; A15: now__::_thesis:_for_x_being_set_st_x_in_the_Sorts_of_B_._s1_holds_ t_._x_=_(transl_((g_._o),i,a,A))_._x let x be set ; ::_thesis: ( x in the Sorts of B . s1 implies t . x = (transl ((g . o),i,a,A)) . x ) assume x in the Sorts of B . s1 ; ::_thesis: t . x = (transl ((g . o),i,a,A)) . x then ( t . x = (Den (o,B)) . (a +* (i,x)) & (transl ((g . o),i,a,A)) . x = (Den ((g . o),A)) . (a +* (i,x)) ) by A8, A10, A11, A14, MSUALG_6:def_4; hence t . x = (transl ((g . o),i,a,A)) . x by A1, A3, Th23; ::_thesis: verum end; take a ; ::_thesis: ( a in Args ((g . o),A) & t = transl ((g . o),i,a,A) ) thus a in Args ((g . o),A) by A1, A3, A9, Th24; ::_thesis: t = transl ((g . o),i,a,A) dom t = the Sorts of B . s1 by A8, A10, MSUALG_6:def_4; hence t = transl ((g . o),i,a,A) by A12, A13, A15, FUNCT_1:2, FUNCT_2:15; ::_thesis: verum end; Lm1: for S, S9 being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) proof let S, S9 be non empty non void ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) let A be non-empty MSAlgebra over S; ::_thesis: for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) let f be Function of the carrier of S9, the carrier of S; ::_thesis: for g being Function st f,g form_morphism_between S9,S holds for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) let g be Function; ::_thesis: ( f,g form_morphism_between S9,S implies for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) ) assume A1: f,g form_morphism_between S9,S ; ::_thesis: for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) defpred S1[ set , SortSymbol of S9, SortSymbol of S9] means ( TranslationRel S reduces f . $2,f . $3 & $1 is Translation of A,f . $2,f . $3 ); let B be non-empty MSAlgebra over S9; ::_thesis: ( B = A | (S9,f,g) implies for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) ) assume A2: B = A | (S9,f,g) ; ::_thesis: for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) A3: for s1, s2, s3 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds for t being Translation of B,s1,s2 st S1[t,s1,s2] holds for h being Function st h is_e.translation_of B,s2,s3 holds S1[h * t,s1,s3] proof let s1, s2, s3 be SortSymbol of S9; ::_thesis: ( TranslationRel S9 reduces s1,s2 implies for t being Translation of B,s1,s2 st S1[t,s1,s2] holds for h being Function st h is_e.translation_of B,s2,s3 holds S1[h * t,s1,s3] ) assume TranslationRel S9 reduces s1,s2 ; ::_thesis: for t being Translation of B,s1,s2 st S1[t,s1,s2] holds for h being Function st h is_e.translation_of B,s2,s3 holds S1[h * t,s1,s3] let t be Translation of B,s1,s2; ::_thesis: ( S1[t,s1,s2] implies for h being Function st h is_e.translation_of B,s2,s3 holds S1[h * t,s1,s3] ) assume A4: S1[t,s1,s2] ; ::_thesis: for h being Function st h is_e.translation_of B,s2,s3 holds S1[h * t,s1,s3] let h be Function; ::_thesis: ( h is_e.translation_of B,s2,s3 implies S1[h * t,s1,s3] ) assume A5: h is_e.translation_of B,s2,s3 ; ::_thesis: S1[h * t,s1,s3] then [(f . s2),(f . s3)] in TranslationRel S by A1, A2, Th36, MSUALG_6:12; then A6: TranslationRel S reduces f . s2,f . s3 by REWRITE1:15; h is_e.translation_of A,f . s2,f . s3 by A1, A2, A5, Th36; hence S1[h * t,s1,s3] by A4, A6, MSUALG_6:19, REWRITE1:16; ::_thesis: verum end; let s1, s2 be SortSymbol of S9; ::_thesis: ( TranslationRel S9 reduces s1,s2 implies ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) ) assume A7: TranslationRel S9 reduces s1,s2 ; ::_thesis: ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) A8: for s being SortSymbol of S9 holds S1[ id ( the Sorts of B . s),s,s] proof let s be SortSymbol of S9; ::_thesis: S1[ id ( the Sorts of B . s),s,s] thus TranslationRel S reduces f . s,f . s by REWRITE1:12; ::_thesis: id ( the Sorts of B . s) is Translation of A,f . s,f . s the Sorts of B = the Sorts of A * f by A1, A2, Def3; then the Sorts of B . s = the Sorts of A . (f . s) by FUNCT_2:15; hence id ( the Sorts of B . s) is Translation of A,f . s,f . s by MSUALG_6:16; ::_thesis: verum end; for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds for t being Translation of B,s1,s2 holds S1[t,s1,s2] from MSUALG_6:sch_1(A8, A3); hence ( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) ) by A7; ::_thesis: verum end; theorem :: INSTALG1:37 for S, S9 being non empty non void ManySortedSign for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds TranslationRel S reduces f . s1,f . s2 proof let S, S9 be non empty non void ManySortedSign ; ::_thesis: for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds TranslationRel S reduces f . s1,f . s2 set A = the non-empty MSAlgebra over S; let f be Function of the carrier of S9, the carrier of S; ::_thesis: for g being Function st f,g form_morphism_between S9,S holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds TranslationRel S reduces f . s1,f . s2 let g be Function; ::_thesis: ( f,g form_morphism_between S9,S implies for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds TranslationRel S reduces f . s1,f . s2 ) assume A1: f,g form_morphism_between S9,S ; ::_thesis: for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds TranslationRel S reduces f . s1,f . s2 then the non-empty MSAlgebra over S | (S9,f,g) is non-empty MSAlgebra over S9 by Th22; hence for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds TranslationRel S reduces f . s1,f . s2 by A1, Lm1; ::_thesis: verum end; theorem :: INSTALG1:38 for S, S9 being non empty non void ManySortedSign for A being non-empty MSAlgebra over S for f being Function of the carrier of S9, the carrier of S for g being Function st f,g form_morphism_between S9,S holds for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 by Lm1; begin scheme :: INSTALG1:sch 1 GenFuncEx{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> V16() ManySortedSet of the carrier of F1(), F4( set , set ) -> set } : ex h being ManySortedFunction of (FreeMSA F3()),F2() st ( h is_homomorphism FreeMSA F3(),F2() & ( for s being SortSymbol of F1() for x being Element of F3() . s holds (h . s) . (root-tree [x,s]) = F4(x,s) ) ) provided A1: for s being SortSymbol of F1() for x being Element of F3() . s holds F4(x,s) in the Sorts of F2() . s proof defpred S1[ set , set ] means ex f being Function of ((FreeGen F3()) . $1),( the Sorts of F2() . $1) st ( $2 = f & ( for x being Element of F3() . $1 holds f . (root-tree [x,$1]) = F4(x,$1) ) ); A2: for a being set st a in the carrier of F1() holds ex y being set st S1[a,y] proof let a be set ; ::_thesis: ( a in the carrier of F1() implies ex y being set st S1[a,y] ) assume a in the carrier of F1() ; ::_thesis: ex y being set st S1[a,y] then reconsider s = a as SortSymbol of F1() ; defpred S2[ set , set ] means ex x being Element of F3() . s st ( $1 = root-tree [x,s] & $2 = F4(x,s) ); A3: (FreeGen F3()) . s = FreeGen (s,F3()) by MSAFREE:def_16; A4: for y being set st y in (FreeGen F3()) . s holds ex z being set st ( z in the Sorts of F2() . s & S2[y,z] ) proof let y be set ; ::_thesis: ( y in (FreeGen F3()) . s implies ex z being set st ( z in the Sorts of F2() . s & S2[y,z] ) ) assume y in (FreeGen F3()) . s ; ::_thesis: ex z being set st ( z in the Sorts of F2() . s & S2[y,z] ) then consider a being set such that A5: a in F3() . s and A6: y = root-tree [a,s] by A3, MSAFREE:def_15; reconsider a = a as Element of F3() . s by A5; take z = F4(a,s); ::_thesis: ( z in the Sorts of F2() . s & S2[y,z] ) thus z in the Sorts of F2() . s by A1; ::_thesis: S2[y,z] take a ; ::_thesis: ( y = root-tree [a,s] & z = F4(a,s) ) thus ( y = root-tree [a,s] & z = F4(a,s) ) by A6; ::_thesis: verum end; consider f being Function such that A7: ( dom f = (FreeGen F3()) . s & rng f c= the Sorts of F2() . s ) and A8: for y being set st y in (FreeGen F3()) . s holds S2[y,f . y] from FUNCT_1:sch_5(A4); reconsider f = f as Function of ((FreeGen F3()) . a),( the Sorts of F2() . a) by A7, FUNCT_2:2; take y = f; ::_thesis: S1[a,y] take f ; ::_thesis: ( y = f & ( for x being Element of F3() . a holds f . (root-tree [x,a]) = F4(x,a) ) ) thus y = f ; ::_thesis: for x being Element of F3() . a holds f . (root-tree [x,a]) = F4(x,a) let x be Element of F3() . a; ::_thesis: f . (root-tree [x,a]) = F4(x,a) root-tree [x,s] in (FreeGen F3()) . s by A3, MSAFREE:def_15; then consider z being Element of F3() . s such that A9: root-tree [x,s] = root-tree [z,s] and A10: f . (root-tree [x,s]) = F4(z,s) by A8; [x,s] = [z,s] by A9, TREES_4:4; hence f . (root-tree [x,a]) = F4(x,a) by A10, XTUPLE_0:1; ::_thesis: verum end; consider h being Function such that A11: dom h = the carrier of F1() and A12: for a being set st a in the carrier of F1() holds S1[a,h . a] from CLASSES1:sch_1(A2); reconsider h = h as ManySortedSet of the carrier of F1() by A11, PARTFUN1:def_2, RELAT_1:def_18; h is ManySortedFunction of FreeGen F3(), the Sorts of F2() proof let a be set ; :: according to PBOOLE:def_15 ::_thesis: ( not a in the carrier of F1() or h . a is Element of bool [:((FreeGen F3()) . a),( the Sorts of F2() . a):] ) assume a in the carrier of F1() ; ::_thesis: h . a is Element of bool [:((FreeGen F3()) . a),( the Sorts of F2() . a):] then ex f being Function of ((FreeGen F3()) . a),( the Sorts of F2() . a) st ( h . a = f & ( for x being Element of F3() . a holds f . (root-tree [x,a]) = F4(x,a) ) ) by A12; hence h . a is Element of bool [:((FreeGen F3()) . a),( the Sorts of F2() . a):] ; ::_thesis: verum end; then reconsider h = h as ManySortedFunction of FreeGen F3(), the Sorts of F2() ; consider H being ManySortedFunction of (FreeMSA F3()),F2() such that A13: H is_homomorphism FreeMSA F3(),F2() and A14: H || (FreeGen F3()) = h by MSAFREE:def_5; take H ; ::_thesis: ( H is_homomorphism FreeMSA F3(),F2() & ( for s being SortSymbol of F1() for x being Element of F3() . s holds (H . s) . (root-tree [x,s]) = F4(x,s) ) ) thus H is_homomorphism FreeMSA F3(),F2() by A13; ::_thesis: for s being SortSymbol of F1() for x being Element of F3() . s holds (H . s) . (root-tree [x,s]) = F4(x,s) let s be SortSymbol of F1(); ::_thesis: for x being Element of F3() . s holds (H . s) . (root-tree [x,s]) = F4(x,s) let x be Element of F3() . s; ::_thesis: (H . s) . (root-tree [x,s]) = F4(x,s) A15: ex f being Function of ((FreeGen F3()) . s),( the Sorts of F2() . s) st ( h . s = f & ( for x being Element of F3() . s holds f . (root-tree [x,s]) = F4(x,s) ) ) by A12; reconsider t = root-tree [x,s] as Term of F1(),F3() by MSATERM:4; (FreeGen F3()) . s = FreeGen (s,F3()) by MSAFREE:def_16; then A16: t in (FreeGen F3()) . s by MSAFREE:def_15; h . s = (H . s) | ((FreeGen F3()) . s) by A14, MSAFREE:def_1; then (H . s) . (root-tree [x,s]) = (h . s) . (root-tree [x,s]) by A16, FUNCT_1:49; hence (H . s) . (root-tree [x,s]) = F4(x,s) by A15; ::_thesis: verum end; theorem Th39: :: INSTALG1:39 for I being set for A, B being ManySortedSet of I for C being ManySortedSubset of A for F being ManySortedFunction of A,B for i being set st i in I holds for f, g being Function st f = F . i & g = (F || C) . i holds for x being set st x in C . i holds g . x = f . x proof let I be set ; ::_thesis: for A, B being ManySortedSet of I for C being ManySortedSubset of A for F being ManySortedFunction of A,B for i being set st i in I holds for f, g being Function st f = F . i & g = (F || C) . i holds for x being set st x in C . i holds g . x = f . x let A, B be ManySortedSet of I; ::_thesis: for C being ManySortedSubset of A for F being ManySortedFunction of A,B for i being set st i in I holds for f, g being Function st f = F . i & g = (F || C) . i holds for x being set st x in C . i holds g . x = f . x let C be ManySortedSubset of A; ::_thesis: for F being ManySortedFunction of A,B for i being set st i in I holds for f, g being Function st f = F . i & g = (F || C) . i holds for x being set st x in C . i holds g . x = f . x let F be ManySortedFunction of A,B; ::_thesis: for i being set st i in I holds for f, g being Function st f = F . i & g = (F || C) . i holds for x being set st x in C . i holds g . x = f . x let i be set ; ::_thesis: ( i in I implies for f, g being Function st f = F . i & g = (F || C) . i holds for x being set st x in C . i holds g . x = f . x ) assume A1: i in I ; ::_thesis: for f, g being Function st f = F . i & g = (F || C) . i holds for x being set st x in C . i holds g . x = f . x then reconsider Fi = F . i as Function of (A . i),(B . i) by PBOOLE:def_15; let f, g be Function; ::_thesis: ( f = F . i & g = (F || C) . i implies for x being set st x in C . i holds g . x = f . x ) assume that A2: f = F . i and A3: g = (F || C) . i ; ::_thesis: for x being set st x in C . i holds g . x = f . x let x be set ; ::_thesis: ( x in C . i implies g . x = f . x ) g = Fi | (C . i) by A1, A3, MSAFREE:def_1; hence ( x in C . i implies g . x = f . x ) by A2, FUNCT_1:49; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let X be V16() ManySortedSet of the carrier of S; cluster FreeGen X -> V16() ; coherence FreeGen X is non-empty ; end; definition let S1, S2 be non empty non void ManySortedSign ; let X be V16() ManySortedSet of the carrier of S2; let f be Function of the carrier of S1, the carrier of S2; let g be Function; assume B1: f,g form_morphism_between S1,S2 ; func hom (f,g,X,S1,S2) -> ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) means :Def5: :: INSTALG1:def 5 ( it is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (it . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ); existence ex b1 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st ( b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) proof set A = (FreeMSA X) | (S1,f,g); the Sorts of ((FreeMSA X) | (S1,f,g)) = the Sorts of (FreeMSA X) * f by B1, Def3; then reconsider A = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra over S1 by MSUALG_1:def_3; deffunc H1( set , set ) -> set = root-tree [$1,(f . $2)]; A1: now__::_thesis:_for_s_being_SortSymbol_of_S1 for_x_being_Element_of_(X_*_f)_._s_holds_H1(x,s)_in_the_Sorts_of_A_._s let s be SortSymbol of S1; ::_thesis: for x being Element of (X * f) . s holds H1(x,s) in the Sorts of A . s let x be Element of (X * f) . s; ::_thesis: H1(x,s) in the Sorts of A . s reconsider fs = f . s as SortSymbol of S2 ; reconsider y = x as Element of X . fs by FUNCT_2:15; reconsider t = root-tree [y,fs] as Term of S2,X by MSATERM:4; the_sort_of t = fs by MSATERM:14; then t in FreeSort (X,fs) by MSATERM:def_5; then A2: t in (FreeSort X) . fs by MSAFREE:def_11; ( FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) & the Sorts of A = the Sorts of (FreeMSA X) * f ) by B1, Def3, MSAFREE:def_14; hence H1(x,s) in the Sorts of A . s by A2, FUNCT_2:15; ::_thesis: verum end; consider H being ManySortedFunction of (FreeMSA (X * f)),A such that A3: ( H is_homomorphism FreeMSA (X * f),A & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (H . s) . (root-tree [x,s]) = H1(x,s) ) ) from INSTALG1:sch_1(A1); reconsider G = H as ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) ; take G ; ::_thesis: ( G is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (G . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) thus ( G is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (G . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & b2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (b2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) holds b1 = b2 proof reconsider A1 = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra over S1 by B1, Th22; let G1, G2 be ManySortedFunction of the Sorts of (FreeMSA (X * f)), the Sorts of ((FreeMSA X) | (S1,f,g)); ::_thesis: ( G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) implies G1 = G2 ) assume that A4: G1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and A5: for s being SortSymbol of S1 for x being Element of (X * f) . s holds (G1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] and A6: G2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) and A7: for s being SortSymbol of S1 for x being Element of (X * f) . s holds (G2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ; ::_thesis: G1 = G2 set H1 = G1; set H2 = G2; A8: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_S1_holds_ (G1_||_(FreeGen_(X_*_f)))_._x_=_(G2_||_(FreeGen_(X_*_f)))_._x let x be set ; ::_thesis: ( x in the carrier of S1 implies (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x ) assume x in the carrier of S1 ; ::_thesis: (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x then reconsider s = x as SortSymbol of S1 ; reconsider g1 = (G1 || (FreeGen (X * f))) . s, g2 = (G2 || (FreeGen (X * f))) . s as Function of ((FreeGen (X * f)) . s),( the Sorts of A1 . s) ; now__::_thesis:_for_z_being_Element_of_(FreeGen_(X_*_f))_._s_holds_g1_._z_=_g2_._z let z be Element of (FreeGen (X * f)) . s; ::_thesis: g1 . z = g2 . z FreeGen (s,(X * f)) = (FreeGen (X * f)) . s by MSAFREE:def_16; then consider a being set such that A9: a in (X * f) . s and A10: z = root-tree [a,s] by MSAFREE:def_15; reconsider a = a as Element of (X * f) . s by A9; thus g1 . z = (G1 . s) . z by Th39 .= root-tree [a,(f . s)] by A5, A10 .= (G2 . s) . z by A7, A10 .= g2 . z by Th39 ; ::_thesis: verum end; hence (G1 || (FreeGen (X * f))) . x = (G2 || (FreeGen (X * f))) . x by FUNCT_2:63; ::_thesis: verum end; A1 = (FreeMSA X) | (S1,f,g) ; hence G1 = G2 by A4, A6, A8, EXTENS_1:14, PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def5 defines hom INSTALG1:def_5_:_ for S1, S2 being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S2 for f being Function of the carrier of S1, the carrier of S2 for g being Function st f,g form_morphism_between S1,S2 holds for b6 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) holds ( b6 = hom (f,g,X,S1,S2) iff ( b6 is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) & ( for s being SortSymbol of S1 for x being Element of (X * f) . s holds (b6 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) ); theorem Th40: :: INSTALG1:40 for S1, S2 being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S2 for f being Function of the carrier of S1, the carrier of S2 for g being Function st f,g form_morphism_between S1,S2 holds for o being OperSymbol of S1 for p being Element of Args (o,(FreeMSA (X * f))) for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q proof let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S2 for f being Function of the carrier of S1, the carrier of S2 for g being Function st f,g form_morphism_between S1,S2 holds for o being OperSymbol of S1 for p being Element of Args (o,(FreeMSA (X * f))) for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q let X be V16() ManySortedSet of the carrier of S2; ::_thesis: for f being Function of the carrier of S1, the carrier of S2 for g being Function st f,g form_morphism_between S1,S2 holds for o being OperSymbol of S1 for p being Element of Args (o,(FreeMSA (X * f))) for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q let f be Function of the carrier of S1, the carrier of S2; ::_thesis: for g being Function st f,g form_morphism_between S1,S2 holds for o being OperSymbol of S1 for p being Element of Args (o,(FreeMSA (X * f))) for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q let g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for o being OperSymbol of S1 for p being Element of Args (o,(FreeMSA (X * f))) for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q ) set F = hom (f,g,X,S1,S2); assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for o being OperSymbol of S1 for p being Element of Args (o,(FreeMSA (X * f))) for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q then reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9; let o be OperSymbol of S1; ::_thesis: for p being Element of Args (o,(FreeMSA (X * f))) for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q let p be Element of Args (o,(FreeMSA (X * f))); ::_thesis: for q being FinSequence st q = (hom (f,g,X,S1,S2)) # p holds ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q let q be FinSequence; ::_thesis: ( q = (hom (f,g,X,S1,S2)) # p implies ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q ) assume A2: q = (hom (f,g,X,S1,S2)) # p ; ::_thesis: ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = [(g . o), the carrier of S2] -tree q then A3: q is Element of Args ((h . o),(FreeMSA X)) by A1, Th24; hom (f,g,X,S1,S2) is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) by A1, Def5; then ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ((Den (o,(FreeMSA (X * f)))) . p) = (Den (o,((FreeMSA X) | (S1,f,g)))) . q by A2, MSUALG_3:def_7; hence ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree p) = (Den (o,((FreeMSA X) | (S1,f,g)))) . q by Th3 .= (Den ((h . o),(FreeMSA X))) . q by A1, Th23 .= [(g . o), the carrier of S2] -tree q by A3, Th3 ; ::_thesis: verum end; theorem Th41: :: INSTALG1:41 for S1, S2 being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S2 for f being Function of the carrier of S1, the carrier of S2 for g being Function st f,g form_morphism_between S1,S2 holds for t being Term of S1,(X * f) holds ( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f ) proof let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S2 for f being Function of the carrier of S1, the carrier of S2 for g being Function st f,g form_morphism_between S1,S2 holds for t being Term of S1,(X * f) holds ( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f ) let X be V16() ManySortedSet of the carrier of S2; ::_thesis: for f being Function of the carrier of S1, the carrier of S2 for g being Function st f,g form_morphism_between S1,S2 holds for t being Term of S1,(X * f) holds ( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f ) let f be Function of the carrier of S1, the carrier of S2; ::_thesis: for g being Function st f,g form_morphism_between S1,S2 holds for t being Term of S1,(X * f) holds ( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f ) let g be Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies for t being Term of S1,(X * f) holds ( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f ) ) assume A1: f,g form_morphism_between S1,S2 ; ::_thesis: for t being Term of S1,(X * f) holds ( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f ) then reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9; let t be Term of S1,(X * f); ::_thesis: ( ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X iff t is CompoundTerm of S1,X * f ) hereby ::_thesis: ( t is CompoundTerm of S1,X * f implies ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X ) assume ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X ; ::_thesis: t is CompoundTerm of S1,X * f then reconsider w = ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t as CompoundTerm of S2,X ; assume t is not CompoundTerm of S1,X * f ; ::_thesis: contradiction then not t . {} in [: the carrier' of S1,{ the carrier of S1}:] by MSATERM:def_6; then consider s being SortSymbol of S1, v being Element of (X * f) . s such that A2: t . {} = [v,s] by MSATERM:2; t = root-tree [v,s] by A2, MSATERM:5; then ( ((hom (f,g,X,S1,S2)) . s) . t = root-tree [v,(f . s)] & the_sort_of t = s ) by A1, Def5, MSATERM:14; then ( w . {} in [: the carrier' of S2,{ the carrier of S2}:] & w . {} = [v,(f . s)] ) by MSATERM:def_6, TREES_4:3; then A3: f . s = the carrier of S2 by ZFMISC_1:106; f . s in the carrier of S2 ; hence contradiction by A3; ::_thesis: verum end; assume t is CompoundTerm of S1,X * f ; ::_thesis: ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X then reconsider t = t as CompoundTerm of S1,X * f ; t . {} in [: the carrier' of S1,{ the carrier of S1}:] by MSATERM:def_6; then consider o, r being set such that A4: o in the carrier' of S1 and A5: r in { the carrier of S1} and A6: t . {} = [o,r] by ZFMISC_1:def_2; reconsider o = o as OperSymbol of S1 by A4; r = the carrier of S1 by A5, TARSKI:def_1; then consider a being ArgumentSeq of Sym (o,(X * f)) such that A7: t = [o, the carrier of S1] -tree a by A6, MSATERM:10; reconsider a = a as Element of Args (o,(FreeMSA (X * f))) by Th1; reconsider b = (hom (f,g,X,S1,S2)) # a as Element of Args ((h . o),(FreeMSA X)) by A1, Th24; A8: ((hom (f,g,X,S1,S2)) . (the_result_sort_of o)) . ([o, the carrier of S1] -tree a) = [(g . o), the carrier of S2] -tree b by A1, Th40; t . {} = [o, the carrier of S1] by A7, TREES_4:def_4; then A9: the_sort_of t = the_result_sort_of o by MSATERM:17; reconsider b = b as ArgumentSeq of Sym ((h . o),X) by Th1; (Sym ((h . o),X)) -tree b = [(h . o), the carrier of S2] -tree b by MSAFREE:def_9; then reconsider T = [(h . o), the carrier of S2] -tree b as Term of S2,X ; ( T . {} = [(g . o), the carrier of S2] & [(h . o), the carrier of S2] in [: the carrier' of S2,{ the carrier of S2}:] ) by TREES_4:def_4, ZFMISC_1:106; hence ((hom (f,g,X,S1,S2)) . (the_sort_of t)) . t is CompoundTerm of S2,X by A7, A9, A8, MSATERM:def_6; ::_thesis: verum end; theorem :: INSTALG1:42 for S1, S2 being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S2 for f being Function of the carrier of S1, the carrier of S2 for g being one-to-one Function st f,g form_morphism_between S1,S2 holds hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) proof let S1, S2 be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S2 for f being Function of the carrier of S1, the carrier of S2 for g being one-to-one Function st f,g form_morphism_between S1,S2 holds hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) let X be V16() ManySortedSet of the carrier of S2; ::_thesis: for f being Function of the carrier of S1, the carrier of S2 for g being one-to-one Function st f,g form_morphism_between S1,S2 holds hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) let f be Function of the carrier of S1, the carrier of S2; ::_thesis: for g being one-to-one Function st f,g form_morphism_between S1,S2 holds hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) let g be one-to-one Function; ::_thesis: ( f,g form_morphism_between S1,S2 implies hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) ) set A = (FreeMSA X) | (S1,f,g); set H = hom (f,g,X,S1,S2); defpred S1[ set ] means ex t1 being Term of S1,(X * f) st ( t1 = $1 & ( for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds t1 = t2 ) ); A1: FreeMSA (X * f) = MSAlgebra(# (FreeSort (X * f)),(FreeOper (X * f)) #) by MSAFREE:def_14; assume A2: f,g form_morphism_between S1,S2 ; ::_thesis: hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) then reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9; reconsider B = (FreeMSA X) | (S1,f,g) as non-empty MSAlgebra over S1 by A2, Th22; reconsider H9 = hom (f,g,X,S1,S2) as ManySortedFunction of (FreeMSA (X * f)),B ; A3: for o being OperSymbol of S1 for p being ArgumentSeq of Sym (o,(X * f)) st ( for t being Term of S1,(X * f) st t in rng p holds S1[t] ) holds S1[[o, the carrier of S1] -tree p] proof let o be OperSymbol of S1; ::_thesis: for p being ArgumentSeq of Sym (o,(X * f)) st ( for t being Term of S1,(X * f) st t in rng p holds S1[t] ) holds S1[[o, the carrier of S1] -tree p] let p be ArgumentSeq of Sym (o,(X * f)); ::_thesis: ( ( for t being Term of S1,(X * f) st t in rng p holds S1[t] ) implies S1[[o, the carrier of S1] -tree p] ) assume A4: for t being Term of S1,(X * f) st t in rng p holds S1[t] ; ::_thesis: S1[[o, the carrier of S1] -tree p] A5: dom p = dom (the_arity_of o) by MSATERM:22; reconsider a = p as Element of Args (o,(FreeMSA (X * f))) by Th1; A6: [(h . o), the carrier of S2] in [: the carrier' of S2,{ the carrier of S2}:] by ZFMISC_1:106; reconsider q = (hom (f,g,X,S1,S2)) # a as Element of Args ((h . o),(FreeMSA X)) by A2, Th24; take t1 = (Sym (o,(X * f))) -tree p; ::_thesis: ( t1 = [o, the carrier of S1] -tree p & ( for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds t1 = t2 ) ) thus A7: t1 = [o, the carrier of S1] -tree p by MSAFREE:def_9; ::_thesis: for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds t1 = t2 reconsider b = q as ArgumentSeq of Sym ((h . o),X) by Th1; let t2 be Term of S1,(X * f); ::_thesis: ( the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 implies t1 = t2 ) assume A8: ( the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 ) ; ::_thesis: t1 = t2 the_sort_of t1 = the_result_sort_of o by MSATERM:20; then A9: ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = [(g . o), the carrier of S2] -tree q by A2, A7, Th40; ( ((Sym ((h . o),X)) -tree b) . {} = Sym ((h . o),X) & Sym ((h . o),X) = [(h . o), the carrier of S2] ) by MSAFREE:def_9, TREES_4:def_4; then [(h . o), the carrier of S2] -tree b is CompoundTerm of S2,X by A6, MSATERM:def_6; then t2 is CompoundTerm of S1,X * f by A2, A8, A9, Th41; then t2 . {} in [: the carrier' of S1,{ the carrier of S1}:] by MSATERM:def_6; then consider o9, s9 being set such that A10: o9 in the carrier' of S1 and A11: ( s9 in { the carrier of S1} & t2 . {} = [o9,s9] ) by ZFMISC_1:def_2; reconsider o9 = o9 as OperSymbol of S1 by A10; A12: t2 . {} = [o9, the carrier of S1] by A11, TARSKI:def_1; then consider r being ArgumentSeq of Sym (o9,(X * f)) such that A13: t2 = [o9, the carrier of S1] -tree r by MSATERM:10; reconsider c = r as Element of Args (o9,(FreeMSA (X * f))) by Th1; reconsider R = (hom (f,g,X,S1,S2)) # c as Element of Args ((h . o9),(FreeMSA X)) by A2, Th24; the_result_sort_of o9 = the_sort_of t2 by A12, MSATERM:17; then A14: ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = [(g . o9), the carrier of S2] -tree R by A2, A8, A13, Th40; then [(g . o9), the carrier of S2] = [(g . o), the carrier of S2] by A9, TREES_4:15; then h . o = h . o9 by XTUPLE_0:1; then A15: o = o9 by FUNCT_2:19; then A16: dom r = dom (the_arity_of o) by MSATERM:22; A17: q = R by A9, A14, TREES_4:15; now__::_thesis:_for_i_being_Nat_st_i_in_dom_(the_arity_of_o)_holds_ p_._i_=_r_._i let i be Nat; ::_thesis: ( i in dom (the_arity_of o) implies p . i = r . i ) A18: R = H9 # c ; assume A19: i in dom (the_arity_of o) ; ::_thesis: p . i = r . i then reconsider w1 = p . i, w2 = r . i as Term of S1,(X * f) by A5, A16, MSATERM:22; A20: the_sort_of w1 = (the_arity_of o) /. i by A5, A19, MSATERM:23; q = H9 # a ; then q . i = ((hom (f,g,X,S1,S2)) . (the_sort_of w1)) . w1 by A5, A19, A20, MSUALG_3:def_6; then A21: ((hom (f,g,X,S1,S2)) . (the_sort_of w1)) . w1 = ((hom (f,g,X,S1,S2)) . (the_sort_of w1)) . w2 by A17, A15, A16, A19, A20, A18, MSUALG_3:def_6; w1 in rng p by A5, A19, FUNCT_1:def_3; then A22: S1[w1] by A4; the_sort_of w2 = (the_arity_of o) /. i by A15, A16, A19, MSATERM:23; hence p . i = r . i by A22, A20, A21; ::_thesis: verum end; hence t1 = t2 by A7, A13, A15, A5, A16, FINSEQ_1:13; ::_thesis: verum end; thus hom (f,g,X,S1,S2) is_homomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g) by A2, Def5; :: according to MSUALG_3:def_9 ::_thesis: hom (f,g,X,S1,S2) is "1-1" let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for b1 being set holds ( not i in dom (hom (f,g,X,S1,S2)) or not (hom (f,g,X,S1,S2)) . i = b1 or b1 is one-to-one ) let h be Function; ::_thesis: ( not i in dom (hom (f,g,X,S1,S2)) or not (hom (f,g,X,S1,S2)) . i = h or h is one-to-one ) assume i in dom (hom (f,g,X,S1,S2)) ; ::_thesis: ( not (hom (f,g,X,S1,S2)) . i = h or h is one-to-one ) then reconsider s = i as SortSymbol of S1 by PARTFUN1:def_2; assume A23: (hom (f,g,X,S1,S2)) . i = h ; ::_thesis: h is one-to-one then A24: dom h = dom (H9 . s) .= (FreeSort (X * f)) . s by A1, FUNCT_2:def_1 .= FreeSort ((X * f),s) by MSAFREE:def_11 ; let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in dom h or not y in dom h or not h . x = h . y or x = y ) assume A25: ( x in dom h & y in dom h ) ; ::_thesis: ( not h . x = h . y or x = y ) FreeSort ((X * f),s) c= S1 -Terms (X * f) by MSATERM:12; then reconsider t1 = x, t2 = y as Term of S1,(X * f) by A24, A25; A26: for s being SortSymbol of S1 for v being Element of (X * f) . s holds S1[ root-tree [v,s]] proof let s be SortSymbol of S1; ::_thesis: for v being Element of (X * f) . s holds S1[ root-tree [v,s]] let v be Element of (X * f) . s; ::_thesis: S1[ root-tree [v,s]] reconsider t1 = root-tree [v,s] as Term of S1,(X * f) by MSATERM:4; take t1 ; ::_thesis: ( t1 = root-tree [v,s] & ( for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds t1 = t2 ) ) thus t1 = root-tree [v,s] ; ::_thesis: for t2 being Term of S1,(X * f) st the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 holds t1 = t2 let t2 be Term of S1,(X * f); ::_thesis: ( the_sort_of t1 = the_sort_of t2 & ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 implies t1 = t2 ) assume that A27: the_sort_of t1 = the_sort_of t2 and A28: ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t1 = ((hom (f,g,X,S1,S2)) . (the_sort_of t1)) . t2 ; ::_thesis: t1 = t2 A29: the_sort_of t1 = s by MSATERM:14; A30: ((hom (f,g,X,S1,S2)) . s) . (root-tree [v,s]) = root-tree [v,(f . s)] by A2, Def5; now__::_thesis:_not_t2_._{}_in_[:_the_carrier'_of_S1,{_the_carrier_of_S1}:] assume t2 . {} in [: the carrier' of S1,{ the carrier of S1}:] ; ::_thesis: contradiction then t2 is CompoundTerm of S1,X * f by MSATERM:def_6; then ( (root-tree [v,(f . s)]) . {} = [v,(f . s)] & root-tree [v,(f . s)] is CompoundTerm of S2,X ) by A2, A27, A28, A30, A29, Th41, TREES_4:3; then [v,(f . s)] in [: the carrier' of S2,{ the carrier of S2}:] by MSATERM:def_6; then A31: f . s = the carrier of S2 by ZFMISC_1:106; f . s in the carrier of S2 ; hence contradiction by A31; ::_thesis: verum end; then consider s2 being SortSymbol of S1, v2 being Element of (X * f) . s2 such that A32: t2 . {} = [v2,s2] by MSATERM:2; A33: t2 = root-tree [v2,s2] by A32, MSATERM:5; then A34: s = s2 by A27, A29, MSATERM:14; then ((hom (f,g,X,S1,S2)) . s) . t2 = root-tree [v2,(f . s)] by A2, A33, Def5; then [v,(f . s)] = [v2,(f . s)] by A28, A30, A29, TREES_4:4; hence t1 = t2 by A33, A34, XTUPLE_0:1; ::_thesis: verum end; for t being Term of S1,(X * f) holds S1[t] from MSATERM:sch_1(A26, A3); then A35: S1[t1] ; ( the_sort_of t1 = s & the_sort_of t2 = s ) by A24, A25, MSATERM:def_5; hence ( not h . x = h . y or x = y ) by A23, A35; ::_thesis: verum end; theorem :: INSTALG1:43 for S being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S holds hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X) proof let S be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S holds hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X) let X be V16() ManySortedSet of the carrier of S; ::_thesis: hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X) set f = id the carrier of S; set h = hom ((id the carrier of S),(id the carrier' of S),X,S,S); set I = id the Sorts of (FreeMSA X); set g = id the carrier' of S; A1: id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:28; dom X = the carrier of S by PARTFUN1:def_2; then A2: X * (id the carrier of S) = X by RELAT_1:52; A3: (FreeMSA X) | (S,(id the carrier of S),(id the carrier' of S)) = FreeMSA X by Th25; A4: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_ ((id_the_Sorts_of_(FreeMSA_X))_||_(FreeGen_X))_._i_=_((hom_((id_the_carrier_of_S),(id_the_carrier'_of_S),X,S,S))_||_(FreeGen_(X_*_(id_the_carrier_of_S))))_._i let i be set ; ::_thesis: ( i in the carrier of S implies ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i ) assume i in the carrier of S ; ::_thesis: ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i then reconsider s = i as SortSymbol of S ; FreeGen X c= the Sorts of (FreeMSA X) by PBOOLE:def_18; then A5: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s by PBOOLE:def_2; then ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) is Function of ((FreeGen X) . s),( the Sorts of (FreeMSA X) . s) by FUNCT_2:32; then A6: dom (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def_1; A7: now__::_thesis:_for_a_being_set_st_a_in_(FreeGen_X)_._s_holds_ (((id_the_Sorts_of_(FreeMSA_X))_._s)_|_((FreeGen_X)_._s))_._a_=_(((hom_((id_the_carrier_of_S),(id_the_carrier'_of_S),X,S,S))_._s)_|_((FreeGen_X)_._s))_._a let a be set ; ::_thesis: ( a in (FreeGen X) . s implies (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a ) assume A8: a in (FreeGen X) . s ; ::_thesis: (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a then reconsider b = a as Element of (FreeMSA X),s by A5; b in FreeGen (s,X) by A8, MSAFREE:def_16; then consider x being set such that A9: x in X . s and A10: b = root-tree [x,s] by MSAFREE:def_15; thus (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = ((id the Sorts of (FreeMSA X)) . s) . b by A8, FUNCT_1:49 .= (id ( the Sorts of (FreeMSA X) . s)) . b by MSUALG_3:def_1 .= b by FUNCT_1:18 .= root-tree [x,((id the carrier of S) . s)] by A10, FUNCT_1:18 .= ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) . b by A1, A2, A9, A10, Def5 .= (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a by A8, FUNCT_1:49 ; ::_thesis: verum end; ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s) is Function of ((FreeGen X) . s),( the Sorts of (FreeMSA X) . s) by A2, A3, A5, FUNCT_2:32; then A11: dom (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def_1; ( ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . s = ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) & ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . s = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen (X * (id the carrier of S))) . s) ) by MSAFREE:def_1; hence ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i by A2, A6, A11, A7, FUNCT_1:2; ::_thesis: verum end; ( id the Sorts of (FreeMSA X) is_homomorphism FreeMSA X, FreeMSA X & hom ((id the carrier of S),(id the carrier' of S),X,S,S) is_homomorphism FreeMSA (X * (id the carrier of S)),(FreeMSA X) | (S,(id the carrier of S),(id the carrier' of S)) ) by A1, Def5, MSUALG_3:9; hence hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X) by A2, A3, A4, EXTENS_1:19, PBOOLE:3; ::_thesis: verum end; theorem :: INSTALG1:44 for S1, S2, S3 being non empty non void ManySortedSign for X being V16() ManySortedSet of the carrier of S3 for f1 being Function of the carrier of S1, the carrier of S2 for g1 being Function st f1,g1 form_morphism_between S1,S2 holds for f2 being Function of the carrier of S2, the carrier of S3 for g2 being Function st f2,g2 form_morphism_between S2,S3 holds hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) proof let S1, S2, S3 be non empty non void ManySortedSign ; ::_thesis: for X being V16() ManySortedSet of the carrier of S3 for f1 being Function of the carrier of S1, the carrier of S2 for g1 being Function st f1,g1 form_morphism_between S1,S2 holds for f2 being Function of the carrier of S2, the carrier of S3 for g2 being Function st f2,g2 form_morphism_between S2,S3 holds hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) let X be V16() ManySortedSet of the carrier of S3; ::_thesis: for f1 being Function of the carrier of S1, the carrier of S2 for g1 being Function st f1,g1 form_morphism_between S1,S2 holds for f2 being Function of the carrier of S2, the carrier of S3 for g2 being Function st f2,g2 form_morphism_between S2,S3 holds hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) let f1 be Function of the carrier of S1, the carrier of S2; ::_thesis: for g1 being Function st f1,g1 form_morphism_between S1,S2 holds for f2 being Function of the carrier of S2, the carrier of S3 for g2 being Function st f2,g2 form_morphism_between S2,S3 holds hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) let g1 be Function; ::_thesis: ( f1,g1 form_morphism_between S1,S2 implies for f2 being Function of the carrier of S2, the carrier of S3 for g2 being Function st f2,g2 form_morphism_between S2,S3 holds hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) ) assume A1: f1,g1 form_morphism_between S1,S2 ; ::_thesis: for f2 being Function of the carrier of S2, the carrier of S3 for g2 being Function st f2,g2 form_morphism_between S2,S3 holds hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) let f2 be Function of the carrier of S2, the carrier of S3; ::_thesis: for g2 being Function st f2,g2 form_morphism_between S2,S3 holds hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) let g2 be Function; ::_thesis: ( f2,g2 form_morphism_between S2,S3 implies hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) ) set f = f2 * f1; set g = g2 * g1; assume A2: f2,g2 form_morphism_between S2,S3 ; ::_thesis: hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) then reconsider Af = (FreeMSA X) | (S1,(f2 * f1),(g2 * g1)), Af1 = (FreeMSA (X * f2)) | (S1,f1,g1) as non-empty MSAlgebra over S1 by A1, Th22, PUA2MSS1:29; A3: hom (f2,g2,X,S2,S3) is_homomorphism FreeMSA (X * f2),(FreeMSA X) | (S2,f2,g2) by A2, Def5; A4: the Sorts of (FreeMSA (X * f2)) is_transformable_to the Sorts of ((FreeMSA X) | (S2,f2,g2)) proof let i be set ; :: according to PZFMISC1:def_3 ::_thesis: ( not i in the carrier of S2 or not the Sorts of ((FreeMSA X) | (S2,f2,g2)) . i = {} or the Sorts of (FreeMSA (X * f2)) . i = {} ) assume i in the carrier of S2 ; ::_thesis: ( not the Sorts of ((FreeMSA X) | (S2,f2,g2)) . i = {} or the Sorts of (FreeMSA (X * f2)) . i = {} ) then reconsider s = i as SortSymbol of S2 ; the Sorts of ((FreeMSA X) | (S2,f2,g2)) . s = ( the Sorts of (FreeMSA X) * f2) . s by A2, Def3; hence ( not the Sorts of ((FreeMSA X) | (S2,f2,g2)) . i = {} or the Sorts of (FreeMSA (X * f2)) . i = {} ) ; ::_thesis: verum end; (FreeMSA X) | (S1,(f2 * f1),(g2 * g1)) = ((FreeMSA X) | (S2,f2,g2)) | (S1,f1,g1) by A1, A2, Th27; then consider hf1 being ManySortedFunction of Af1,Af such that A5: hf1 = (hom (f2,g2,X,S2,S3)) * f1 and A6: hf1 is_homomorphism Af1,Af by A1, A3, A4, Th34; reconsider hh = hom (f1,g1,(X * f2),S1,S2) as ManySortedFunction of (FreeMSA (X * (f2 * f1))),Af1 by RELAT_1:36; reconsider hf1h = hf1 ** hh as ManySortedFunction of (FreeMSA (X * (f2 * f1))),((FreeMSA X) | (S1,(f2 * f1),(g2 * g1))) ; A7: X * (f2 * f1) = (X * f2) * f1 by RELAT_1:36; A8: now__::_thesis:_for_s_being_SortSymbol_of_S1 for_x_being_Element_of_(X_*_(f2_*_f1))_._s_holds_(hf1h_._s)_._(root-tree_[x,s])_=_root-tree_[x,((f2_*_f1)_._s)] let s be SortSymbol of S1; ::_thesis: for x being Element of (X * (f2 * f1)) . s holds (hf1h . s) . (root-tree [x,s]) = root-tree [x,((f2 * f1) . s)] let x be Element of (X * (f2 * f1)) . s; ::_thesis: (hf1h . s) . (root-tree [x,s]) = root-tree [x,((f2 * f1) . s)] reconsider t = root-tree [x,s] as Term of S1,(X * (f2 * f1)) by MSATERM:4; A9: FreeMSA (X * (f2 * f1)) = MSAlgebra(# (FreeSort (X * (f2 * f1))),(FreeOper (X * (f2 * f1))) #) by MSAFREE:def_14; ( the_sort_of t = s & (FreeSort (X * (f2 * f1))) . s = FreeSort ((X * (f2 * f1)),s) ) by MSAFREE:def_11, MSATERM:14; then A10: root-tree [x,s] in the Sorts of (FreeMSA (X * (f2 * f1))) . s by A9, MSATERM:def_5; A11: (X * (f2 * f1)) . s = (X * f2) . (f1 . s) by A7, FUNCT_2:15; (hf1h . s) . (root-tree [x,s]) = ((hf1 . s) * ((hom (f1,g1,(X * f2),S1,S2)) . s)) . (root-tree [x,s]) by MSUALG_3:2 .= (hf1 . s) . (((hom (f1,g1,(X * f2),S1,S2)) . s) . (root-tree [x,s])) by A7, A10, FUNCT_2:15 .= (hf1 . s) . (root-tree [x,(f1 . s)]) by A1, A7, Def5 ; hence (hf1h . s) . (root-tree [x,s]) = ((hom (f2,g2,X,S2,S3)) . (f1 . s)) . (root-tree [x,(f1 . s)]) by A5, FUNCT_2:15 .= root-tree [x,(f2 . (f1 . s))] by A2, A11, Def5 .= root-tree [x,((f2 * f1) . s)] by FUNCT_2:15 ; ::_thesis: verum end; A12: f2 * f1,g2 * g1 form_morphism_between S1,S3 by A1, A2, PUA2MSS1:29; hom (f1,g1,(X * f2),S1,S2) is_homomorphism FreeMSA ((X * f2) * f1),(FreeMSA (X * f2)) | (S1,f1,g1) by A1, Def5; then hf1 ** hh is_homomorphism FreeMSA (X * (f2 * f1)),Af by A6, A7, MSUALG_3:10; hence hom ((f2 * f1),(g2 * g1),X,S1,S3) = ((hom (f2,g2,X,S2,S3)) * f1) ** (hom (f1,g1,(X * f2),S1,S2)) by A12, A5, A8, Def5; ::_thesis: verum end;