instalg1.miz



    begin

    theorem :: INSTALG1:1

    

     Th1: for S be non empty non void ManySortedSign holds for o be OperSymbol of S holds for V be non-empty ManySortedSet of the carrier of S holds for x be 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;

      let o be OperSymbol of S;

      let V be non-empty ManySortedSet of the carrier of S;

      let x be set;

      

       A1: ( TS ( DTConMSA V)) = (S -Terms V) by MSATERM:def 1;

      

       A2: ( FreeMSA V) = MSAlgebra (# ( FreeSort V), ( FreeOper V) #) by MSAFREE:def 14;

      hereby

        assume x is ArgumentSeq of ( Sym (o,V));

        then

        reconsider p = x as ArgumentSeq of ( Sym (o,V));

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

      end;

      assume x is Element of ( Args (o,( FreeMSA V)));

      then

      reconsider x as Element of ( Args (o,( FreeMSA V)));

      ( rng x) c= ( TS ( DTConMSA V))

      proof

        let y be object;

        assume y in ( rng x);

        then

        consider z be object such that

         A3: z in ( dom x) and

         A4: y = (x . z) by FUNCT_1:def 3;

        reconsider 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 thesis by A5;

      end;

      then

      reconsider x as FinSequence of ( TS ( DTConMSA V)) by FINSEQ_1:def 4;

      ( Sym (o,V)) ==> ( roots x) by A2, MSAFREE: 10;

      hence thesis by A1, MSATERM: 21;

    end;

    registration

      let S be non empty non void ManySortedSign;

      let V be non-empty ManySortedSet of the carrier of S;

      let o be OperSymbol of S;

      cluster -> DTree-yielding for Element of ( Args (o,( FreeMSA V)));

      coherence by Th1;

    end

    theorem :: INSTALG1:2

    

     Th2: for S be non empty non void ManySortedSign holds for A1,A2 be MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for o be OperSymbol of S st ( Args (o,A1)) <> {} holds ( Args (o,A2)) <> {}

    proof

      let S be non void non empty ManySortedSign;

      let A1,A2 be MSAlgebra over S such that

       A1: for i be set st i in the carrier of S & (the Sorts of A2 . i) = {} holds (the Sorts of A1 . i) = {} ;

      let o be OperSymbol of S;

      assume

       A2: ( Args (o,A1)) <> {} ;

      now

        let i be Element of NAT ;

        assume i in ( dom ( the_arity_of o));

        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;

      end;

      hence thesis by MSUALG_6: 3;

    end;

    theorem :: INSTALG1:3

    

     Th3: for S be non empty non void ManySortedSign holds for o be OperSymbol of S holds for V be non-empty ManySortedSet of the carrier of S holds for x be 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;

      let o be OperSymbol of S;

      let V be non-empty ManySortedSet of the carrier of S;

      let x be Element of ( Args (o,( FreeMSA V)));

      

       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 thesis by A1, MSAFREE:def 13;

    end;

    theorem :: INSTALG1:4

    for S be non empty non void ManySortedSign holds for A,B be MSAlgebra over S st the MSAlgebra of A = the MSAlgebra of B holds for o be OperSymbol of S holds ( Den (o,A)) = ( Den (o,B));

    theorem :: INSTALG1:5

    

     Th5: for S be non empty non void ManySortedSign holds for A1,A2,B1,B2 be MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of B1 & the MSAlgebra of A2 = the MSAlgebra of B2 holds for f be ManySortedFunction of A1, A2 holds for g be ManySortedFunction of B1, B2 st f = g holds for o be OperSymbol of S st ( Args (o,A1)) <> {} & ( Args (o,A2)) <> {} holds for x be Element of ( Args (o,A1)) holds for y be Element of ( Args (o,B1)) st x = y holds (f # x) = (g # y)

    proof

      let S be non empty non void ManySortedSign;

      let A1,A2,B1,B2 be MSAlgebra over S such that

       A1: the MSAlgebra of A1 = the MSAlgebra of B1 & the MSAlgebra of A2 = the MSAlgebra of B2;

      let f be ManySortedFunction of A1, A2;

      let g be ManySortedFunction of B1, B2 such that

       A2: f = g;

      let o be OperSymbol of S such that

       A3: ( Args (o,A1)) <> {} & ( Args (o,A2)) <> {} ;

      let x be Element of ( Args (o,A1));

      let y be Element of ( Args (o,B1));

      assume

       A4: x = y;

      (f # x) = (( Frege (f * ( the_arity_of o))) . x) by A3, MSUALG_3:def 5;

      hence thesis by A1, A2, A3, A4, MSUALG_3:def 5;

    end;

    theorem :: INSTALG1:6

    for S be non empty non void ManySortedSign holds for A1,A2,B1,B2 be MSAlgebra over S st the MSAlgebra of A1 = the MSAlgebra of B1 & the MSAlgebra of A2 = the MSAlgebra of B2 & the Sorts of A1 is_transformable_to the Sorts of A2 holds for h be ManySortedFunction of A1, A2 st h is_homomorphism (A1,A2) holds ex h9 be ManySortedFunction of B1, B2 st h9 = h & h9 is_homomorphism (B1,B2)

    proof

      let S be non empty non void ManySortedSign;

      let A1,A2,B1,B2 be MSAlgebra over S such that

       A1: the MSAlgebra of A1 = the MSAlgebra of B1 and

       A2: the MSAlgebra of A2 = the MSAlgebra of B2 and

       A3: the Sorts of A1 is_transformable_to the Sorts of A2;

      let h be ManySortedFunction of A1, A2 such that

       A4: h is_homomorphism (A1,A2);

      reconsider h9 = h as ManySortedFunction of B1, B2 by A1, A2;

      take h9;

      thus h9 = h;

      let o be OperSymbol of S;

      assume

       A5: ( Args (o,B1)) <> {} ;

      then

       A6: ( Args (o,B2)) <> {} by A1, A2, A3, Th2;

      let x be Element of ( Args (o,B1));

      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

      .= (( Den (o,B2)) . (h9 # x)) by A1, A2, A5, A6, Th5;

    end;

    definition

      let S be ManySortedSign;

      :: INSTALG1:def1

      attr S is feasible means

      : Def1: the carrier of S = {} implies the carrier' of S = {} ;

    end

    theorem :: INSTALG1:7

    

     Th7: for S be ManySortedSign holds S is feasible iff ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

    registration

      cluster non empty -> feasible for ManySortedSign;

      coherence ;

      cluster void -> feasible for ManySortedSign;

      coherence ;

      cluster empty feasible -> void for ManySortedSign;

      coherence ;

      cluster non void feasible -> non empty for ManySortedSign;

      coherence ;

    end

    registration

      cluster non void non empty for ManySortedSign;

      existence

      proof

        set S = the non void non empty ManySortedSign;

        take S;

        thus thesis;

      end;

    end

    theorem :: INSTALG1:8

    

     Th8: for S be feasible ManySortedSign holds (( id the carrier of S),( id the carrier' of S)) form_morphism_between (S,S)

    proof

      let S be feasible ManySortedSign;

      per cases ;

        suppose S is void;

        hence thesis by MSALIMIT: 6;

      end;

        suppose S is non void;

        then

        reconsider S as non void feasible ManySortedSign;

        S is non empty;

        hence thesis by PUA2MSS1: 28;

      end;

    end;

    theorem :: INSTALG1:9

    

     Th9: for S1,S2 be ManySortedSign holds for f,g be 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 by FUNCT_2: 2;

    begin

    definition

      let S be feasible ManySortedSign;

      :: INSTALG1:def2

      mode Subsignature of S -> ManySortedSign means

      : Def2: (( id the carrier of it ),( id the carrier' of it )) form_morphism_between (it ,S);

      existence

      proof

        take S;

        thus thesis by Th8;

      end;

    end

    theorem :: INSTALG1:10

    

     Th10: for S be feasible ManySortedSign, T be 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, T be Subsignature of S;

      set g = ( id the carrier' of T);

      (( id the carrier of T),g) 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;

      hence thesis;

    end;

    registration

      let S be feasible ManySortedSign;

      cluster -> feasible for Subsignature of S;

      coherence

      proof

        let T be Subsignature of S;

        set f = ( id the carrier of T), g = ( id the carrier' of T);

        

         A1: ( dom g) = the carrier' of T;

        (f,g) form_morphism_between (T,S) by Def2;

        then

         A2: (f * the ResultSort of T) = (the ResultSort of S * g);

        assume the carrier of T = {} ;

        then

         A3: {} = (the ResultSort of S * g) by A2;

        the carrier' of S = ( dom the ResultSort of S) & ( rng g) = the carrier' of T by Th7;

        hence thesis by A3, A1, Th10, RELAT_1: 27;

      end;

    end

    theorem :: INSTALG1:11

    

     Th11: for S be feasible ManySortedSign, T be 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, T be Subsignature of S;

      set f = ( id the carrier of T), g = ( id the carrier' of T);

      

       A1: ( dom the Arity of T) = the carrier' of T by FUNCT_2:def 1;

      

       A2: (f,g) form_morphism_between (T,S) by Def2;

       A3:

      now

        let x be object;

        

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

        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;

        (g . x) = x by A1, A5, FUNCT_1: 17;

        then ( rng p) c= the carrier of T & (f * p) = (the Arity of S . x) by A2, A1, A5, FINSEQ_1:def 4;

        hence (the Arity of T . x) = (the Arity of S . x) by RELAT_1: 53;

      end;

      the ResultSort of T = (f * the ResultSort of T) by FUNCT_2: 17

      .= (the ResultSort of S * g) by A2;

      hence the ResultSort of T c= the ResultSort of S by RELAT_1: 50;

      ( 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 thesis by A3, GRFUNC_1: 2;

    end;

    theorem :: INSTALG1:12

    

     Th12: for S be feasible ManySortedSign, T be 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, T be Subsignature of S;

      

       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 thesis by A2, A1, GRFUNC_1: 23;

    end;

    theorem :: INSTALG1:13

    

     Th13: for S,T be 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;

      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;

      set f = ( id the carrier of T), g = ( id the carrier' of T);

      thus ( dom f) = the carrier of T & ( dom g) = the carrier' of T;

      thus ( rng f) c= the carrier of S by A1;

      

       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 g) = the carrier' of T by FUNCT_2:def 1;

      hence ( rng g) c= the carrier' of S by A2, A4, GRFUNC_1: 2;

      

       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 (f * 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 * g) by RELAT_1: 65;

      let o be set, p be Function;

      assume that

       A6: o in the carrier' of T and

       A7: p = (the Arity 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 (f * p) = p by RELAT_1: 53

      .= (the Arity of S . o) by A2, A4, A6, A7, GRFUNC_1: 2

      .= (the Arity of S . (g . o)) by A6, FUNCT_1: 17;

    end;

    theorem :: INSTALG1:14

    for S,T be 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 such that

       A1: the carrier of T c= the carrier 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);

      the Arity of T c= the Arity of S by A2, RELAT_1: 59;

      hence thesis by A1, A3, Th13, RELAT_1: 59;

    end;

    theorem :: INSTALG1:15

    

     Th15: for S be feasible ManySortedSign holds S is Subsignature of S

    proof

      let S be feasible ManySortedSign;

      thus (( id the carrier of S),( id the carrier' of S)) form_morphism_between (S,S) by Th8;

    end;

    theorem :: INSTALG1:16

    for S1 be feasible ManySortedSign holds for S2 be Subsignature of S1 holds for S3 be Subsignature of S2 holds S3 is Subsignature of S1

    proof

      let S1 be feasible ManySortedSign;

      let S2 be Subsignature of S1, S3 be Subsignature of S2;

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

    end;

    theorem :: INSTALG1:17

    for S1 be feasible ManySortedSign holds for S2 be Subsignature of S1 st S1 is Subsignature of S2 holds the ManySortedSign of S1 = the ManySortedSign of S2

    proof

      let S1 be feasible ManySortedSign;

      let S2 be Subsignature of S1;

      

       A1: the carrier of S2 c= the carrier of S1 by Th10;

      assume

       A2: S1 is Subsignature 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 thesis by A6, A3, A5, A8, XBOOLE_0:def 10;

    end;

    registration

      let S be non empty ManySortedSign;

      cluster non empty for Subsignature of S;

      existence

      proof

        reconsider T = S as Subsignature of S by Th15;

        take T;

        thus thesis;

      end;

    end

    registration

      let S be non void feasible ManySortedSign;

      cluster non void for Subsignature of S;

      existence

      proof

        reconsider T = S as Subsignature of S by Th15;

        take T;

        thus thesis;

      end;

    end

    theorem :: INSTALG1:18

    for S be feasible ManySortedSign, S9 be Subsignature of S holds for T be ManySortedSign, f,g be 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, S9 be Subsignature of S;

      let T be ManySortedSign, f,g be Function;

      

       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 thesis by A1, PUA2MSS1: 29;

    end;

    theorem :: INSTALG1:19

    for S be ManySortedSign, T be feasible ManySortedSign holds for T9 be Subsignature of T, f,g be Function st (f,g) form_morphism_between (S,T9) holds (f,g) form_morphism_between (S,T)

    proof

      let S be ManySortedSign, T be feasible ManySortedSign;

      let T9 be Subsignature of T, f,g be Function such that

       A1: (f,g) form_morphism_between (S,T9);

      ( rng f) c= the carrier of T9 by A1;

      then

       A2: (( id the carrier of T9) * f) = f by RELAT_1: 53;

      ( rng g) c= the carrier' of T9 by A1;

      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 thesis by A1, A2, A3, PUA2MSS1: 29;

    end;

    theorem :: INSTALG1:20

    for S be ManySortedSign, T be feasible ManySortedSign holds for T9 be Subsignature of T, f,g be 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, T be feasible ManySortedSign;

      let T9 be Subsignature of T, f,g be Function;

      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 be set, p be 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;

      thus ( dom f) = the carrier of S & ( dom g) = the carrier' of S by A1, A2;

      thus ( rng f) c= the carrier of T9 & ( rng g) c= the carrier' of T9 by A5, A6;

      

      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;

      let o be set, p be Function;

      assume that

       A7: o in the carrier' of S and

       A8: p = (the Arity of S . 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 thesis by A4, A7, A8;

    end;

    begin

    definition

      let S1,S2 be non empty ManySortedSign;

      let A be MSAlgebra over S2;

      let f,g be Function;

      :: INSTALG1:def3

      func A | (S1,f,g) -> strict MSAlgebra over S1 means

      : Def3: the Sorts of it = (the Sorts of A * f) & the Charact of it = (the Charact of A * g);

      existence

      proof

        ( dom f) = the carrier of S1 & ( rng f) c= the carrier of S2 by A1;

        then

        reconsider f9 = f as Function of the carrier of S1, the carrier of S2 by FUNCT_2:def 1, RELSET_1: 4;

        

         A2: ( rng g) c= the carrier' of S2 by A1;

        

         A3: ( dom g) = the carrier' of S1 by A1;

        then

        reconsider g9 = g as Function of the carrier' of S1, the carrier' of S2 by A2, 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 A3, A2, 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 object;

          assume

           A4: o in the carrier' of S1;

          then

          reconsider p1 = (the Arity of S1 . o) as Element of (the carrier of S1 * ) by FUNCT_2: 5;

          

           A5: (g . o) in ( rng g) by A3, A4, FUNCT_1:def 3;

          then

          reconsider p2 = (the Arity of S2 . (g . o)) as Element of (the carrier of S2 * ) by A2, FUNCT_2: 5;

          reconsider o as OperSymbol of S1 by A4;

          

           A6: (C . o) = (the Charact of A . (g9 . o)) by A2, A4, A5, 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 A1

          .= ((the Sorts of A * the ResultSort of S2) * g) by RELAT_1: 36;

          then

           A7: (((the Sorts of A * f9) * the ResultSort of S1) . o) = ((the Sorts of A * the ResultSort of S2) . (g9 . o)) by A2, A4, A5, FUNCT_2: 15;

          

           A8: ((the Sorts of A * f9) * p1) = (the Sorts of A * (f9 * p1)) by RELAT_1: 36

          .= (the Sorts of A * p2) by A1, A4;

          ((((the Sorts of A * f9) # ) * the Arity of S1) . o) = (((the Sorts of A * f9) # ) . p1) by A4, FUNCT_2: 15

          .= ( product ((the Sorts of A * f9) * p1)) by FINSEQ_2:def 5

          .= ((the Sorts of A # ) . p2) by A8, FINSEQ_2:def 5

          .= (((the Sorts of A # ) * the Arity of S2) . (g9 . o)) by A2, A5, FUNCT_2: 15;

          hence thesis by A2, A5, A7, A6, PBOOLE:def 15;

        end;

        then

        reconsider 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 #);

        thus thesis;

      end;

      correctness ;

    end

    definition

      let S2,S1 be non empty ManySortedSign;

      let A be MSAlgebra over S2;

      :: INSTALG1:def4

      func A | S1 -> strict MSAlgebra over S1 equals (A | (S1,( id the carrier of S1),( id the carrier' of S1)));

      correctness ;

    end

    theorem :: INSTALG1:21

    for S1,S2 be non empty ManySortedSign holds for A,B be MSAlgebra over S2 st the MSAlgebra of A = the MSAlgebra of B holds for f,g be 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;

      let A,B be MSAlgebra over S2 such that

       A1: the MSAlgebra of A = the MSAlgebra of B;

      let f,g be Function;

      assume

       A2: (f,g) form_morphism_between (S1,S2);

      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 thesis by A1, A2, Def3;

    end;

    theorem :: INSTALG1:22

    

     Th22: for S1,S2 be non empty ManySortedSign holds for A be non-empty MSAlgebra over S2 holds for f,g be 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;

      let A be non-empty MSAlgebra over S2;

      let f,g be Function;

      assume (f,g) form_morphism_between (S1,S2);

      then the Sorts of (A | (S1,f,g)) = (the Sorts of A * f) by Def3;

      hence the Sorts of (A | (S1,f,g)) is non-empty;

    end;

    registration

      let S2 be non empty ManySortedSign;

      let S1 be non empty Subsignature of S2;

      let A be non-empty MSAlgebra over S2;

      cluster (A | S1) -> non-empty;

      coherence by Def2, Th22;

    end

    theorem :: INSTALG1:23

    

     Th23: for S1,S2 be non void non empty ManySortedSign holds for f,g be Function st (f,g) form_morphism_between (S1,S2) holds for A be MSAlgebra over S2 holds for o1 be OperSymbol of S1, o2 be OperSymbol of S2 st o2 = (g . o1) holds ( Den (o1,(A | (S1,f,g)))) = ( Den (o2,A))

    proof

      let S1,S2 be non void non empty ManySortedSign;

      let f,g be Function;

      assume

       A1: (f,g) form_morphism_between (S1,S2);

      then

      reconsider g9 = g as Function of the carrier' of S1, the carrier' of S2 by Th9;

      let A be MSAlgebra over S2;

      let o1 be OperSymbol of S1, o2 be OperSymbol of S2;

      assume o2 = (g . o1);

      

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

    end;

    theorem :: INSTALG1:24

    

     Th24: for S1,S2 be non void non empty ManySortedSign holds for f,g be Function st (f,g) form_morphism_between (S1,S2) holds for A be MSAlgebra over S2 holds for o1 be OperSymbol of S1, o2 be 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 void non empty ManySortedSign;

      let f,g be Function such that

       A1: (f,g) form_morphism_between (S1,S2);

      

       A2: ( dom f) = the carrier of S1 by A1;

      let A be MSAlgebra over S2;

      let o1 be OperSymbol of S1, o2 be OperSymbol of S2;

      assume

       A3: o2 = (g . o1);

      

      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

      .= ( 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;

      ( dom g) = the carrier' of S1 by A1;

      

      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

      .= (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;

    end;

    theorem :: INSTALG1:25

    

     Th25: for S be non empty ManySortedSign holds for A be MSAlgebra over S holds (A | (S,( id the carrier of S),( id the carrier' of S))) = the MSAlgebra of A

    proof

      let S be non empty ManySortedSign;

      let A be MSAlgebra over S;

      set f = ( id the carrier of S), g = ( id the carrier' of S);

      ( dom the Charact of A) = the carrier' of S by PARTFUN1:def 2;

      then

       A1: the Charact of the MSAlgebra of A = (the Charact of A * g) by RELAT_1: 52;

      ( dom the Sorts of A) = the carrier of S by PARTFUN1:def 2;

      then

       A2: the Sorts of the MSAlgebra of A = (the Sorts of A * f) by RELAT_1: 52;

      (f,g) form_morphism_between (S,S) by Th8;

      hence thesis by A2, A1, Def3;

    end;

    theorem :: INSTALG1:26

    for S be non empty ManySortedSign holds for A be MSAlgebra over S holds (A | S) = the MSAlgebra of A by Th25;

    theorem :: INSTALG1:27

    

     Th27: for S1,S2,S3 be non empty ManySortedSign holds for f1,g1 be Function st (f1,g1) form_morphism_between (S1,S2) holds for f2,g2 be Function st (f2,g2) form_morphism_between (S2,S3) holds for A be 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;

      let f1,g1 be Function such that

       A1: (f1,g1) form_morphism_between (S1,S2);

      let f2,g2 be Function such that

       A2: (f2,g2) form_morphism_between (S2,S3);

      

       A3: ((f2 * f1),(g2 * g1)) form_morphism_between (S1,S3) by A1, A2, PUA2MSS1: 29;

      let A be MSAlgebra over S3;

      

       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 thesis by A3, A4, Def3;

    end;

    theorem :: INSTALG1:28

    for S1 be non empty feasible ManySortedSign holds for S2 be non empty Subsignature of S1 holds for S3 be non empty Subsignature of S2 holds for A be MSAlgebra over S1 holds (A | S3) = ((A | S2) | S3)

    proof

      let S1 be non empty feasible ManySortedSign;

      let S2 be non empty Subsignature of S1;

      let S3 be non empty Subsignature of S2;

      let A be MSAlgebra over S1;

      set f1 = ( id the carrier of S2), g1 = ( id the carrier' of S2);

      set f2 = ( id the carrier of S3), g2 = ( id the carrier' of S3);

      ( rng f2) = the carrier of S3;

      then

       A1: (f1 * f2) = f2 by Th10, RELAT_1: 53;

      ( rng g2) = the carrier' of S3;

      then

       A2: (g1 * g2) = g2 by Th10, RELAT_1: 53;

      (f1,g1) form_morphism_between (S2,S1) & (f2,g2) form_morphism_between (S3,S2) by Def2;

      hence thesis by A1, A2, Th27;

    end;

    theorem :: INSTALG1:29

    

     Th29: for S1,S2 be non empty ManySortedSign holds for f be Function of the carrier of S1, the carrier of S2 holds for g be Function st (f,g) form_morphism_between (S1,S2) holds for A1,A2 be MSAlgebra over S2 holds for h be 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;

      let f be Function of the carrier of S1, the carrier of S2;

      let g be Function such that

       A1: (f,g) form_morphism_between (S1,S2);

      let A1,A2 be MSAlgebra over S2;

      let h be ManySortedFunction of the Sorts of A1, the Sorts of A2;

      set B1 = (A1 | (S1,f,g)), B2 = (A2 | (S1,f,g));

      let x be object;

      assume x in the carrier of S1;

      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 B1 & (the Sorts of A2 * f) = the Sorts of B2 by A1, Def3;

      hence thesis by A2, A3;

    end;

    theorem :: INSTALG1:30

    for S1 be non empty ManySortedSign holds for S2 be non empty Subsignature of S1 holds for A1,A2 be MSAlgebra over S1 holds for h be 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;

      let S2 be non empty Subsignature of S1;

      set f = ( id the carrier of S2), g = ( id the carrier' of S2);

      let A1,A2 be MSAlgebra over S1;

      let h be ManySortedFunction of the Sorts of A1, the Sorts of A2;

      

       A1: (f,g) form_morphism_between (S2,S1) by Def2;

      then

      reconsider f as Function of the carrier of S2, the carrier of S1 by Th9;

      (h * f) is ManySortedFunction of the Sorts of (A1 | (S2,f,g)), the Sorts of (A2 | (S2,f,g)) by A1, Th29;

      hence thesis by RELAT_1: 65;

    end;

    theorem :: INSTALG1:31

    

     Th31: for S1,S2 be non empty ManySortedSign holds for f,g be Function st (f,g) form_morphism_between (S1,S2) holds for A be 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;

      let f,g be Function such that

       A1: (f,g) form_morphism_between (S1,S2);

      ( dom f) = the carrier of S1 & ( rng f) c= the carrier of S2 by A1;

      then

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

      now

        let i be object;

        assume i in the carrier of S1;

        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;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: INSTALG1:32

    for S1 be non empty ManySortedSign holds for S2 be non empty Subsignature of S1 holds for A be 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;

      let S2 be non empty Subsignature of S1;

      set f = ( id the carrier of S2), g = ( id the carrier' of S2);

      let A be MSAlgebra over S1;

      (f,g) form_morphism_between (S2,S1) by Def2;

      then (( id the Sorts of A) * f) = ( id the Sorts of (A | S2)) by Th31;

      hence thesis by RELAT_1: 65;

    end;

    theorem :: INSTALG1:33

    

     Th33: for S1,S2 be non void non empty ManySortedSign holds for f,g be Function st (f,g) form_morphism_between (S1,S2) holds for A,B be MSAlgebra over S2 holds for h2 be ManySortedFunction of A, B holds for h1 be ManySortedFunction of (A | (S1,f,g)), (B | (S1,f,g)) st h1 = (h2 * f) holds for o1 be OperSymbol of S1, o2 be OperSymbol of S2 st o2 = (g . o1) & ( Args (o2,A)) <> {} & ( Args (o2,B)) <> {} holds for x2 be Element of ( Args (o2,A)) holds for x1 be Element of ( Args (o1,(A | (S1,f,g)))) st x2 = x1 holds (h1 # x1) = (h2 # x2)

    proof

      let S1,S2 be non void non empty ManySortedSign;

      let f,g be Function such that

       A1: (f,g) form_morphism_between (S1,S2);

      let A2,B2 be MSAlgebra over S2;

      set A1 = (A2 | (S1,f,g)), B1 = (B2 | (S1,f,g));

      let h2 be ManySortedFunction of A2, B2;

      let h1 be ManySortedFunction of A1, B1 such that

       A2: h1 = (h2 * f);

      let o1 be OperSymbol of S1, o2 be OperSymbol of S2 such that

       A3: o2 = (g . o1);

      assume that

       A4: ( Args (o2,A2)) <> {} and

       A5: ( Args (o2,B2)) <> {} ;

      let x2 be Element of ( Args (o2,A2));

      let x1 be Element of ( Args (o1,A1));

      assume

       A6: x2 = x1;

      then

      reconsider f1 = x1, f2 = x2, g2 = (h2 # x2) as Function by A4, A5, MSUALG_6: 1;

      

       A7: ( Args (o2,A2)) = ( Args (o1,A1)) 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

        let i be Nat;

        assume

         A11: i in ( dom f1);

        ( dom f) = the carrier of S1 by A1;

        

        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

        .= (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;

      end;

      ( Args (o2,B2)) = ( Args (o1,B1)) by A1, A3, Th24;

      hence thesis by A4, A5, A7, A10, MSUALG_3: 24;

    end;

    theorem :: INSTALG1:34

    

     Th34: for S,S9 be non empty non void ManySortedSign holds for A1,A2 be MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for h be ManySortedFunction of A1, A2 st h is_homomorphism (A1,A2) holds for f be Function of the carrier of S9, the carrier of S holds for g be Function st (f,g) form_morphism_between (S9,S) holds ex h9 be 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;

      let A1,A2 be MSAlgebra over S such that

       A1: the Sorts of A1 is_transformable_to the Sorts of A2;

      let h be ManySortedFunction of A1, A2 such that

       A2: h is_homomorphism (A1,A2);

      let f be Function of the carrier of S9, the carrier of S;

      let g be Function such that

       A3: (f,g) form_morphism_between (S9,S);

      

       A4: ( dom g) = the carrier' of S9 & ( rng g) c= the carrier' of S by A3;

      set B1 = (A1 | (S9,f,g)), B2 = (A2 | (S9,f,g));

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

      reconsider h9 = (h * f) as ManySortedFunction of B1, B2 by A3, Th29;

      take h9;

      thus h9 = (h * f);

      let o be OperSymbol of S9;

      set go = (g . o);

      assume

       A6: ( Args (o,B1)) <> {} ;

      let x be Element of ( Args (o,B1));

      reconsider y = x as Element of ( Args (go,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 go)) by FUNCT_2: 15;

      

       A8: ( Den (o,B1)) = ( Den (go,A1)) & ( Den (o,B2)) = ( Den (go,A2)) by A3, Th23;

      

       A9: ( Args (o,B1)) = ( Args ((g . o),A1)) by A3, Th24;

      

       A10: ( Args (o,B2)) = ( Args ((g . o),A2)) by A3, Th24;

      then ( Args (o,B2)) <> {} by A1, A6, A9, Th2;

      then (h9 # x) = (h # y) by A3, A6, A9, A10, Th33;

      hence thesis by A2, A6, A9, A8, A7;

    end;

    theorem :: INSTALG1:35

    for S be non void feasible ManySortedSign holds for S9 be non void Subsignature of S holds for A1,A2 be MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds for h be ManySortedFunction of A1, A2 st h is_homomorphism (A1,A2) holds ex h9 be 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;

      let S9 be non void Subsignature of S;

      let A1,A2 be MSAlgebra over S such that

       A1: the Sorts of A1 is_transformable_to the Sorts of A2;

      set f = ( id the carrier of S9), g = ( id the carrier' of S9);

      

       A2: (f,g) form_morphism_between (S9,S) by Def2;

      then

      reconsider f as Function of the carrier of S9, the carrier of S by Th9;

      let h be ManySortedFunction of A1, A2;

      assume h is_homomorphism (A1,A2);

      then

      consider h9 be ManySortedFunction of (A1 | (S9,f,g)), (A2 | (S9,f,g)) such that

       A3: h9 = (h * f) and

       A4: h9 is_homomorphism ((A1 | (S9,f,g)),(A2 | (S9,f,g))) by A1, A2, Th34;

      consider k be ManySortedFunction of (A1 | S9), (A2 | S9) such that

       A5: k = h9 and k is_homomorphism ((A1 | S9),(A2 | S9)) by A4;

      take k;

      thus thesis by A3, A4, A5, RELAT_1: 65;

    end;

    theorem :: INSTALG1:36

    

     Th36: for S,S9 be non empty non void ManySortedSign holds for A be non-empty MSAlgebra over S holds for f be Function of the carrier of S9, the carrier of S holds for g be Function st (f,g) form_morphism_between (S9,S) holds for B be non-empty MSAlgebra over S9 st B = (A | (S9,f,g)) holds for s1,s2 be SortSymbol of S9, t be 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;

      let A be non-empty MSAlgebra over S;

      let f be Function of the carrier of S9, the carrier of S;

      let g be Function such that

       A1: (f,g) form_morphism_between (S9,S);

      

       A2: ( dom g) = the carrier' of S9 & ( rng g) c= the carrier' of S by A1;

      let B be non-empty MSAlgebra over S9 such that

       A3: B = (A | (S9,f,g));

      reconsider 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, t be Function;

      given o be OperSymbol of S9 such that

       A4: ( the_result_sort_of o) = s2 and

       A5: ex i be Element of NAT st i in ( dom ( the_arity_of o)) & (( the_arity_of o) /. i) = s1 & ex a be Function st a in ( Args (o,B)) & t = ( transl (o,i,a,B));

      

       A6: (f * ( the_arity_of o)) = ( the_arity_of (g . o)) by A1;

      take (g . o);

      (f * the ResultSort of S9) = (the ResultSort of S * g) by A1;

      

      hence ( the_result_sort_of (g . o)) = ((f * the ResultSort of S9) . o) by FUNCT_2: 15

      .= (f . s2) by A4, FUNCT_2: 15;

      consider i be Element of NAT , a be 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;

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

      

      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;

      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

        let x be object;

        assume x in (the Sorts of B . s1);

        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;

      end;

      take a;

      thus a in ( Args ((g . o),A)) by A1, A3, A9, Th24;

      ( dom t) = (the Sorts of B . s1) by A8, A10, MSUALG_6:def 4;

      hence thesis by A12, A13, A15, FUNCT_2: 15;

    end;

    

     Lm1: for S,S9 be non empty non void ManySortedSign holds for A be non-empty MSAlgebra over S holds for f be Function of the carrier of S9, the carrier of S holds for g be Function st (f,g) form_morphism_between (S9,S) holds for B be non-empty MSAlgebra over S9 st B = (A | (S9,f,g)) holds for s1,s2 be SortSymbol of S9 st ( TranslationRel S9) reduces (s1,s2) holds ( TranslationRel S) reduces ((f . s1),(f . s2)) & for t be Translation of B, s1, s2 holds t is Translation of A, (f . s1), (f . s2)

    proof

      let S,S9 be non void non empty ManySortedSign;

      let A be non-empty MSAlgebra over S;

      let f be Function of the carrier of S9, the carrier of S;

      let g be Function such that

       A1: (f,g) form_morphism_between (S9,S);

      defpred P[ 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 such that

       A2: B = (A | (S9,f,g));

      

       A3: for s1,s2,s3 be SortSymbol of S9 st ( TranslationRel S9) reduces (s1,s2) holds for t be Translation of B, s1, s2 st P[t, s1, s2] holds for h be Function st h is_e.translation_of (B,s2,s3) holds P[(h * t), s1, s3]

      proof

        let s1,s2,s3 be SortSymbol of S9 such that ( TranslationRel S9) reduces (s1,s2);

        let t be Translation of B, s1, s2 such that

         A4: P[t, s1, s2];

        let h be Function;

        assume

         A5: h is_e.translation_of (B,s2,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 thesis by A4, A6, MSUALG_6: 19, REWRITE1: 16;

      end;

      let s1,s2 be SortSymbol of S9;

      assume

       A7: ( TranslationRel S9) reduces (s1,s2);

      

       A8: for s be SortSymbol of S9 holds P[( id (the Sorts of B . s)), s, s]

      proof

        let s be SortSymbol of S9;

        thus ( TranslationRel S) reduces ((f . s),(f . s)) by REWRITE1: 12;

        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 thesis by MSUALG_6: 16;

      end;

      for s1,s2 be SortSymbol of S9 st ( TranslationRel S9) reduces (s1,s2) holds for t be Translation of B, s1, s2 holds P[t, s1, s2] from MSUALG_6:sch 1( A8, A3);

      hence thesis by A7;

    end;

    theorem :: INSTALG1:37

    for S,S9 be non empty non void ManySortedSign holds for f be Function of the carrier of S9, the carrier of S holds for g be Function st (f,g) form_morphism_between (S9,S) holds for s1,s2 be 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;

      set A = the non-empty MSAlgebra over S;

      let f be Function of the carrier of S9, the carrier of S;

      let g be Function;

      assume

       A1: (f,g) form_morphism_between (S9,S);

      then (A | (S9,f,g)) is non-empty MSAlgebra over S9 by Th22;

      hence thesis by A1, Lm1;

    end;

    theorem :: INSTALG1:38

    for S,S9 be non void non empty ManySortedSign holds for A be non-empty MSAlgebra over S holds for f be Function of the carrier of S9, the carrier of S holds for g be Function st (f,g) form_morphism_between (S9,S) holds for B be non-empty MSAlgebra over S9 st B = (A | (S9,f,g)) holds for s1,s2 be SortSymbol of S9 st ( TranslationRel S9) reduces (s1,s2) holds for t be Translation of B, s1, s2 holds t is Translation of A, (f . s1), (f . s2) by Lm1;

    begin

    scheme :: INSTALG1:sch1

    GenFuncEx { S() -> non empty non void ManySortedSign , A() -> non-empty MSAlgebra over S() , X() -> non-empty ManySortedSet of the carrier of S() , F( object, object) -> set } :

ex h be ManySortedFunction of ( FreeMSA X()), A() st h is_homomorphism (( FreeMSA X()),A()) & for s be SortSymbol of S() holds for x be Element of (X() . s) holds ((h . s) . ( root-tree [x, s])) = F(x,s)

      provided

       A1: for s be SortSymbol of S() holds for x be Element of (X() . s) holds F(x,s) in (the Sorts of A() . s);

      defpred P[ object, object] means ex f be Function of (( FreeGen X()) . $1), (the Sorts of A() . $1) st $2 = f & for x be Element of (X() . $1) holds (f . ( root-tree [x, $1])) = F(x,$1);

      

       A2: for a be object st a in the carrier of S() holds ex y be object st P[a, y]

      proof

        let a be object;

        assume a in the carrier of S();

        then

        reconsider s = a as SortSymbol of S();

        defpred P[ object, object] means ex x be Element of (X() . s) st $1 = ( root-tree [x, s]) & $2 = F(x,s);

        

         A3: (( FreeGen X()) . s) = ( FreeGen (s,X())) by MSAFREE:def 16;

        

         A4: for y be object st y in (( FreeGen X()) . s) holds ex z be object st z in (the Sorts of A() . s) & P[y, z]

        proof

          let y be object;

          assume y in (( FreeGen X()) . s);

          then

          consider a be set such that

           A5: a in (X() . s) and

           A6: y = ( root-tree [a, s]) by A3, MSAFREE:def 15;

          reconsider a as Element of (X() . s) by A5;

          take z = F(a,s);

          thus z in (the Sorts of A() . s) by A1;

          take a;

          thus thesis by A6;

        end;

        consider f be Function such that

         A7: ( dom f) = (( FreeGen X()) . s) & ( rng f) c= (the Sorts of A() . s) and

         A8: for y be object st y in (( FreeGen X()) . s) holds P[y, (f . y)] from FUNCT_1:sch 6( A4);

        reconsider f as Function of (( FreeGen X()) . a), (the Sorts of A() . a) by A7, FUNCT_2: 2;

        take y = f, f;

        thus y = f;

        let x be Element of (X() . a);

        ( root-tree [x, s]) in (( FreeGen X()) . s) by A3, MSAFREE:def 15;

        then

        consider z be Element of (X() . s) such that

         A9: ( root-tree [x, s]) = ( root-tree [z, s]) and

         A10: (f . ( root-tree [x, s])) = F(z,s) by A8;

         [x, s] = [z, s] by A9, TREES_4: 4;

        hence thesis by A10, XTUPLE_0: 1;

      end;

      consider h be Function such that

       A11: ( dom h) = the carrier of S() and

       A12: for a be object st a in the carrier of S() holds P[a, (h . a)] from CLASSES1:sch 1( A2);

      reconsider h as ManySortedSet of the carrier of S() by A11, PARTFUN1:def 2, RELAT_1:def 18;

      h is ManySortedFunction of ( FreeGen X()), the Sorts of A()

      proof

        let a be object;

        assume a in the carrier of S();

        then ex f be Function of (( FreeGen X()) . a), (the Sorts of A() . a) st (h . a) = f & for x be Element of (X() . a) holds (f . ( root-tree [x, a])) = F(x,a) by A12;

        hence thesis;

      end;

      then

      reconsider h as ManySortedFunction of ( FreeGen X()), the Sorts of A();

      consider H be ManySortedFunction of ( FreeMSA X()), A() such that

       A13: H is_homomorphism (( FreeMSA X()),A()) and

       A14: (H || ( FreeGen X())) = h by MSAFREE:def 5;

      take H;

      thus H is_homomorphism (( FreeMSA X()),A()) by A13;

      let s be SortSymbol of S(), x be Element of (X() . s);

      

       A15: ex f be Function of (( FreeGen X()) . s), (the Sorts of A() . s) st (h . s) = f & for x be Element of (X() . s) holds (f . ( root-tree [x, s])) = F(x,s) by A12;

      reconsider t = ( root-tree [x, s]) as Term of S(), X() by MSATERM: 4;

      (( FreeGen X()) . s) = ( FreeGen (s,X())) by MSAFREE:def 16;

      then

       A16: t in (( FreeGen X()) . s) by MSAFREE:def 15;

      (h . s) = ((H . s) | (( FreeGen X()) . 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 thesis by A15;

    end;

    theorem :: INSTALG1:39

    

     Th39: for I be set, A,B be ManySortedSet of I holds for C be ManySortedSubset of A holds for F be ManySortedFunction of A, B holds for i be set st i in I holds for f,g be Function st f = (F . i) & g = ((F || C) . i) holds for x be set st x in (C . i) holds (g . x) = (f . x)

    proof

      let I be set, A,B be ManySortedSet of I;

      let C be ManySortedSubset of A;

      let F be ManySortedFunction of A, B;

      let i be set;

      assume

       A1: i in I;

      then

      reconsider Fi = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

      let f,g be Function;

      assume that

       A2: f = (F . i) and

       A3: g = ((F || C) . i);

      let x be set;

      g = (Fi | (C . i)) by A1, A3, MSAFREE:def 1;

      hence thesis by A2, FUNCT_1: 49;

    end;

    registration

      let S be non void non empty ManySortedSign;

      let X be non-empty ManySortedSet of the carrier of S;

      cluster ( FreeGen X) -> non-empty;

      coherence ;

    end

    definition

      let S1,S2 be non empty non void ManySortedSign;

      let X be non-empty ManySortedSet of the carrier of S2;

      let f be Function of the carrier of S1, the carrier of S2;

      let g be Function;

      :: INSTALG1:def5

      func hom (f,g,X,S1,S2) -> ManySortedFunction of ( FreeMSA (X * f)), (( FreeMSA X) | (S1,f,g)) means

      : Def5: it is_homomorphism (( FreeMSA (X * f)),(( FreeMSA X) | (S1,f,g))) & for s be SortSymbol of S1, x be Element of ((X * f) . s) holds ((it . s) . ( root-tree [x, s])) = ( root-tree [x, (f . s)]);

      existence

      proof

        set A = (( FreeMSA X) | (S1,f,g));

        the Sorts of A = (the Sorts of ( FreeMSA X) * f) by A1, Def3;

        then

        reconsider A as non-empty MSAlgebra over S1 by MSUALG_1:def 3;

        deffunc F( set, set) = ( root-tree [$1, (f . $2)]);

         A2:

        now

          let s be SortSymbol of S1, x be Element of ((X * f) . 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

           A3: 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 A1, Def3, MSAFREE:def 14;

          hence F(x,s) in (the Sorts of A . s) by A3, FUNCT_2: 15;

        end;

        consider H be ManySortedFunction of ( FreeMSA (X * f)), A such that

         A4: H is_homomorphism (( FreeMSA (X * f)),A) & for s be SortSymbol of S1 holds for x be Element of ((X * f) . s) holds ((H . s) . ( root-tree [x, s])) = F(x,s) from GenFuncEx( A2);

        reconsider G = H as ManySortedFunction of ( FreeMSA (X * f)), (( FreeMSA X) | (S1,f,g));

        take G;

        thus thesis by A4;

      end;

      uniqueness

      proof

        reconsider A1 = (( FreeMSA X) | (S1,f,g)) as non-empty MSAlgebra over S1 by A1, Th22;

        let G1,G2 be ManySortedFunction of the Sorts of ( FreeMSA (X * f)), the Sorts of (( FreeMSA X) | (S1,f,g)) such that

         A5: G1 is_homomorphism (( FreeMSA (X * f)),(( FreeMSA X) | (S1,f,g))) and

         A6: for s be SortSymbol of S1, x be Element of ((X * f) . s) holds ((G1 . s) . ( root-tree [x, s])) = ( root-tree [x, (f . s)]) and

         A7: G2 is_homomorphism (( FreeMSA (X * f)),(( FreeMSA X) | (S1,f,g))) and

         A8: for s be SortSymbol of S1, x be Element of ((X * f) . s) holds ((G2 . s) . ( root-tree [x, s])) = ( root-tree [x, (f . s)]);

        set H1 = G1, H2 = G2;

         A9:

        now

          let x be object;

          assume x in the carrier of S1;

          then

          reconsider s = x as SortSymbol of S1;

          reconsider g1 = ((H1 || ( FreeGen (X * f))) . s), g2 = ((H2 || ( FreeGen (X * f))) . s) as Function of (( FreeGen (X * f)) . s), (the Sorts of A1 . s);

          now

            let z be Element of (( FreeGen (X * f)) . s);

            ( FreeGen (s,(X * f))) = (( FreeGen (X * f)) . s) by MSAFREE:def 16;

            then

            consider a be set such that

             A10: a in ((X * f) . s) and

             A11: z = ( root-tree [a, s]) by MSAFREE:def 15;

            reconsider a as Element of ((X * f) . s) by A10;

            

            thus (g1 . z) = ((H1 . s) . z) by Th39

            .= ( root-tree [a, (f . s)]) by A6, A11

            .= ((H2 . s) . z) by A8, A11

            .= (g2 . z) by Th39;

          end;

          hence ((H1 || ( FreeGen (X * f))) . x) = ((H2 || ( FreeGen (X * f))) . x) by FUNCT_2: 63;

        end;

        A1 = (( FreeMSA X) | (S1,f,g));

        hence thesis by A5, A7, A9, EXTENS_1: 14, PBOOLE: 3;

      end;

    end

    theorem :: INSTALG1:40

    

     Th40: for S1,S2 be non void non empty ManySortedSign holds for X be non-empty ManySortedSet of the carrier of S2 holds for f be Function of the carrier of S1, the carrier of S2 holds for g be Function st (f,g) form_morphism_between (S1,S2) holds for o be OperSymbol of S1, p be Element of ( Args (o,( FreeMSA (X * f)))) holds for q be 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 void non empty ManySortedSign;

      let X be non-empty ManySortedSet of the carrier of S2;

      let f be Function of the carrier of S1, the carrier of S2;

      let g be Function;

      set F = ( hom (f,g,X,S1,S2));

      assume

       A1: (f,g) form_morphism_between (S1,S2);

      then

      reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;

      let o be OperSymbol of S1, p be Element of ( Args (o,( FreeMSA (X * f))));

      let q be FinSequence;

      assume

       A2: q = (F # p);

      then

       A3: q is Element of ( Args ((h . o),( FreeMSA X))) by A1, Th24;

      F is_homomorphism (( FreeMSA (X * f)),(( FreeMSA X) | (S1,f,g))) by A1, Def5;

      then ((F . ( the_result_sort_of o)) . (( Den (o,( FreeMSA (X * f)))) . p)) = (( Den (o,(( FreeMSA X) | (S1,f,g)))) . q) by A2;

      

      hence ((F . ( 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;

    end;

    theorem :: INSTALG1:41

    

     Th41: for S1,S2 be non void non empty ManySortedSign holds for X be non-empty ManySortedSet of the carrier of S2 holds for f be Function of the carrier of S1, the carrier of S2 holds for g be Function st (f,g) form_morphism_between (S1,S2) holds for t be 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 void non empty ManySortedSign;

      let X be non-empty ManySortedSet of the carrier of S2;

      let f be Function of the carrier of S1, the carrier of S2;

      let g be Function;

      assume

       A1: (f,g) form_morphism_between (S1,S2);

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

      hereby

        assume ((( hom (f,g,X,S1,S2)) . ( the_sort_of t)) . t) is CompoundTerm of S2, X;

        then

        reconsider w = ((( hom (f,g,X,S1,S2)) . ( the_sort_of t)) . t) as CompoundTerm of S2, X;

        assume not t is CompoundTerm of S1, (X * f);

        then not (t . {} ) in [:the carrier' of S1, {the carrier of S1}:] by MSATERM:def 6;

        then

        consider s be SortSymbol of S1, v be 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;

      end;

      assume t is CompoundTerm of S1, (X * f);

      then

      reconsider 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 be object 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 as OperSymbol of S1 by A4;

      r = the carrier of S1 by A5, TARSKI:def 1;

      then

      consider a be ArgumentSeq of ( Sym (o,(X * f))) such that

       A7: t = ( [o, the carrier of S1] -tree a) by A6, MSATERM: 10;

      reconsider 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 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 thesis by A7, A9, A8, MSATERM:def 6;

    end;

    theorem :: INSTALG1:42

    for S1,S2 be non void non empty ManySortedSign holds for X be non-empty ManySortedSet of the carrier of S2 holds for f be Function of the carrier of S1, the carrier of S2 holds for g be 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 void non empty ManySortedSign;

      let X be non-empty ManySortedSet of the carrier of S2;

      let f be Function of the carrier of S1, the carrier of S2;

      let g be one-to-one Function;

      set A = (( FreeMSA X) | (S1,f,g));

      set H = ( hom (f,g,X,S1,S2));

      defpred P[ set] means ex t1 be Term of S1, (X * f) st t1 = $1 & for t2 be Term of S1, (X * f) st ( the_sort_of t1) = ( the_sort_of t2) & ((H . ( the_sort_of t1)) . t1) = ((H . ( 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);

      then

      reconsider h = g as Function of the carrier' of S1, the carrier' of S2 by Th9;

      reconsider B = A as non-empty MSAlgebra over S1 by A2, Th22;

      reconsider H9 = H as ManySortedFunction of ( FreeMSA (X * f)), B;

      

       A3: for o be OperSymbol of S1, p be ArgumentSeq of ( Sym (o,(X * f))) st for t be Term of S1, (X * f) st t in ( rng p) holds P[t] holds P[( [o, the carrier of S1] -tree p)]

      proof

        let o be OperSymbol of S1, p be ArgumentSeq of ( Sym (o,(X * f))) such that

         A4: for t be Term of S1, (X * f) st t in ( rng p) holds P[t];

        

         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 = (H # a) as Element of ( Args ((h . o),( FreeMSA X))) by A2, Th24;

        take t1 = (( Sym (o,(X * f))) -tree p);

        thus

         A7: t1 = ( [o, the carrier of S1] -tree p) by MSAFREE:def 9;

        reconsider b = q as ArgumentSeq of ( Sym ((h . o),X)) by Th1;

        let t2 be Term of S1, (X * f) such that

         A8: ( the_sort_of t1) = ( the_sort_of t2) & ((H . ( the_sort_of t1)) . t1) = ((H . ( the_sort_of t1)) . t2);

        ( the_sort_of t1) = ( the_result_sort_of o) by MSATERM: 20;

        then

         A9: ((H . ( 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 be object 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 as OperSymbol of S1 by A10;

        

         A12: (t2 . {} ) = [o9, the carrier of S1] by A11, TARSKI:def 1;

        then

        consider r be 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 = (H # 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: ((H . ( 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

          let i be Nat;

          

           A18: R = (H9 # c);

          assume

           A19: i in ( dom ( the_arity_of o));

          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) = ((H . ( the_sort_of w1)) . w1) by A5, A19, A20, MSUALG_3:def 6;

          then

           A21: ((H . ( the_sort_of w1)) . w1) = ((H . ( 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: P[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;

        end;

        hence thesis by A7, A13, A15, A5, A16, FINSEQ_1: 13;

      end;

      thus H is_homomorphism (( FreeMSA (X * f)),A) by A2, Def5;

      let i be set, h be Function;

      assume i in ( dom H);

      then

      reconsider s = i as SortSymbol of S1 by PARTFUN1:def 2;

      assume

       A23: (H . i) = h;

      

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

      assume

       A25: x in ( dom h) & y in ( dom h);

      ( 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 be SortSymbol of S1, v be Element of ((X * f) . s) holds P[( root-tree [v, s])]

      proof

        let s be SortSymbol of S1, v be Element of ((X * f) . s);

        reconsider t1 = ( root-tree [v, s]) as Term of S1, (X * f) by MSATERM: 4;

        take t1;

        thus t1 = ( root-tree [v, s]);

        let t2 be Term of S1, (X * f) such that

         A27: ( the_sort_of t1) = ( the_sort_of t2) and

         A28: ((H . ( the_sort_of t1)) . t1) = ((H . ( the_sort_of t1)) . t2);

        

         A29: ( the_sort_of t1) = s by MSATERM: 14;

        

         A30: ((H . s) . ( root-tree [v, s])) = ( root-tree [v, (f . s)]) by A2, Def5;

        now

          assume (t2 . {} ) in [:the carrier' of S1, {the carrier of S1}:];

          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;

        end;

        then

        consider s2 be SortSymbol of S1, v2 be 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 ((H . 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 thesis by A33, A34, XTUPLE_0: 1;

      end;

      for t be Term of S1, (X * f) holds P[t] from MSATERM:sch 1( A26, A3);

      then

       A35: P[t1];

      ( the_sort_of t1) = s & ( the_sort_of t2) = s by A24, A25, MSATERM:def 5;

      hence thesis by A23, A35;

    end;

    theorem :: INSTALG1:43

    for S be non void non empty ManySortedSign holds for X be non-empty 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 void non empty ManySortedSign;

      let X be non-empty ManySortedSet of the carrier of S;

      set f = ( id the carrier of S);

      set h = ( hom (f,( id the carrier' of S),X,S,S));

      set I = ( id the Sorts of ( FreeMSA X)), g = ( id the carrier' of S);

      

       A1: (f,g) form_morphism_between (S,S) by PUA2MSS1: 28;

      ( dom X) = the carrier of S by PARTFUN1:def 2;

      then

       A2: (X * f) = X by RELAT_1: 52;

      

       A3: (( FreeMSA X) | (S,f,g)) = ( FreeMSA X) by Th25;

       A4:

      now

        let i be object;

        assume i in the carrier of S;

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

        then ((I . s) | (( FreeGen X) . s)) is Function of (( FreeGen X) . s), (the Sorts of ( FreeMSA X) . s) by FUNCT_2: 32;

        then

         A6: ( dom ((I . s) | (( FreeGen X) . s))) = (( FreeGen X) . s) by FUNCT_2:def 1;

         A7:

        now

          let a be object;

          assume

           A8: a in (( FreeGen X) . s);

          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 be set such that

           A9: x in (X . s) and

           A10: b = ( root-tree [x, s]) by MSAFREE:def 15;

          

          thus (((I . s) | (( FreeGen X) . s)) . a) = ((I . s) . b) by A8, FUNCT_1: 49

          .= (( id (the Sorts of ( FreeMSA X) . s)) . b) by MSUALG_3:def 1

          .= b

          .= ( root-tree [x, (f . s)]) by A10

          .= ((h . s) . b) by A1, A2, A9, A10, Def5

          .= (((h . s) | (( FreeGen X) . s)) . a) by A8, FUNCT_1: 49;

        end;

        ((h . 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 ((h . s) | (( FreeGen X) . s))) = (( FreeGen X) . s) by FUNCT_2:def 1;

        ((I || ( FreeGen X)) . s) = ((I . s) | (( FreeGen X) . s)) & ((h || ( FreeGen (X * f))) . s) = ((h . s) | (( FreeGen (X * f)) . s)) by MSAFREE:def 1;

        hence ((I || ( FreeGen X)) . i) = ((h || ( FreeGen (X * f))) . i) by A2, A6, A11, A7;

      end;

      I is_homomorphism (( FreeMSA X),( FreeMSA X)) & h is_homomorphism (( FreeMSA (X * f)),(( FreeMSA X) | (S,f,g))) by A1, Def5, MSUALG_3: 9;

      hence thesis by A2, A3, A4, EXTENS_1: 19, PBOOLE: 3;

    end;

    theorem :: INSTALG1:44

    for S1,S2,S3 be non void non empty ManySortedSign holds for X be non-empty ManySortedSet of the carrier of S3 holds for f1 be Function of the carrier of S1, the carrier of S2 holds for g1 be Function st (f1,g1) form_morphism_between (S1,S2) holds for f2 be Function of the carrier of S2, the carrier of S3 holds for g2 be 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 void non empty ManySortedSign;

      let X be non-empty ManySortedSet of the carrier of S3;

      let f1 be Function of the carrier of S1, the carrier of S2;

      let g1 be Function such that

       A1: (f1,g1) form_morphism_between (S1,S2);

      let f2 be Function of the carrier of S2, the carrier of S3;

      let g2 be Function;

      set f = (f2 * f1), g = (g2 * g1);

      assume

       A2: (f2,g2) form_morphism_between (S2,S3);

      then

      reconsider Af = (( FreeMSA X) | (S1,f,g)), 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;

        assume i in the carrier of S2;

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

      end;

      (( FreeMSA X) | (S1,f,g)) = ((( FreeMSA X) | (S2,f2,g2)) | (S1,f1,g1)) by A1, A2, Th27;

      then

      consider hf1 be 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 * f)), Af1 by RELAT_1: 36;

      reconsider hf1h = (hf1 ** hh) as ManySortedFunction of ( FreeMSA (X * f)), (( FreeMSA X) | (S1,f,g));

      

       A7: (X * f) = ((X * f2) * f1) by RELAT_1: 36;

       A8:

      now

        let s be SortSymbol of S1, x be Element of ((X * f) . s);

        reconsider t = ( root-tree [x, s]) as Term of S1, (X * f) by MSATERM: 4;

        

         A9: ( FreeMSA (X * f)) = MSAlgebra (# ( FreeSort (X * f)), ( FreeOper (X * f)) #) by MSAFREE:def 14;

        ( the_sort_of t) = s & (( FreeSort (X * f)) . s) = ( FreeSort ((X * f),s)) by MSAFREE:def 11, MSATERM: 14;

        then

         A10: ( root-tree [x, s]) in (the Sorts of ( FreeMSA (X * f)) . s) by A9, MSATERM:def 5;

        

         A11: ((X * f) . 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, (f . s)]) by FUNCT_2: 15;

      end;

      

       A12: (f,g) 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 * f)),Af) by A6, A7, MSUALG_3: 10;

      hence thesis by A12, A5, A8, Def5;

    end;