algspec1.miz



    begin

    theorem :: ALGSPEC1:1

    

     Th1: for f,g,h be Function st (( dom f) /\ ( dom g)) c= ( dom h) holds ((f +* g) +* h) = ((g +* f) +* h)

    proof

      let f,g,h be Function;

      

       A1: ( dom ((g +* f) +* h)) = (( dom (g +* f)) \/ ( dom h)) by FUNCT_4:def 1;

      

       A2: ( dom (f +* g)) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

      assume

       A3: (( dom f) /\ ( dom g)) c= ( dom h);

       A4:

      now

        let x be object;

        assume

         A5: x in ((( dom f) \/ ( dom g)) \/ ( dom h));

        per cases ;

          suppose

           A6: x in ( dom h);

          then (((f +* g) +* h) . x) = (h . x) by FUNCT_4: 13;

          hence (((f +* g) +* h) . x) = (((g +* f) +* h) . x) by A6, FUNCT_4: 13;

        end;

          suppose

           A7: not x in ( dom h);

          then not x in (( dom f) /\ ( dom g)) by A3;

          then

           A8: not x in ( dom f) or not x in ( dom g) by XBOOLE_0:def 4;

          

           A9: (((f +* g) +* h) . x) = ((f +* g) . x) by A7, FUNCT_4: 11;

          x in (( dom g) \/ ( dom f)) by A5, A7, XBOOLE_0:def 3;

          then x in ( dom f) or x in ( dom g) by XBOOLE_0:def 3;

          then ((f +* g) . x) = (f . x) & ((g +* f) . x) = (f . x) or ((f +* g) . x) = (g . x) & ((g +* f) . x) = (g . x) by A8, FUNCT_4: 11, FUNCT_4: 13;

          hence (((f +* g) +* h) . x) = (((g +* f) +* h) . x) by A7, A9, FUNCT_4: 11;

        end;

      end;

      

       A10: ( dom (g +* f)) = (( dom g) \/ ( dom f)) by FUNCT_4:def 1;

      ( dom ((f +* g) +* h)) = (( dom (f +* g)) \/ ( dom h)) by FUNCT_4:def 1;

      hence thesis by A1, A2, A10, A4;

    end;

    theorem :: ALGSPEC1:2

    

     Th2: for f,g,h be Function st f c= g & (( rng h) /\ ( dom g)) c= ( dom f) holds (g * h) = (f * h)

    proof

      let f,g,h be Function;

      assume that

       A1: f c= g and

       A2: (( rng h) /\ ( dom g)) c= ( dom f);

      

       A3: ( dom (f * h)) = ( dom (g * h))

      proof

        (f * h) c= (g * h) by A1, RELAT_1: 29;

        hence ( dom (f * h)) c= ( dom (g * h)) by RELAT_1: 11;

        let x be object;

        assume

         A4: x in ( dom (g * h));

        then

         A5: (h . x) in ( dom g) by FUNCT_1: 11;

        

         A6: x in ( dom h) by A4, FUNCT_1: 11;

        then (h . x) in ( rng h) by FUNCT_1:def 3;

        then (h . x) in (( rng h) /\ ( dom g)) by A5, XBOOLE_0:def 4;

        hence thesis by A2, A6, FUNCT_1: 11;

      end;

      now

        let x be object;

        assume

         A7: x in ( dom (f * h));

        then

         A8: x in ( dom h) by FUNCT_1: 11;

        then

         A9: ((g * h) . x) = (g . (h . x)) by FUNCT_1: 13;

        

         A10: ((f * h) . x) = (f . (h . x)) by A8, FUNCT_1: 13;

        (h . x) in ( dom f) by A7, FUNCT_1: 11;

        hence ((g * h) . x) = ((f * h) . x) by A1, A9, A10, GRFUNC_1: 2;

      end;

      hence thesis by A3;

    end;

    theorem :: ALGSPEC1:3

    

     Th3: for f,g,h be Function st ( dom f) misses ( rng h) & (g .: ( dom h)) misses ( dom f) holds (f * (g +* h)) = (f * g)

    proof

      let f,g,h be Function such that

       A1: ( dom f) misses ( rng h) and

       A2: (g .: ( dom h)) misses ( dom f);

      

       A3: ( dom (f * g)) = ( dom (f * (g +* h)))

      proof

        hereby

          let x be object;

          assume

           A4: x in ( dom (f * g));

          then

           A5: x in ( dom g) by FUNCT_1: 11;

          

           A6: (g . x) in ( dom f) by A4, FUNCT_1: 11;

          now

            assume x in ( dom h);

            then (g . x) in (g .: ( dom h)) by A5, FUNCT_1:def 6;

            hence contradiction by A2, A6, XBOOLE_0: 3;

          end;

          then

           A7: (g . x) = ((g +* h) . x) by FUNCT_4: 11;

          x in ( dom (g +* h)) by A5, FUNCT_4: 12;

          hence x in ( dom (f * (g +* h))) by A6, A7, FUNCT_1: 11;

        end;

        let x be object;

        assume

         A8: x in ( dom (f * (g +* h)));

        then x in ( dom (g +* h)) by FUNCT_1: 11;

        then x in ( dom g) & not x in ( dom h) or x in ( dom h) by FUNCT_4: 12;

        then

         A9: x in ( dom g) & ((g +* h) . x) = (g . x) or ((g +* h) . x) = (h . x) & (h . x) in ( rng h) by FUNCT_1:def 3, FUNCT_4: 11, FUNCT_4: 13;

        ((g +* h) . x) in ( dom f) by A8, FUNCT_1: 11;

        hence thesis by A1, A9, FUNCT_1: 11, XBOOLE_0: 3;

      end;

      now

        let x be object;

        assume

         A10: x in ( dom (f * g));

        then

         A11: x in ( dom g) by FUNCT_1: 11;

        

         A12: (g . x) in ( dom f) by A10, FUNCT_1: 11;

        now

          assume x in ( dom h);

          then (g . x) in (g .: ( dom h)) by A11, FUNCT_1:def 6;

          hence contradiction by A2, A12, XBOOLE_0: 3;

        end;

        then

         A13: (g . x) = ((g +* h) . x) by FUNCT_4: 11;

        x in ( dom (g +* h)) by A11, FUNCT_4: 12;

        

        hence ((f * (g +* h)) . x) = (f . (g . x)) by A13, FUNCT_1: 13

        .= ((f * g) . x) by A11, FUNCT_1: 13;

      end;

      hence thesis by A3;

    end;

    theorem :: ALGSPEC1:4

    

     Th4: for f1,f2,g1,g2 be Function st f1 tolerates f2 & g1 tolerates g2 holds (f1 * g1) tolerates (f2 * g2)

    proof

      let f1,f2,g1,g2 be Function such that

       A1: for x be object st x in (( dom f1) /\ ( dom f2)) holds (f1 . x) = (f2 . x) and

       A2: for x be object st x in (( dom g1) /\ ( dom g2)) holds (g1 . x) = (g2 . x);

      let x be object;

      assume

       A3: x in (( dom (f1 * g1)) /\ ( dom (f2 * g2)));

      then

       A4: x in ( dom (f1 * g1)) by XBOOLE_0:def 4;

      then

       A5: x in ( dom g1) by FUNCT_1: 11;

      then

       A6: ((f1 * g1) . x) = (f1 . (g1 . x)) by FUNCT_1: 13;

      

       A7: x in ( dom (f2 * g2)) by A3, XBOOLE_0:def 4;

      then

       A8: x in ( dom g2) by FUNCT_1: 11;

      then

       A9: ((f2 * g2) . x) = (f2 . (g2 . x)) by FUNCT_1: 13;

      x in (( dom g1) /\ ( dom g2)) by A5, A8, XBOOLE_0:def 4;

      then

       A10: (g1 . x) = (g2 . x) by A2;

      

       A11: (g2 . x) in ( dom f2) by A7, FUNCT_1: 11;

      (g1 . x) in ( dom f1) by A4, FUNCT_1: 11;

      then (g1 . x) in (( dom f1) /\ ( dom f2)) by A11, A10, XBOOLE_0:def 4;

      hence thesis by A1, A10, A6, A9;

    end;

    theorem :: ALGSPEC1:5

    

     Th5: for X1,Y1,X2,Y2 be non empty set holds for f be Function of X1, X2, g be Function of Y1, Y2 st f c= g holds (f * ) c= (g * )

    proof

      let X1,Y1,X2,Y2 be non empty set;

      let f be Function of X1, X2, g be Function of Y1, Y2;

      

       A1: ( dom g) = Y1 by FUNCT_2:def 1;

      assume

       A2: f c= g;

      

       A3: ( dom f) = X1 by FUNCT_2:def 1;

      then

       A4: (X1 * ) c= (Y1 * ) by A1, A2, FINSEQ_1: 62, RELAT_1: 11;

       A5:

      now

        let x be object;

        assume x in (X1 * );

        then

        reconsider p = x as Element of (X1 * );

        

         A6: ((f * ) . p) = (f * p) by LANG1:def 13;

        (( rng p) /\ Y1) c= X1;

        then

         A7: (f * p) = (g * p) by A3, A1, A2, Th2;

        p in (X1 * );

        hence ((f * ) . x) = ((g * ) . x) by A4, A6, A7, LANG1:def 13;

      end;

      

       A8: ( dom (g * )) = (Y1 * ) by FUNCT_2:def 1;

      ( dom (f * )) = (X1 * ) by FUNCT_2:def 1;

      hence thesis by A8, A4, A5, GRFUNC_1: 2;

    end;

    theorem :: ALGSPEC1:6

    

     Th6: for X1,Y1,X2,Y2 be non empty set holds for f be Function of X1, X2, g be Function of Y1, Y2 st f tolerates g holds (f * ) tolerates (g * )

    proof

      let X1,Y1,X2,Y2 be non empty set;

      let f be Function of X1, X2, g be Function of Y1, Y2;

      

       A1: ( dom g) = Y1 by FUNCT_2:def 1;

      assume

       A2: for x be object st x in (( dom f) /\ ( dom g)) holds (f . x) = (g . x);

      let x be object;

      assume

       A3: x in (( dom (f * )) /\ ( dom (g * )));

      then

      reconsider q = x as Element of (Y1 * );

      

       A4: ((g * ) . x) = (g * q) by LANG1:def 13;

      x in ( dom (f * )) by A3, XBOOLE_0:def 4;

      then

      reconsider p = x as Element of (X1 * );

      

       A5: ( dom f) = X1 by FUNCT_2:def 1;

       A6:

      now

        let i be object;

        assume

         A7: i in ( dom p);

        then

         A8: (q . i) in ( rng q) by FUNCT_1:def 3;

        (p . i) in ( rng p) by A7, FUNCT_1:def 3;

        then (p . i) in (( dom f) /\ ( dom g)) by A5, A1, A8, XBOOLE_0:def 4;

        

        then (f . (p . i)) = (g . (q . i)) by A2

        .= ((g * q) . i) by A7, FUNCT_1: 13;

        hence ((f * p) . i) = ((g * q) . i) by A7, FUNCT_1: 13;

      end;

      ( rng q) c= Y1;

      then

       A9: ( dom (g * q)) = ( dom q) by A1, RELAT_1: 27;

      ( rng p) c= X1;

      then

       A10: ( dom (f * p)) = ( dom p) by A5, RELAT_1: 27;

      ((f * ) . x) = (f * p) by LANG1:def 13;

      hence thesis by A4, A10, A9, A6;

    end;

    definition

      let X be set, f be Function;

      :: ALGSPEC1:def1

      func X -indexing (f) -> ManySortedSet of X equals (( id X) +* (f | X));

      coherence

      proof

        ( dom ( id X)) = X;

        then ( dom (( id X) +* (f | X))) = (X \/ ( dom (f | X))) by FUNCT_4:def 1;

        then ( dom (( id X) +* (f | X))) = X by RELAT_1: 58, XBOOLE_1: 12;

        hence thesis by PARTFUN1:def 2, RELAT_1:def 18;

      end;

    end

    theorem :: ALGSPEC1:7

    

     Th7: for X be set, f be Function holds ( rng (X -indexing f)) = ((X \ ( dom f)) \/ (f .: X))

    proof

      let X be set, f be Function;

      ( dom ( id X)) = X;

      

      hence ( rng (X -indexing f)) = ((( id X) .: (X \ ( dom (f | X)))) \/ ( rng (f | X))) by FRECHET: 12

      .= ((( id X) .: (X \ ( dom (f | X)))) \/ (f .: X)) by RELAT_1: 115

      .= ((X \ ( dom (f | X))) \/ (f .: X)) by FUNCT_1: 92

      .= ((X \ (( dom f) /\ X)) \/ (f .: X)) by RELAT_1: 61

      .= ((X \ ( dom f)) \/ (f .: X)) by XBOOLE_1: 47;

    end;

    theorem :: ALGSPEC1:8

    

     Th8: for X be non empty set, f be Function, x be Element of X holds ((X -indexing f) . x) = ((( id X) +* f) . x)

    proof

      let X be non empty set, f be Function, x be Element of X;

      ((( id X) +* f) | X) = ((( id X) | X) +* (f | X)) by FUNCT_4: 71

      .= ((( id X) | ( dom ( id X))) +* (f | X))

      .= (X -indexing f);

      hence thesis by FUNCT_1: 49;

    end;

    theorem :: ALGSPEC1:9

    

     Th9: for X,x be set, f be Function st x in X holds (x in ( dom f) implies ((X -indexing f) . x) = (f . x)) & ( not x in ( dom f) implies ((X -indexing f) . x) = x)

    proof

      let X,x be set, f be Function;

      assume

       A1: x in X;

      then

       A2: (( id X) . x) = x by FUNCT_1: 18;

      ((X -indexing f) . x) = ((( id X) +* f) . x) by A1, Th8;

      hence thesis by A2, FUNCT_4: 11, FUNCT_4: 13;

    end;

    theorem :: ALGSPEC1:10

    

     Th10: for X be set, f be Function st ( dom f) = X holds (X -indexing f) = f

    proof

      let X be set, f be Function;

      

       A1: ( dom ( id X)) = X;

      assume

       A2: ( dom f) = X;

      thus thesis by A2, A1, FUNCT_4: 19;

    end;

    theorem :: ALGSPEC1:11

    

     Th11: for X be set, f be Function holds (X -indexing (X -indexing f)) = (X -indexing f)

    proof

      let X be set, f be Function;

      ( dom (X -indexing f)) = X by PARTFUN1:def 2;

      then for x be object st x in X holds ((X -indexing (X -indexing f)) . x) = ((X -indexing f) . x) by Th9;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: ALGSPEC1:12

    

     Th12: for X be set, f be Function holds (X -indexing (( id X) +* f)) = (X -indexing f)

    proof

      let X be set, f be Function;

      

      thus (X -indexing (( id X) +* f)) = (( id X) +* ((( id X) | X) +* (f | X))) by FUNCT_4: 71

      .= (( id X) +* (( id X) +* (f | X)))

      .= ((( id X) +* ( id X)) +* (f | X)) by FUNCT_4: 14

      .= (X -indexing f);

    end;

    theorem :: ALGSPEC1:13

    for X be set, f be Function st f c= ( id X) holds (X -indexing f) = ( id X)

    proof

      let X be set, f be Function;

      assume f c= ( id X);

      then (( id X) +* f) = ( id X) by FUNCT_4: 98;

      

      hence (X -indexing f) = (X -indexing ( id X)) by Th12

      .= ( id X);

    end;

    theorem :: ALGSPEC1:14

    for X be set holds (X -indexing {} ) = ( id X);

    theorem :: ALGSPEC1:15

    for X be set, f be Function st X c= ( dom f) holds (X -indexing f) = (f | X)

    proof

      let X be set, f be Function;

      assume X c= ( dom f);

      then

       A1: ( dom (f | X)) = X by RELAT_1: 62;

      

      thus (X -indexing f) = (X -indexing (f | X))

      .= (f | X) by A1, Th10;

    end;

    theorem :: ALGSPEC1:16

    for f be Function holds ( {} -indexing f) = {} ;

    theorem :: ALGSPEC1:17

    

     Th17: for X,Y be set, f be Function st X c= Y holds ((Y -indexing f) | X) = (X -indexing f)

    proof

      let X,Y be set, f be Function;

      assume

       A1: X c= Y;

      then

       A2: ((f | Y) | X) = (f | X) by RELAT_1: 74;

      (( id Y) | X) = ( id X) by A1, FUNCT_3: 1;

      hence thesis by A2, FUNCT_4: 71;

    end;

    theorem :: ALGSPEC1:18

    

     Th18: for X,Y be set, f be Function holds ((X \/ Y) -indexing f) = ((X -indexing f) +* (Y -indexing f))

    proof

      let X,Y be set, f be Function;

      set Z = (X \/ Y);

      

       A1: (f | Y) c= f by RELAT_1: 59;

      (f | X) c= f by RELAT_1: 59;

      then (f | X) tolerates (f | Y) by A1, PARTFUN1: 52;

      then

       A2: ((f | X) \/ (f | Y)) = ((f | X) +* (f | Y)) by FUNCT_4: 30;

      ( dom (f | X)) = (( dom f) /\ X) by RELAT_1: 61;

      then

       A3: ( dom (f | X)) c= ( dom f) by XBOOLE_1: 17;

      ( dom (f | Y)) = (( dom f) /\ Y) by RELAT_1: 61;

      then

       A4: (( dom (f | X)) /\ ( dom ( id Y))) c= ( dom (f | Y)) by A3, XBOOLE_1: 27;

      

      thus (Z -indexing f) = ((( id X) +* ( id Y)) +* (f | Z)) by FUNCT_4: 22

      .= ((( id X) +* ( id Y)) +* ((f | X) +* (f | Y))) by A2, RELAT_1: 78

      .= (( id X) +* (( id Y) +* ((f | X) +* (f | Y)))) by FUNCT_4: 14

      .= (( id X) +* ((( id Y) +* (f | X)) +* (f | Y))) by FUNCT_4: 14

      .= (( id X) +* (((f | X) +* ( id Y)) +* (f | Y))) by A4, Th1

      .= (( id X) +* ((f | X) +* (( id Y) +* (f | Y)))) by FUNCT_4: 14

      .= ((X -indexing f) +* (Y -indexing f)) by FUNCT_4: 14;

    end;

    theorem :: ALGSPEC1:19

    

     Th19: for X,Y be set, f be Function holds (X -indexing f) tolerates (Y -indexing f)

    proof

      let X,Y be set, f be Function;

      (Y -indexing f) = (((X \/ Y) -indexing f) | Y) by Th17, XBOOLE_1: 7;

      then

       A1: (Y -indexing f) c= ((X \/ Y) -indexing f) by RELAT_1: 59;

      (X -indexing f) = (((X \/ Y) -indexing f) | X) by Th17, XBOOLE_1: 7;

      then (X -indexing f) c= ((X \/ Y) -indexing f) by RELAT_1: 59;

      hence thesis by A1, PARTFUN1: 52;

    end;

    theorem :: ALGSPEC1:20

    

     Th20: for X,Y be set, f be Function holds ((X \/ Y) -indexing f) = ((X -indexing f) \/ (Y -indexing f))

    proof

      let X,Y be set, f be Function;

      

       A1: (X -indexing f) tolerates (Y -indexing f) by Th19;

      ((X \/ Y) -indexing f) = ((X -indexing f) +* (Y -indexing f)) by Th18;

      hence thesis by A1, FUNCT_4: 30;

    end;

    theorem :: ALGSPEC1:21

    

     Th21: for X be non empty set, f,g be Function st ( rng g) c= X holds ((X -indexing f) * g) = ((( id X) +* f) * g)

    proof

      let X be non empty set, f,g be Function such that

       A1: ( rng g) c= X;

      ( rng g) c= ( dom (X -indexing f)) by A1, PARTFUN1:def 2;

      then

       A2: ( dom ((X -indexing f) * g)) = ( dom g) by RELAT_1: 27;

       A3:

      now

        let x be object;

        assume

         A4: x in ( dom g);

        then

         A5: (((( id X) +* f) * g) . x) = ((( id X) +* f) . (g . x)) by FUNCT_1: 13;

        

         A6: (g . x) in ( rng g) by A4, FUNCT_1:def 3;

        (((X -indexing f) * g) . x) = ((X -indexing f) . (g . x)) by A4, FUNCT_1: 13;

        hence (((X -indexing f) * g) . x) = (((( id X) +* f) * g) . x) by A1, A5, A6, Th8;

      end;

      ( dom ( id X)) = X;

      then

       A7: ( dom (( id X) +* f)) = (X \/ ( dom f)) by FUNCT_4:def 1;

      X c= (X \/ ( dom f)) by XBOOLE_1: 7;

      then ( dom ((( id X) +* f) * g)) = ( dom g) by A1, A7, RELAT_1: 27, XBOOLE_1: 1;

      hence thesis by A2, A3;

    end;

    theorem :: ALGSPEC1:22

    for f,g be Function st ( dom f) misses ( dom g) & ( rng g) misses ( dom f) holds for X be set holds (f * (X -indexing g)) = (f | X)

    proof

      let f,g be Function such that

       A1: ( dom f) misses ( dom g) and

       A2: ( rng g) misses ( dom f);

      let X be set;

      

       A3: ( dom (f | X)) c= ( dom f) by RELAT_1: 60;

      

       A4: (( id X) .: ( dom (g | X))) c= ( dom (g | X))

      proof

        let x be object;

        assume x in (( id X) .: ( dom (g | X)));

        then ex y be object st y in ( dom ( id X)) & y in ( dom (g | X)) & x = (( id X) . y) by FUNCT_1:def 6;

        hence thesis by FUNCT_1: 18;

      end;

      ( dom (g | X)) c= ( dom g) by RELAT_1: 60;

      then ( dom (f | X)) misses ( dom (g | X)) by A1, A3, XBOOLE_1: 64;

      then

       A5: (( id X) .: ( dom (g | X))) misses ( dom (f | X)) by A4, XBOOLE_1: 64;

      

       A6: ( dom (f | X)) c= X by RELAT_1: 58;

      ( rng (g | X)) c= ( rng g) by RELAT_1: 70;

      then

       A7: ( dom (f | X)) misses ( rng (g | X)) by A2, A3, XBOOLE_1: 64;

      (g .: X) c= ( rng g) by RELAT_1: 111;

      then (g .: X) misses ( dom f) by A2, XBOOLE_1: 64;

      then

       A8: ((g .: X) /\ ( dom f)) = {} ;

      ( rng (X -indexing g)) = ((X \ ( dom g)) \/ (g .: X)) by Th7;

      

      then (( rng (X -indexing g)) /\ ( dom f)) = (((X \ ( dom g)) /\ ( dom f)) \/ ((g .: X) /\ ( dom f))) by XBOOLE_1: 23

      .= ((X \ ( dom g)) /\ ( dom f)) by A8;

      then (( rng (X -indexing g)) /\ ( dom f)) c= (X /\ ( dom f)) by XBOOLE_1: 26;

      then (( rng (X -indexing g)) /\ ( dom f)) c= ( dom (f | X)) by RELAT_1: 61;

      

      hence (f * (X -indexing g)) = ((f | X) * (( id X) +* (g | X))) by Th2, RELAT_1: 59

      .= ((f | X) * ( id X)) by A7, A5, Th3

      .= (f | X) by A6, RELAT_1: 51;

    end;

    definition

      let f be Function;

      :: ALGSPEC1:def2

      mode rng-retract of f -> Function means

      : Def2: ( dom it ) = ( rng f) & (f * it ) = ( id ( rng f));

      existence

      proof

        defpred P[ object, object] means (f . $2) = $1;

        

         A1: for o be object st o in ( rng f) holds ex y be object st y in ( dom f) & P[o, y] by FUNCT_1:def 3;

        consider g be Function such that

         A2: ( dom g) = ( rng f) & ( rng g) c= ( dom f) and

         A3: for o be object st o in ( rng f) holds P[o, (g . o)] from FUNCT_1:sch 6( A1);

         A4:

        now

          let x be object;

          assume

           A5: x in ( rng f);

          then

           A6: ((f * g) . x) = (f . (g . x)) by A2, FUNCT_1: 13;

          (f . (g . x)) = x by A3, A5;

          hence ((f * g) . x) = (( id ( rng f)) . x) by A5, A6, FUNCT_1: 18;

        end;

        take g;

        thus ( dom g) = ( rng f) by A2;

        ( dom (f * g)) = ( rng f) by A2, RELAT_1: 27;

        hence thesis by A4;

      end;

    end

    theorem :: ALGSPEC1:23

    

     Th23: for f be Function, g be rng-retract of f holds ( rng g) c= ( dom f)

    proof

      let f,g be Function;

      assume that

       A1: ( dom g) = ( rng f) and

       A2: (f * g) = ( id ( rng f));

      ( dom g) = ( dom (f * g)) by A1, A2;

      hence thesis by FUNCT_1: 15;

    end;

    theorem :: ALGSPEC1:24

    

     Th24: for f be Function, g be rng-retract of f holds for x be set st x in ( rng f) holds (g . x) in ( dom f) & (f . (g . x)) = x

    proof

      let f be Function, g be rng-retract of f, x be set such that

       A1: x in ( rng f);

      

       A2: ( rng g) c= ( dom f) by Th23;

      

       A3: ( dom g) = ( rng f) by Def2;

      then (g . x) in ( rng g) by A1, FUNCT_1:def 3;

      hence (g . x) in ( dom f) by A2;

      

      thus (f . (g . x)) = ((f * g) . x) by A1, A3, FUNCT_1: 13

      .= (( id ( rng f)) . x) by Def2

      .= x by A1, FUNCT_1: 18;

    end;

    theorem :: ALGSPEC1:25

    for f be Function st f is one-to-one holds (f " ) is rng-retract of f

    proof

      let f be Function;

      assume f is one-to-one;

      hence ( dom (f " )) = ( rng f) & (f * (f " )) = ( id ( rng f)) by FUNCT_1: 32, FUNCT_1: 39;

    end;

    theorem :: ALGSPEC1:26

    for f be Function st f is one-to-one holds for g be rng-retract of f holds g = (f " )

    proof

      let f be Function such that

       A1: f is one-to-one;

      let g be rng-retract of f;

      

       A2: ( rng f) = ( dom g) by Def2;

      

       A3: ( rng g) = ( dom f)

      proof

        thus ( rng g) c= ( dom f) by Th23;

        let x be object;

        assume

         A4: x in ( dom f);

        then

         A5: (f . x) in ( rng f) by FUNCT_1:def 3;

        then

         A6: (g . (f . x)) in ( dom f) by Th24;

        (f . (g . (f . x))) = (f . x) by A5, Th24;

        then x = (g . (f . x)) by A1, A4, A6;

        hence thesis by A2, A5, FUNCT_1:def 3;

      end;

      now

        let x,y be object;

        assume that

         A7: x in ( dom f) and

         A8: y in ( dom g);

        

         A9: (g . y) in ( rng g) by A8, FUNCT_1:def 3;

        (f . (g . y)) = y by A2, A8, Th24;

        hence (f . x) = y iff (g . y) = x by A1, A3, A7, A9;

      end;

      hence thesis by A1, A2, A3, FUNCT_1: 38;

    end;

    theorem :: ALGSPEC1:27

    

     Th27: for f1,f2 be Function st f1 tolerates f2 holds for g1 be rng-retract of f1, g2 be rng-retract of f2 holds (g1 +* g2) is rng-retract of (f1 +* f2)

    proof

      let f1,f2 be Function;

      assume

       A1: f1 tolerates f2;

      then

       A2: (f1 +* f2) = (f1 \/ f2) by FUNCT_4: 30;

      let g1 be rng-retract of f1, g2 be rng-retract of f2;

      

       A3: ( dom g1) = ( rng f1) by Def2;

      

       A4: ( dom g2) = ( rng f2) by Def2;

      

      thus ( dom (g1 +* g2)) = (( dom g1) \/ ( dom g2)) by FUNCT_4:def 1

      .= ( rng (f1 +* f2)) by A2, A3, A4, RELAT_1: 12;

      

       A5: ( rng g2) c= ( dom f2) by Th23;

      ( rng g1) c= ( dom f1) by Th23;

      

      hence ((f1 +* f2) * (g1 +* g2)) = ((f1 * g1) +* (f2 * g2)) by A1, A5, FUNCT_4: 69

      .= (( id ( rng f1)) +* (f2 * g2)) by Def2

      .= (( id ( rng f1)) +* ( id ( rng f2))) by Def2

      .= ( id (( rng f1) \/ ( rng f2))) by FUNCT_4: 22

      .= ( id ( rng (f1 +* f2))) by A2, RELAT_1: 12;

    end;

    theorem :: ALGSPEC1:28

    for f1,f2 be Function st f1 c= f2 holds for g1 be rng-retract of f1 holds ex g2 be rng-retract of f2 st g1 c= g2

    proof

      let f1,f2 be Function such that

       A1: f1 c= f2;

      

       A2: (f2 +* f1) = f2 by A1, FUNCT_4: 98;

      set g = the rng-retract of f2;

      let g1 be rng-retract of f1;

      f1 tolerates f2 by A1, PARTFUN1: 52;

      then

      reconsider g2 = (g +* g1) as rng-retract of f2 by A2, Th27;

      take g2;

      thus thesis by FUNCT_4: 25;

    end;

    begin

    definition

      let S be non empty non void ManySortedSign;

      let f,g be Function;

      :: ALGSPEC1:def3

      pred f,g form_a_replacement_in S means for o1,o2 be OperSymbol of S st ((( id the carrier' of S) +* g) . o1) = ((( id the carrier' of S) +* g) . o2) holds ((( id the carrier of S) +* f) * ( the_arity_of o1)) = ((( id the carrier of S) +* f) * ( the_arity_of o2)) & ((( id the carrier of S) +* f) . ( the_result_sort_of o1)) = ((( id the carrier of S) +* f) . ( the_result_sort_of o2));

    end

    theorem :: ALGSPEC1:29

    

     Th29: for S be non empty non void ManySortedSign, f,g be Function holds (f,g) form_a_replacement_in S iff for o1,o2 be OperSymbol of S st ((the carrier' of S -indexing g) . o1) = ((the carrier' of S -indexing g) . o2) holds ((the carrier of S -indexing f) * ( the_arity_of o1)) = ((the carrier of S -indexing f) * ( the_arity_of o2)) & ((the carrier of S -indexing f) . ( the_result_sort_of o1)) = ((the carrier of S -indexing f) . ( the_result_sort_of o2))

    proof

      let S be non empty non void ManySortedSign;

      let f,g be Function;

      hereby

        assume

         A1: (f,g) form_a_replacement_in S;

        let o1,o2 be OperSymbol of S;

        

         A2: ( rng ( the_arity_of o1)) c= the carrier of S;

        

         A3: ( rng ( the_arity_of o2)) c= the carrier of S;

        assume ((the carrier' of S -indexing g) . o1) = ((the carrier' of S -indexing g) . o2);

        

        then

         A4: ((( id the carrier' of S) +* g) . o1) = ((the carrier' of S -indexing g) . o2) by Th8

        .= ((( id the carrier' of S) +* g) . o2) by Th8;

        then ((( id the carrier of S) +* f) * ( the_arity_of o1)) = ((( id the carrier of S) +* f) * ( the_arity_of o2)) by A1;

        

        hence ((the carrier of S -indexing f) * ( the_arity_of o1)) = ((( id the carrier of S) +* f) * ( the_arity_of o2)) by A2, Th21

        .= ((the carrier of S -indexing f) * ( the_arity_of o2)) by A3, Th21;

        

        thus ((the carrier of S -indexing f) . ( the_result_sort_of o1)) = ((( id the carrier of S) +* f) . ( the_result_sort_of o1)) by Th8

        .= ((( id the carrier of S) +* f) . ( the_result_sort_of o2)) by A1, A4

        .= ((the carrier of S -indexing f) . ( the_result_sort_of o2)) by Th8;

      end;

      assume

       A5: for o1,o2 be OperSymbol of S st ((the carrier' of S -indexing g) . o1) = ((the carrier' of S -indexing g) . o2) holds ((the carrier of S -indexing f) * ( the_arity_of o1)) = ((the carrier of S -indexing f) * ( the_arity_of o2)) & ((the carrier of S -indexing f) . ( the_result_sort_of o1)) = ((the carrier of S -indexing f) . ( the_result_sort_of o2));

      let o1,o2 be OperSymbol of S;

      

       A6: ( rng ( the_arity_of o1)) c= the carrier of S;

      

       A7: ( rng ( the_arity_of o2)) c= the carrier of S;

      assume ((( id the carrier' of S) +* g) . o1) = ((( id the carrier' of S) +* g) . o2);

      

      then

       A8: ((the carrier' of S -indexing g) . o1) = ((( id the carrier' of S) +* g) . o2) by Th8

      .= ((the carrier' of S -indexing g) . o2) by Th8;

      then ((the carrier of S -indexing f) * ( the_arity_of o1)) = ((the carrier of S -indexing f) * ( the_arity_of o2)) by A5;

      

      hence ((( id the carrier of S) +* f) * ( the_arity_of o1)) = ((the carrier of S -indexing f) * ( the_arity_of o2)) by A6, Th21

      .= ((( id the carrier of S) +* f) * ( the_arity_of o2)) by A7, Th21;

      

      thus ((( id the carrier of S) +* f) . ( the_result_sort_of o1)) = ((the carrier of S -indexing f) . ( the_result_sort_of o1)) by Th8

      .= ((the carrier of S -indexing f) . ( the_result_sort_of o2)) by A5, A8

      .= ((( id the carrier of S) +* f) . ( the_result_sort_of o2)) by Th8;

    end;

    theorem :: ALGSPEC1:30

    

     Th30: for S be non empty non void ManySortedSign, f,g be Function holds (f,g) form_a_replacement_in S iff ((the carrier of S -indexing f),(the carrier' of S -indexing g)) form_a_replacement_in S

    proof

      let S be non empty non void ManySortedSign;

      let f,g be Function;

      (( id the carrier' of S) +* ( id the carrier' of S)) = ( id the carrier' of S);

      then

       A1: (( id the carrier' of S) +* (( id the carrier' of S) +* (g | the carrier' of S))) = (( id the carrier' of S) +* (g | the carrier' of S)) by FUNCT_4: 14;

      (( id the carrier of S) +* ( id the carrier of S)) = ( id the carrier of S);

      then

       A2: (( id the carrier of S) +* (( id the carrier of S) +* (f | the carrier of S))) = (( id the carrier of S) +* (f | the carrier of S)) by FUNCT_4: 14;

      (f,g) form_a_replacement_in S iff for o1,o2 be OperSymbol of S st ((the carrier' of S -indexing g) . o1) = ((the carrier' of S -indexing g) . o2) holds ((the carrier of S -indexing f) * ( the_arity_of o1)) = ((the carrier of S -indexing f) * ( the_arity_of o2)) & ((the carrier of S -indexing f) . ( the_result_sort_of o1)) = ((the carrier of S -indexing f) . ( the_result_sort_of o2)) by Th29;

      hence thesis by A1, A2;

    end;

    reserve S,S9 for non void Signature,

f,g for Function;

    theorem :: ALGSPEC1:31

    

     Th31: (f,g) form_morphism_between (S,S9) implies (f,g) form_a_replacement_in S

    proof

      

       A1: ( dom ( id the carrier of S)) = the carrier of S;

      

       A2: ( dom ( id the carrier' of S)) = the carrier' of S;

      assume

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

      then ( dom g) = the carrier' of S;

      then

       A4: (( id the carrier' of S) +* g) = g by A2, FUNCT_4: 19;

      let o1,o2 be OperSymbol of S;

      assume

       A5: ((( id the carrier' of S) +* g) . o1) = ((( id the carrier' of S) +* g) . o2);

      ( dom f) = the carrier of S by A3;

      then

       A6: (( id the carrier of S) +* f) = f by A1, FUNCT_4: 19;

      

      hence ((( id the carrier of S) +* f) * ( the_arity_of o1)) = (the Arity of S9 . (g . o1)) by A3

      .= ((( id the carrier of S) +* f) * ( the_arity_of o2)) by A3, A6, A4, A5;

      reconsider g9 = g as Function of the carrier' of S, the carrier' of S9 by A3, INSTALG1: 9;

      

      thus ((( id the carrier of S) +* f) . ( the_result_sort_of o1)) = ((f * the ResultSort of S) . o1) by A6, FUNCT_2: 15

      .= ((the ResultSort of S9 * g) . o1) by A3

      .= (the ResultSort of S9 . (g9 . o1)) by FUNCT_2: 15

      .= ((the ResultSort of S9 * g9) . o2) by A4, A5, FUNCT_2: 15

      .= ((f * the ResultSort of S) . o2) by A3

      .= ((( id the carrier of S) +* f) . ( the_result_sort_of o2)) by A6, FUNCT_2: 15;

    end;

    theorem :: ALGSPEC1:32

    (f, {} ) form_a_replacement_in S;

    theorem :: ALGSPEC1:33

    

     Th33: g is one-to-one & (the carrier' of S /\ ( rng g)) c= ( dom g) implies (f,g) form_a_replacement_in S

    proof

      assume that

       A1: g is one-to-one and

       A2: (the carrier' of S /\ ( rng g)) c= ( dom g);

      let o1,o2 be OperSymbol of S;

      assume

       A3: ((( id the carrier' of S) +* g) . o1) = ((( id the carrier' of S) +* g) . o2);

      

       A4: (( id the carrier' of S) . o1) = o1;

      

       A5: (( id the carrier' of S) . o2) = o2;

      per cases ;

        suppose

         A6: o1 in ( dom g);

        then

         A7: (g . o1) in ( rng g) by FUNCT_1:def 3;

        

         A8: ((( id the carrier' of S) +* g) . o1) = (g . o1) by A6, FUNCT_4: 13;

        then not o2 in ( dom g) implies (g . o1) = o2 by A3, A5, FUNCT_4: 11;

        then

         A9: not o2 in ( dom g) implies o2 in (the carrier' of S /\ ( rng g)) by A7, XBOOLE_0:def 4;

        then ((( id the carrier' of S) +* g) . o2) = (g . o2) by A2, FUNCT_4: 13;

        hence thesis by A1, A2, A3, A6, A8, A9;

      end;

        suppose

         A10: not o1 in ( dom g);

        then

         A11: not o1 in (the carrier' of S /\ ( rng g)) by A2;

        

         A12: ((( id the carrier' of S) +* g) . o1) = o1 by A4, A10, FUNCT_4: 11;

        then o2 in ( dom g) implies o1 = (g . o2) & (g . o2) in ( rng g) by A3, FUNCT_1:def 3, FUNCT_4: 13;

        hence thesis by A3, A5, A12, A11, FUNCT_4: 11, XBOOLE_0:def 4;

      end;

    end;

    theorem :: ALGSPEC1:34

    g is one-to-one & ( rng g) misses the carrier' of S implies (f,g) form_a_replacement_in S

    proof

      assume

       A1: g is one-to-one;

      assume ( rng g) misses the carrier' of S;

      then (the carrier' of S /\ ( rng g)) = {} ;

      then (the carrier' of S /\ ( rng g)) c= ( dom g);

      hence thesis by A1, Th33;

    end;

    registration

      let X be set, Y be non empty set;

      let a be Function of Y, (X * );

      let r be Function of Y, X;

      cluster ManySortedSign (# X, Y, a, r #) -> non void;

      coherence ;

    end

    definition

      let S be non empty non void ManySortedSign;

      let f,g be Function;

      :: ALGSPEC1:def4

      func S with-replacement (f,g) -> strict non empty non void ManySortedSign means

      : Def4: ((the carrier of S -indexing f),(the carrier' of S -indexing g)) form_morphism_between (S,it ) & the carrier of it = ( rng (the carrier of S -indexing f)) & the carrier' of it = ( rng (the carrier' of S -indexing g));

      uniqueness

      proof

        set g1 = (the carrier' of S -indexing g), g2 = g1;

        set f1 = (the carrier of S -indexing f), f2 = f1;

        let S1,S2 be strict non empty non void ManySortedSign;

        assume that

         A2: (f1,g1) form_morphism_between (S,S1) and

         A3: the carrier of S1 = ( rng f1) and

         A4: the carrier' of S1 = ( rng g1) and

         A5: (f2,g2) form_morphism_between (S,S2) and

         A6: the carrier of S2 = ( rng f2) and

         A7: the carrier' of S2 = ( rng g2);

        

         A8: the ResultSort of S1 = the ResultSort of S2

        proof

          thus the carrier' of S1 = the carrier' of S2 by A4, A7;

          let o be OperSymbol of S1;

          consider o1 be object such that

           A9: o1 in ( dom g1) and

           A10: o = (g1 . o1) by A4, FUNCT_1:def 3;

          consider o2 be object such that

           A11: o2 in ( dom g2) and

           A12: o = (g2 . o2) by A4, FUNCT_1:def 3;

          reconsider o1, o2 as OperSymbol of S by A9, A11;

          

          thus (the ResultSort of S1 . o) = ((the ResultSort of S1 * g1) . o1) by A9, A10, FUNCT_1: 13

          .= ((f1 * the ResultSort of S) . o1) by A2

          .= (f1 . ( the_result_sort_of o1)) by FUNCT_2: 15

          .= (f2 . ( the_result_sort_of o2)) by A1, A10, A12, Th29

          .= ((f2 * the ResultSort of S) . o2) by FUNCT_2: 15

          .= ((the ResultSort of S2 * g2) . o2) by A5

          .= (the ResultSort of S2 . o) by A11, A12, FUNCT_1: 13;

        end;

        the Arity of S1 = the Arity of S2

        proof

          thus the carrier' of S1 = the carrier' of S2 by A4, A7;

          let o be OperSymbol of S1;

          consider o2 be object such that

           A13: o2 in ( dom g2) and

           A14: o = (g2 . o2) by A4, FUNCT_1:def 3;

          reconsider o2 as OperSymbol of S by A13;

          

          thus (the Arity of S1 . o) = (f2 * ( the_arity_of o2)) by A2, A14

          .= (the Arity of S2 . o) by A5, A14;

        end;

        hence thesis by A3, A6, A8;

      end;

      existence

      proof

        set g9 = (the carrier' of S -indexing g), gg = g9;

        set f9 = (the carrier of S -indexing f), ff = f9;

        

         A15: ( dom g9) = the carrier' of S by PARTFUN1:def 2;

        reconsider X = ( rng f9), Y = ( rng g9) as non empty set;

        reconsider g9 as Function of the carrier' of S, Y by A15, FUNCT_2: 1;

        set G = the rng-retract of g9;

        

         A16: ( rng G) c= the carrier' of S by A15, Th23;

        ( dom G) = ( rng g9) by Def2;

        then

        reconsider G as Function of Y, the carrier' of S by A16, FUNCT_2:def 1, RELSET_1: 4;

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

        then

        reconsider f9 as Function of the carrier of S, X by FUNCT_2: 1;

        set r = ((f9 * the ResultSort of S) * G);

        take R = ManySortedSign (# X, Y, (((f9 * ) * the Arity of S) * G), r #);

        thus (ff,gg) form_morphism_between (S,R)

        proof

          thus ( dom ff) = the carrier of S & ( dom gg) = the carrier' of S by PARTFUN1:def 2;

          thus ( rng ff) c= the carrier of R & ( rng gg) c= the carrier' of R;

          now

            let x be OperSymbol of S;

            

             A17: (g9 . (G . (g9 . x))) = (g9 . x) by Th24;

            

            thus ((r * g9) . x) = (the ResultSort of R . (g9 . x)) by FUNCT_2: 15

            .= ((f9 * the ResultSort of S) . (G . (g9 . x))) by FUNCT_2: 15

            .= (f9 . ( the_result_sort_of (G . (g9 . x)))) by FUNCT_2: 15

            .= (f9 . ( the_result_sort_of x)) by A1, A17, Th29

            .= ((f9 * the ResultSort of S) . x) by FUNCT_2: 15;

          end;

          hence (ff * the ResultSort of S) = (the ResultSort of R * gg) by FUNCT_2: 63;

          let o be set, p be Function;

          assume that

           A18: o in the carrier' of S and

           A19: p = (the Arity of S . o);

          reconsider x = o as OperSymbol of S by A18;

          (g9 . (G . (g9 . x))) = (g9 . x) by Th24;

          then (f9 * ( the_arity_of x)) = (f9 * ( the_arity_of (G . (g9 . x)))) by A1, Th29;

          

          hence (ff * p) = ((f9 * ) . ( the_arity_of (G . (g9 . x)))) by A19, LANG1:def 13

          .= (((f9 * ) * the Arity of S) . (G . (g9 . x))) by FUNCT_2: 15

          .= (the Arity of R . (gg . o)) by FUNCT_2: 15;

        end;

        thus thesis;

      end;

    end

    theorem :: ALGSPEC1:35

    

     Th35: for S1,S2 be non void Signature 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 ((f * ) * the Arity of S1) = (the Arity of S2 * g)

    proof

      let S1,S2 be non void Signature;

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

      let g be Function;

      

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

      

       A2: ( dom ((f * ) * the Arity of S1)) = the carrier' of S1 by FUNCT_2:def 1;

      assume

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

      then

       A4: ( dom g) = the carrier' of S1;

      

       A5: ( dom the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;

       A6:

      now

        let c be object;

        assume

         A7: c in the carrier' of S1;

        then

         A8: (the Arity of S1 . c) in ( rng the Arity of S1) by A5, FUNCT_1:def 3;

        then

        reconsider p = (the Arity of S1 . c) as FinSequence of the carrier of S1 by FINSEQ_1:def 11;

        

        thus (((f * ) * the Arity of S1) . c) = ((f * ) . p) by A5, A7, FUNCT_1: 13

        .= (f * p) by A8, LANG1:def 13

        .= (the Arity of S2 . (g . c)) by A3, A7

        .= ((the Arity of S2 * g) . c) by A4, A7, FUNCT_1: 13;

      end;

      ( rng g) c= the carrier' of S2 by A3;

      then ( dom (the Arity of S2 * g)) = the carrier' of S1 by A4, A1, RELAT_1: 27;

      hence thesis by A2, A6;

    end;

    theorem :: ALGSPEC1:36

    

     Th36: (f,g) form_a_replacement_in S implies (the carrier of S -indexing f) is Function of the carrier of S, the carrier of (S with-replacement (f,g))

    proof

      assume (f,g) form_a_replacement_in S;

      then ((the carrier of S -indexing f),(the carrier' of S -indexing g)) form_morphism_between (S,(S with-replacement (f,g))) by Def4;

      hence thesis by INSTALG1: 9;

    end;

    theorem :: ALGSPEC1:37

    

     Th37: (f,g) form_a_replacement_in S implies for f9 be Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = (the carrier of S -indexing f) holds for g9 be rng-retract of (the carrier' of S -indexing g) holds the Arity of (S with-replacement (f,g)) = (((f9 * ) * the Arity of S) * g9)

    proof

      set ff = (the carrier of S -indexing f);

      set gg = (the carrier' of S -indexing g);

      set T = (S with-replacement (f,g));

      assume

       A1: (f,g) form_a_replacement_in S;

      then

       A2: (ff,gg) form_morphism_between (S,T) by Def4;

      let f9 be Function of the carrier of S, the carrier of (S with-replacement (f,g)) such that

       A3: f9 = (the carrier of S -indexing f);

      let g9 be rng-retract of gg;

      the carrier' of T = ( rng gg) by A1, Def4;

      

      hence the Arity of T = (the Arity of T * ( id ( rng gg))) by FUNCT_2: 17

      .= (the Arity of T * (gg * g9)) by Def2

      .= ((the Arity of T * gg) * g9) by RELAT_1: 36

      .= (((f9 * ) * the Arity of S) * g9) by A2, A3, Th35;

    end;

    theorem :: ALGSPEC1:38

    

     Th38: (f,g) form_a_replacement_in S implies for g9 be rng-retract of (the carrier' of S -indexing g) holds the ResultSort of (S with-replacement (f,g)) = (((the carrier of S -indexing f) * the ResultSort of S) * g9)

    proof

      set ff = (the carrier of S -indexing f);

      set gg = (the carrier' of S -indexing g);

      set T = (S with-replacement (f,g));

      assume

       A1: (f,g) form_a_replacement_in S;

      then

       A2: (ff,gg) form_morphism_between (S,T) by Def4;

      let g9 be rng-retract of gg;

      the carrier' of T = ( rng gg) by A1, Def4;

      

      hence the ResultSort of T = (the ResultSort of T * ( id ( rng gg))) by FUNCT_2: 17

      .= (the ResultSort of T * (gg * g9)) by Def2

      .= ((the ResultSort of T * gg) * g9) by RELAT_1: 36

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

    end;

    theorem :: ALGSPEC1:39

    

     Th39: (f,g) form_morphism_between (S,S9) implies (S with-replacement (f,g)) is Subsignature of S9

    proof

      set R = (S with-replacement (f,g));

      set F = ( id the carrier of R);

      set G = ( id the carrier' of R);

      set f9 = (the carrier of S -indexing f);

      set g9 = (the carrier' of S -indexing g);

      

       A1: ( dom the ResultSort of S9) = the carrier' of S9 by FUNCT_2:def 1;

      

       A2: ( dom the ResultSort of R) = the carrier' of R by FUNCT_2:def 1;

      assume

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

      then ( dom f) = the carrier of S;

      then

       A4: f9 = f by Th10;

      

       A5: (f,g) form_a_replacement_in S by A3, Th31;

      then

       A6: the carrier' of R = ( rng g9) by Def4;

      thus ( dom F) = the carrier of R & ( dom G) = the carrier' of R;

      ( dom g) = the carrier' of S by A3;

      then

       A7: g9 = g by Th10;

      

       A8: (f9,g9) form_morphism_between (S,R) by A5, Def4;

       A9:

      now

        let x be object;

        assume

         A10: x in the carrier' of R;

        then

        consider a be object such that

         A11: a in ( dom g) and

         A12: x = (g . a) by A6, A7, FUNCT_1:def 3;

        reconsider a as OperSymbol of S by A3, A11;

        (the ResultSort of R * g) = (f * the ResultSort of S) by A8, A4, A7;

        then

         A13: (the ResultSort of R . x) = ((f * the ResultSort of S) . a) by A11, A12, FUNCT_1: 13;

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

        then (the ResultSort of S9 . x) = ((f * the ResultSort of S) . a) by A11, A12, FUNCT_1: 13;

        hence (the ResultSort of R . x) = ((the ResultSort of S9 | the carrier' of R) . x) by A10, A13, FUNCT_1: 49;

      end;

      ( rng g) c= the carrier' of S9 by A3;

      then ( dom (the ResultSort of S9 | the carrier' of R)) = the carrier' of R by A6, A7, A1, RELAT_1: 62;

      then

       A14: the ResultSort of R = (the ResultSort of S9 | the carrier' of R) by A2, A9;

      the carrier of R = ( rng f9) by A5, Def4;

      hence ( rng F) c= the carrier of S9 & ( rng G) c= the carrier' of S9 by A3, A6, A4, A7;

      ( rng the ResultSort of R) c= the carrier of R;

      

      hence (F * the ResultSort of R) = the ResultSort of R by RELAT_1: 53

      .= (the ResultSort of S9 * G) by A14, RELAT_1: 65;

      let o be set, p be Function;

      assume that

       A15: o in the carrier' of R and

       A16: p = (the Arity of R . o);

      consider a be object such that

       A17: a in ( dom g) and

       A18: o = (g . a) by A6, A7, A15, FUNCT_1:def 3;

      reconsider a as OperSymbol of S by A3, A17;

      

       A19: (f * ( the_arity_of a)) = (the Arity of S9 . o) by A3, A18;

      p in (the carrier of R * ) by A15, A16, FUNCT_2: 5;

      then p is FinSequence of the carrier of R by FINSEQ_1:def 11;

      then

       A20: ( rng p) c= the carrier of R by FINSEQ_1:def 4;

      (f * ( the_arity_of a)) = p by A8, A4, A7, A16, A18;

      

      hence (F * p) = (the Arity of S9 . o) by A20, A19, RELAT_1: 53

      .= (the Arity of S9 . (G . o)) by A15, FUNCT_1: 18;

    end;

    theorem :: ALGSPEC1:40

    

     Th40: (f,g) form_a_replacement_in S iff ((the carrier of S -indexing f),(the carrier' of S -indexing g)) form_morphism_between (S,(S with-replacement (f,g))) by Th30, Th31, Def4;

    theorem :: ALGSPEC1:41

    

     Th41: ( dom f) c= the carrier of S & ( dom g) c= the carrier' of S & (f,g) form_a_replacement_in S implies ((( id the carrier of S) +* f),(( id the carrier' of S) +* g)) form_morphism_between (S,(S with-replacement (f,g)))

    proof

      assume that

       A1: ( dom f) c= the carrier of S and

       A2: ( dom g) c= the carrier' of S;

      

       A3: (the carrier' of S -indexing g) = (( id the carrier' of S) +* g) by A2, RELAT_1: 68;

      (the carrier of S -indexing f) = (( id the carrier of S) +* f) by A1, RELAT_1: 68;

      hence thesis by A3, Th40;

    end;

    theorem :: ALGSPEC1:42

    ( dom f) = the carrier of S & ( dom g) = the carrier' of S & (f,g) form_a_replacement_in S implies (f,g) form_morphism_between (S,(S with-replacement (f,g)))

    proof

      assume that

       A1: ( dom f) = the carrier of S and

       A2: ( dom g) = the carrier' of S;

      ( dom g) = ( dom ( id the carrier' of S)) by A2;

      then

       A3: (( id the carrier' of S) +* g) = g by FUNCT_4: 19;

      ( dom f) = ( dom ( id the carrier of S)) by A1;

      then (( id the carrier of S) +* f) = f by FUNCT_4: 19;

      hence thesis by A1, A2, A3, Th41;

    end;

    theorem :: ALGSPEC1:43

    

     Th43: (f,g) form_a_replacement_in S implies (S with-replacement ((the carrier of S -indexing f),g)) = (S with-replacement (f,g))

    proof

      set X = the carrier of S, Y = the carrier' of S;

      set S2 = (S with-replacement ((X -indexing f),g));

      

       A1: (X -indexing (X -indexing f)) = (X -indexing f) by Th11;

      assume

       A2: (f,g) form_a_replacement_in S;

      then ((X -indexing f),(Y -indexing g)) form_a_replacement_in S by Th30;

      then

       A3: ((X -indexing f),g) form_a_replacement_in S by A1, Th30;

      then

       A4: the carrier of S2 = ( rng (X -indexing f)) by A1, Def4;

      

       A5: the carrier' of S2 = ( rng (Y -indexing g)) by A3, Def4;

      ((X -indexing f),(Y -indexing g)) form_morphism_between (S,S2) by A1, A3, Def4;

      hence thesis by A2, A4, A5, Def4;

    end;

    theorem :: ALGSPEC1:44

    

     Th44: (f,g) form_a_replacement_in S implies (S with-replacement (f,(the carrier' of S -indexing g))) = (S with-replacement (f,g))

    proof

      set X = the carrier of S, Y = the carrier' of S;

      set S2 = (S with-replacement (f,(Y -indexing g)));

      

       A1: (Y -indexing (Y -indexing g)) = (Y -indexing g) by Th11;

      assume

       A2: (f,g) form_a_replacement_in S;

      then ((X -indexing f),(Y -indexing g)) form_a_replacement_in S by Th30;

      then

       A3: (f,(Y -indexing g)) form_a_replacement_in S by A1, Th30;

      then

       A4: the carrier' of S2 = ( rng (Y -indexing g)) by A1, Def4;

      

       A5: the carrier of S2 = ( rng (X -indexing f)) by A3, Def4;

      ((X -indexing f),(Y -indexing g)) form_morphism_between (S,S2) by A1, A3, Def4;

      hence thesis by A2, A5, A4, Def4;

    end;

    begin

    definition

      let S be Signature;

      :: ALGSPEC1:def5

      mode Extension of S -> Signature means

      : Def5: S is Subsignature of it ;

      existence

      proof

        take S;

        thus thesis by INSTALG1: 15;

      end;

    end

    theorem :: ALGSPEC1:45

    

     Th45: for S be Signature holds S is Extension of S

    proof

      let S be Signature;

      thus S is Subsignature of S by INSTALG1: 15;

    end;

    theorem :: ALGSPEC1:46

    

     Th46: for S1 be Signature, S2 be Extension of S1, S3 be Extension of S2 holds S3 is Extension of S1

    proof

      let S1 be Signature, S2 be Extension of S1, S3 be Extension of S2;

      

       A1: S2 is Subsignature of S3 by Def5;

      S1 is Subsignature of S2 by Def5;

      then S1 is Subsignature of S3 by A1, INSTALG1: 16;

      hence thesis by Def5;

    end;

    theorem :: ALGSPEC1:47

    

     Th47: for S1,S2 be non empty Signature st S1 tolerates S2 holds (S1 +* S2) is Extension of S1

    proof

      let S1,S2 be non empty Signature such that

       A1: the Arity of S1 tolerates the Arity of S2 and

       A2: the ResultSort of S1 tolerates the ResultSort of S2;

      set S = (S1 +* S2);

      the ResultSort of S = (the ResultSort of S1 +* the ResultSort of S2) by CIRCCOMB:def 2;

      then

       A3: the ResultSort of S1 c= the ResultSort of S by A2, FUNCT_4: 28;

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

      thus ( dom f1) = the carrier of S1 & ( dom g1) = the carrier' of S1;

      ( dom the ResultSort of S1) = the carrier' of S1 by FUNCT_2:def 1;

      then the ResultSort of S1 = (the ResultSort of S | the carrier' of S1) by A3, GRFUNC_1: 23;

      then

       A4: the ResultSort of S1 = (the ResultSort of S * g1) by RELAT_1: 65;

      

       A5: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by CIRCCOMB:def 2;

      

       A6: the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      thus ( rng f1) c= the carrier of S & ( rng g1) c= the carrier' of S by A6, A5, XBOOLE_1: 7;

      ( rng the ResultSort of S1) c= the carrier of S1;

      hence (f1 * the ResultSort of S1) = (the ResultSort of S * g1) by A4, RELAT_1: 53;

      let o be set, p be Function such that

       A7: o in the carrier' of S1 and

       A8: p = (the Arity of S1 . o);

      

       A9: ( dom the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;

      then p in ( rng the Arity of S1) by A7, A8, FUNCT_1:def 3;

      then p is FinSequence of the carrier of S1 by FINSEQ_1:def 11;

      then ( rng p) c= the carrier of S1 by FINSEQ_1:def 4;

      

      hence (f1 * p) = p by RELAT_1: 53

      .= ((the Arity of S1 +* the Arity of S2) . o) by A1, A7, A8, A9, FUNCT_4: 15

      .= (the Arity of S . o) by CIRCCOMB:def 2

      .= (the Arity of S . (g1 . o)) by A7, FUNCT_1: 18;

    end;

    theorem :: ALGSPEC1:48

    

     Th48: for S1,S2 be non empty Signature holds (S1 +* S2) is Extension of S2

    proof

      let S1,S2 be non empty Signature;

      set S = (S1 +* S2);

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

      thus ( dom f1) = the carrier of S2 & ( dom g1) = the carrier' of S2;

      

       A1: the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      

       A2: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by CIRCCOMB:def 2;

      thus ( rng f1) c= the carrier of S & ( rng g1) c= the carrier' of S by A1, A2, XBOOLE_1: 7;

      

       A3: the ResultSort of S = (the ResultSort of S1 +* the ResultSort of S2) by CIRCCOMB:def 2;

      ( dom the ResultSort of S2) = the carrier' of S2 by FUNCT_2:def 1;

      then the ResultSort of S2 = (the ResultSort of S | the carrier' of S2) by A3;

      then

       A4: the ResultSort of S2 = (the ResultSort of S * g1) by RELAT_1: 65;

      ( rng the ResultSort of S2) c= the carrier of S2;

      hence (f1 * the ResultSort of S2) = (the ResultSort of S * g1) by A4, RELAT_1: 53;

      let o be set, p be Function such that

       A5: o in the carrier' of S2 and

       A6: p = (the Arity of S2 . o);

      

       A7: ( dom the Arity of S2) = the carrier' of S2 by FUNCT_2:def 1;

      then p in ( rng the Arity of S2) by A5, A6, FUNCT_1:def 3;

      then p is FinSequence of the carrier of S2 by FINSEQ_1:def 11;

      then ( rng p) c= the carrier of S2 by FINSEQ_1:def 4;

      

      hence (f1 * p) = p by RELAT_1: 53

      .= ((the Arity of S1 +* the Arity of S2) . o) by A5, A6, A7, FUNCT_4: 13

      .= (the Arity of S . o) by CIRCCOMB:def 2

      .= (the Arity of S . (g1 . o)) by A5, FUNCT_1: 18;

    end;

    theorem :: ALGSPEC1:49

    

     Th49: for S1,S2,S be non empty ManySortedSign holds for f1,g1,f2,g2 be Function st f1 tolerates f2 & (f1,g1) form_morphism_between (S1,S) & (f2,g2) form_morphism_between (S2,S) holds ((f1 +* f2),(g1 +* g2)) form_morphism_between ((S1 +* S2),S)

    proof

      let S1,S2,E be non empty ManySortedSign;

      let f1,g1,f2,g2 be Function such that

       A1: f1 tolerates f2 and

       A2: ( dom f1) = the carrier of S1 and

       A3: ( dom g1) = the carrier' of S1 and

       A4: ( rng f1) c= the carrier of E and

       A5: ( rng g1) c= the carrier' of E and

       A6: (f1 * the ResultSort of S1) = (the ResultSort of E * g1) and

       A7: for o be set, p be Function st o in the carrier' of S1 & p = (the Arity of S1 . o) holds (f1 * p) = (the Arity of E . (g1 . o)) and

       A8: ( dom f2) = the carrier of S2 and

       A9: ( dom g2) = the carrier' of S2 and

       A10: ( rng f2) c= the carrier of E and

       A11: ( rng g2) c= the carrier' of E and

       A12: (f2 * the ResultSort of S2) = (the ResultSort of E * g2) and

       A13: for o be set, p be Function st o in the carrier' of S2 & p = (the Arity of S2 . o) holds (f2 * p) = (the Arity of E . (g2 . o));

      set f = (f1 +* f2), g = (g1 +* g2), S = (S1 +* S2);

      the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      hence ( dom f) = the carrier of S by A2, A8, FUNCT_4:def 1;

      

       A14: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by CIRCCOMB:def 2;

      hence ( dom g) = the carrier' of S by A3, A9, FUNCT_4:def 1;

      

       A15: ( rng f) c= (( rng f1) \/ ( rng f2)) by FUNCT_4: 17;

      (( rng f1) \/ ( rng f2)) c= the carrier of E by A4, A10, XBOOLE_1: 8;

      hence ( rng f) c= the carrier of E by A15;

      

       A16: ( rng g) c= (( rng g1) \/ ( rng g2)) by FUNCT_4: 17;

      (( rng g1) \/ ( rng g2)) c= the carrier' of E by A5, A11, XBOOLE_1: 8;

      hence ( rng g) c= the carrier' of E by A16;

      

       A17: ( rng the ResultSort of S1) c= the carrier of S1;

      

       A18: ( rng the ResultSort of S2) c= the carrier of S2;

      

       A19: ( dom the ResultSort of E) = the carrier' of E by FUNCT_2:def 1;

      (the ResultSort of S1 +* the ResultSort of S2) = the ResultSort of (S1 +* S2) by CIRCCOMB:def 2;

      

      hence (f * the ResultSort of S) = ((f1 * the ResultSort of S1) +* (f2 * the ResultSort of S2)) by A1, A2, A8, A17, A18, FUNCT_4: 69

      .= (the ResultSort of E * g) by A6, A11, A12, A19, FUNCT_7: 9;

      let o be set, p be Function such that

       A20: o in the carrier' of S and

       A21: p = (the Arity of S . o);

      

       A22: (the Arity of S1 +* the Arity of S2) = the Arity of (S1 +* S2) by CIRCCOMB:def 2;

      

       A23: ( dom the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;

      

       A24: ( dom the Arity of S2) = the carrier' of S2 by FUNCT_2:def 1;

      per cases ;

        suppose

         A25: o in the carrier' of S2;

        then

         A26: p = (the Arity of S2 . o) by A21, A22, A24, FUNCT_4: 13;

        then p in ( rng the Arity of S2) by A24, A25, FUNCT_1:def 3;

        then p is FinSequence of the carrier of S2 by FINSEQ_1:def 11;

        then ( rng p) c= ( dom f2) by A8, FINSEQ_1:def 4;

        then

         A27: ( dom (f2 * p)) = ( dom p) by RELAT_1: 27;

        

         A28: ( dom (f1 * p)) c= ( dom p) by RELAT_1: 25;

        

        thus (f * p) = ((f1 * p) +* (f2 * p)) by FUNCT_7: 10

        .= (f2 * p) by A28, A27, FUNCT_4: 19

        .= (the Arity of E . (g2 . o)) by A13, A25, A26

        .= (the Arity of E . (g . o)) by A9, A25, FUNCT_4: 13;

      end;

        suppose

         A29: not o in the carrier' of S2;

        

         A30: ( dom (f2 * p)) c= ( dom p) by RELAT_1: 25;

        

         A31: o in the carrier' of S1 by A14, A20, A29, XBOOLE_0:def 3;

        

         A32: p = (the Arity of S1 . o) by A21, A22, A24, A29, FUNCT_4: 11;

        then p in ( rng the Arity of S1) by A23, A31, FUNCT_1:def 3;

        then p is FinSequence of the carrier of S1 by FINSEQ_1:def 11;

        then ( rng p) c= ( dom f1) by A2, FINSEQ_1:def 4;

        then

         A33: ( dom (f1 * p)) = ( dom p) by RELAT_1: 27;

        

        thus (f * p) = ((f2 +* f1) * p) by A1, FUNCT_4: 34

        .= ((f2 * p) +* (f1 * p)) by FUNCT_7: 10

        .= (f1 * p) by A33, A30, FUNCT_4: 19

        .= (the Arity of E . (g1 . o)) by A7, A31, A32

        .= (the Arity of E . (g . o)) by A9, A29, FUNCT_4: 11;

      end;

    end;

    theorem :: ALGSPEC1:50

    for S1,S2,E be non empty Signature holds E is Extension of S1 & E is Extension of S2 iff S1 tolerates S2 & E is Extension of (S1 +* S2)

    proof

      let S1,S2,E be non empty Signature;

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

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

      

       A1: E is Extension of S1 & E is Extension of S2 implies S1 tolerates S2

      proof

        assume that

         A2: S1 is Subsignature of E and

         A3: S2 is Subsignature of E;

        

         A4: the Arity of S2 c= the Arity of E by A3, INSTALG1: 11;

        the Arity of S1 c= the Arity of E by A2, INSTALG1: 11;

        hence the Arity of S1 tolerates the Arity of S2 by A4, PARTFUN1: 52;

        

         A5: the ResultSort of S2 c= the ResultSort of E by A3, INSTALG1: 11;

        the ResultSort of S1 c= the ResultSort of E by A2, INSTALG1: 11;

        hence thesis by A5, PARTFUN1: 52;

      end;

      

       A6: the carrier of (S1 +* S2) = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      the carrier of S2 c= (the carrier of S1 \/ the carrier of S2) by XBOOLE_1: 7;

      then

       A7: f2 c= ( id (the carrier of S1 \/ the carrier of S2)) by FUNCT_4: 3;

      

       A8: the carrier' of (S1 +* S2) = (the carrier' of S1 \/ the carrier' of S2) by CIRCCOMB:def 2;

      the carrier of S1 c= (the carrier of S1 \/ the carrier of S2) by XBOOLE_1: 7;

      then f1 c= ( id (the carrier of S1 \/ the carrier of S2)) by FUNCT_4: 3;

      then

       A9: f1 tolerates f2 by A7, PARTFUN1: 52;

      E is Extension of S1 & E is Extension of S2 implies E is Extension of (S1 +* S2)

      proof

        assume that

         A10: (f1,g1) form_morphism_between (S1,E) and

         A11: (f2,g2) form_morphism_between (S2,E);

        ((f1 +* f2),(g1 +* g2)) form_morphism_between ((S1 +* S2),E) by A9, A10, A11, Th49;

        then (( id the carrier of (S1 +* S2)),(g1 +* g2)) form_morphism_between ((S1 +* S2),E) by A6, FUNCT_4: 22;

        hence (( id the carrier of (S1 +* S2)),( id the carrier' of (S1 +* S2))) form_morphism_between ((S1 +* S2),E) by A8, FUNCT_4: 22;

      end;

      hence E is Extension of S1 & E is Extension of S2 implies S1 tolerates S2 & E is Extension of (S1 +* S2) by A1;

      assume S1 tolerates S2;

      then

       A12: (S1 +* S2) is Extension of S1 by Th47;

      (S1 +* S2) is Extension of S2 by Th48;

      hence thesis by A12, Th46;

    end;

    registration

      let S be non empty Signature;

      cluster -> non empty for Extension of S;

      coherence

      proof

        set x = the Element of S;

        let E be Extension of S;

        S is Subsignature of E by Def5;

        then

         A1: the carrier of S c= the carrier of E by INSTALG1: 10;

        x in the carrier of S;

        hence the carrier of E is non empty by A1;

      end;

    end

    registration

      let S be non void Signature;

      cluster -> non void for Extension of S;

      coherence

      proof

        set x = the OperSymbol of S;

        let E be Extension of S;

        S is Subsignature of E by Def5;

        then

         A1: the carrier' of S c= the carrier' of E by INSTALG1: 10;

        x in the carrier' of S;

        hence the carrier' of E is non empty by A1;

      end;

    end

    theorem :: ALGSPEC1:51

    

     Th51: for S,T be Signature st S is empty holds T is Extension of S

    proof

      let S,T be Signature;

      assume

       A1: the carrier of S is empty;

      then the carrier' of S = {} by INSTALG1:def 1;

      then the Arity of S = {} ;

      then

       A2: the Arity of S c= the Arity of T;

      the ResultSort of S = {} by A1;

      then the ResultSort of S c= the ResultSort of T;

      hence S is Subsignature of T by A1, A2, INSTALG1: 13, XBOOLE_1: 2;

    end;

    registration

      let S be Signature;

      cluster non empty non void strict for Extension of S;

      existence

      proof

        set S9 = the non void strict Signature;

        per cases ;

          suppose S is empty;

          then S9 is Extension of S by Th51;

          hence thesis;

        end;

          suppose S is non empty;

          then

          reconsider S1 = S as non empty Signature;

          reconsider E = (S9 +* S1) as Extension of S by Th48;

          take E;

          thus the carrier of E is non empty;

          thus the carrier' of E is non empty;

          thus thesis;

        end;

      end;

    end

    theorem :: ALGSPEC1:52

    

     Th52: for S be non void Signature, E be Extension of S st (f,g) form_a_replacement_in E holds (f,g) form_a_replacement_in S

    proof

      let S be non void Signature, E be Extension of S;

      set f9 = (the carrier of E -indexing f);

      set g9 = (the carrier' of E -indexing g);

      set T = (E with-replacement (f,g));

      

       A1: S is Subsignature of E by Def5;

      then

       A2: (f9 | the carrier of S) = (the carrier of S -indexing f) by Th17, INSTALG1: 10;

      

       A3: (g9 | the carrier' of S) = (the carrier' of S -indexing g) by A1, Th17, INSTALG1: 10;

      assume (f,g) form_a_replacement_in E;

      then (f9,g9) form_morphism_between (E,T) by Th40;

      then ((f9 | the carrier of S),(g9 | the carrier' of S)) form_a_replacement_in S by A1, Th31, INSTALG1: 18;

      hence thesis by A2, A3, Th30;

    end;

    theorem :: ALGSPEC1:53

    for S be non void Signature, E be Extension of S st (f,g) form_a_replacement_in E holds (E with-replacement (f,g)) is Extension of (S with-replacement (f,g))

    proof

      let S be non void Signature, E be Extension of S;

      set f9 = (the carrier of E -indexing f);

      set g9 = (the carrier' of E -indexing g);

      set gg = (the carrier' of S -indexing g);

      set T = (E with-replacement (f,g));

      

       A1: (the carrier' of S -indexing gg) = gg by Th11;

      assume

       A2: (f,g) form_a_replacement_in E;

      then (f,g) form_a_replacement_in S by Th52;

      then ((the carrier of S -indexing f),gg) form_a_replacement_in S by Th30;

      then

       A3: (f,gg) form_a_replacement_in S by A1, Th30;

      

       A4: S is Subsignature of E by Def5;

      then

       A5: (g9 | the carrier' of S) = (the carrier' of S -indexing g) by Th17, INSTALG1: 10;

      (f9,g9) form_morphism_between (E,T) by A2, Th40;

      then

       A6: (S with-replacement ((f9 | the carrier of S),(g9 | the carrier' of S))) is Subsignature of T by A4, Th39, INSTALG1: 18;

      (f9 | the carrier of S) = (the carrier of S -indexing f) by A4, Th17, INSTALG1: 10;

      then (S with-replacement ((f9 | the carrier of S),(g9 | the carrier' of S))) = (S with-replacement (f,(the carrier' of S -indexing g))) by A3, A5, Th43;

      hence (S with-replacement (f,g)) is Subsignature of (E with-replacement (f,g)) by A2, A6, Th44, Th52;

    end;

    theorem :: ALGSPEC1:54

    for S1,S2 be non void Signature st S1 tolerates S2 holds for f,g be Function st (f,g) form_a_replacement_in (S1 +* S2) holds ((S1 +* S2) with-replacement (f,g)) = ((S1 with-replacement (f,g)) +* (S2 with-replacement (f,g)))

    proof

      let S1,S2 be non void Signature such that

       A1: S1 tolerates S2;

      

       A2: the ResultSort of S1 tolerates the ResultSort of S2 by A1;

      

       A3: ( rng the Arity of S2) c= (the carrier of S2 * );

      

       A4: ( rng the ResultSort of S2) c= the carrier of S2;

      

       A5: ( rng the ResultSort of S1) c= the carrier of S1;

      set S = (S1 +* S2);

      let f,g be Function such that

       A6: (f,g) form_a_replacement_in (S1 +* S2);

      deffunc F( non void Signature) = (the carrier of $1 -indexing f);

      deffunc T( non void Signature) = ($1 with-replacement (f,g));

      

       A7: ( dom F(S2)) = the carrier of S2 by PARTFUN1:def 2;

      

       A8: F(S1) tolerates F(S2) by Th19;

      

       A9: S is Extension of S1 by A1, Th47;

      then

      reconsider F1 = F(S1) as Function of the carrier of S1, the carrier of T(S1) by A6, Th36, Th52;

      

       A10: ( dom ( F(S1) * the ResultSort of S1)) = the carrier' of S1 by PARTFUN1:def 2;

      deffunc G( non void Signature) = (the carrier' of $1 -indexing g);

      

       A11: ( dom F(S1)) = the carrier of S1 by PARTFUN1:def 2;

      

       A12: ( dom G(S1)) = the carrier' of S1 by PARTFUN1:def 2;

      set g1 = the rng-retract of G(S1), g2 = the rng-retract of G(S2);

      

       A13: the ResultSort of S = (the ResultSort of S1 +* the ResultSort of S2) by CIRCCOMB:def 2;

      

       A14: ( rng g2) c= ( dom G(S2)) by Th23;

      

       A15: the carrier' of S = (the carrier' of S1 \/ the carrier' of S2) by CIRCCOMB:def 2;

      then G(S) = ( G(S1) \/ G(S2)) by Th20;

      then

       A16: ( rng G(S)) = (( rng G(S1)) \/ ( rng G(S2))) by RELAT_1: 12;

      

       A17: ( dom G(S2)) = the carrier' of S2 by PARTFUN1:def 2;

      

       A18: S is Extension of S2 by Th48;

      then

      reconsider F2 = F(S2) as Function of the carrier of S2, the carrier of T(S2) by A6, Th36, Th52;

      

       A19: ( dom ( F(S2) * the ResultSort of S2)) = the carrier' of S2 by PARTFUN1:def 2;

      

       A20: the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      then

       A21: F(S) = ( F(S1) +* F(S2)) by Th18;

       F(S) = ( F(S1) \/ F(S2)) by A20, Th20;

      then

       A22: ( rng F(S)) = (( rng F(S1)) \/ ( rng F(S2))) by RELAT_1: 12;

      

       A23: ( dom ((F2 * ) * the Arity of S2)) = the carrier' of S2 by FUNCT_2:def 1;

      

       A24: ( dom (F2 * )) = (the carrier of S2 * ) by FUNCT_2:def 1;

       G(S) = ( G(S1) +* G(S2)) by A15, Th18;

      then

      reconsider gg = (g1 +* g2) as rng-retract of G(S) by Th19, Th27;

      

       A25: ( rng g1) c= ( dom G(S1)) by Th23;

      

       A26: the ResultSort of T(S) = (( F(S) * the ResultSort of S) * gg) by A6, Th38

      .= ((( F(S1) * the ResultSort of S1) +* ( F(S2) * the ResultSort of S2)) * gg) by A13, A21, A5, A4, A11, A7, Th19, FUNCT_4: 69

      .= ((( F(S1) * the ResultSort of S1) * g1) +* (( F(S2) * the ResultSort of S2) * g2)) by A8, A25, A14, A12, A17, A10, A19, A2, Th4, FUNCT_4: 69

      .= (the ResultSort of T(S1) +* (( F(S2) * the ResultSort of S2) * g2)) by A6, A9, Th38, Th52

      .= (the ResultSort of T(S1) +* the ResultSort of T(S2)) by A6, A18, Th38, Th52;

      

       A27: the carrier of T(S) = ( rng F(S)) by A6, Def4;

      

       A28: ( dom ((F1 * ) * the Arity of S1)) = the carrier' of S1 by FUNCT_2:def 1;

      reconsider FS = F(S) as Function of the carrier of S, the carrier of T(S) by A6, Th36;

      

       A29: (( rng the Arity of S) /\ ( dom (FS * ))) c= ( rng the Arity of S) by XBOOLE_1: 17;

      

       A30: the Arity of S = (the Arity of S1 +* the Arity of S2) by CIRCCOMB:def 2;

      

       A31: (f,g) form_a_replacement_in S1 by A6, A9, Th52;

      then

       A32: the carrier of T(S1) = ( rng F(S1)) by Def4;

      

       A33: the carrier' of T(S1) = ( rng G(S1)) by A31, Def4;

      

       A34: the carrier' of T(S) = ( rng G(S)) by A6, Def4;

      

       A35: ( dom (F1 * )) = (the carrier of S1 * ) by FUNCT_2:def 1;

      the Arity of S1 tolerates the Arity of S2 by A1;

      then the Arity of S = (the Arity of S1 \/ the Arity of S2) by A30, FUNCT_4: 30;

      then ( rng the Arity of S) = (( rng the Arity of S1) \/ ( rng the Arity of S2)) by RELAT_1: 12;

      then ( rng the Arity of S) c= ((the carrier of S1 * ) \/ (the carrier of S2 * )) by XBOOLE_1: 13;

      then ( rng the Arity of S) c= ( dom ((F1 * ) +* (F2 * ))) by A35, A24, FUNCT_4:def 1;

      then

       A36: (( rng the Arity of S) /\ ( dom (FS * ))) c= ( dom ((F1 * ) +* (F2 * ))) by A29;

      

       A37: (f,g) form_a_replacement_in S2 by A6, A18, Th52;

      then

       A38: the carrier of T(S2) = ( rng F(S2)) by Def4;

      

       A39: the carrier' of T(S2) = ( rng G(S2)) by A37, Def4;

      

       A40: (F1 * ) tolerates (F2 * ) by Th6, Th19;

      

       A41: ((F1 * ) +* (F2 * )) c= ((F1 * ) \/ (F2 * )) by FUNCT_4: 29;

      F2 = (FS | the carrier of S2) by A20, Th17, XBOOLE_1: 7;

      then

       A42: (F2 * ) c= (FS * ) by Th5, RELAT_1: 59;

      F1 = (FS | the carrier of S1) by A20, Th17, XBOOLE_1: 7;

      then (F1 * ) c= (FS * ) by Th5, RELAT_1: 59;

      then ((F1 * ) \/ (F2 * )) c= (FS * ) by A42, XBOOLE_1: 8;

      then

       A43: ((F1 * ) +* (F2 * )) c= (FS * ) by A41;

      

       A44: the Arity of S1 tolerates the Arity of S2 by A1;

      

       A45: ( rng the Arity of S1) c= (the carrier of S1 * );

      

       A46: (f,g) form_a_replacement_in S1 by A6, A9, Th52;

      the Arity of T(S) = (((FS * ) * the Arity of S) * gg) by A6, Th37

      .= ((((F1 * ) +* (F2 * )) * the Arity of S) * gg) by A43, A36, Th2

      .= ((((F1 * ) * the Arity of S1) +* ((F2 * ) * the Arity of S2)) * gg) by A30, A8, A45, A3, A35, A24, Th6, FUNCT_4: 69

      .= ((((F1 * ) * the Arity of S1) * g1) +* (((F2 * ) * the Arity of S2) * g2)) by A25, A14, A12, A17, A40, A44, A28, A23, Th4, FUNCT_4: 69

      .= (the Arity of T(S1) +* (((F2 * ) * the Arity of S2) * g2)) by A46, Th37

      .= (the Arity of T(S1) +* the Arity of T(S2)) by A6, A18, Th37, Th52;

      hence thesis by A22, A27, A32, A38, A16, A34, A33, A39, A26, CIRCCOMB:def 2;

    end;

    begin

    definition

      :: ALGSPEC1:def6

      mode Algebra -> object means

      : Def6: ex S be non void Signature st it is feasible MSAlgebra over S;

      existence

      proof

        set S = the non void Signature, A = the feasible MSAlgebra over S;

        take A, S;

        thus thesis;

      end;

    end

    definition

      let S be Signature;

      :: ALGSPEC1:def7

      mode Algebra of S -> Algebra means

      : Def7: ex E be non void Extension of S st it is feasible MSAlgebra over E;

      existence

      proof

        set E = the non void Extension of S;

        set A = the feasible MSAlgebra over E;

        A is Algebra by Def6;

        hence thesis;

      end;

    end

    theorem :: ALGSPEC1:55

    for S be non void Signature, A be feasible MSAlgebra over S holds A is Algebra of S

    proof

      let S be non void Signature, A be feasible MSAlgebra over S;

      

       A1: S is Extension of S by Th45;

      A is Algebra by Def6;

      hence thesis by A1, Def7;

    end;

    theorem :: ALGSPEC1:56

    for S be Signature, E be Extension of S, A be Algebra of E holds A is Algebra of S

    proof

      let S be Signature, E be Extension of S, A be Algebra of E;

      consider E9 be non void Extension of E such that

       A1: A is feasible MSAlgebra over E9 by Def7;

      E9 is Extension of S by Th46;

      hence thesis by A1, Def7;

    end;

    theorem :: ALGSPEC1:57

    

     Th57: for S be Signature, E be non empty Signature, A be MSAlgebra over E st A is Algebra of S holds the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E

    proof

      let S be Signature, E be non empty Signature, A be MSAlgebra over E;

      

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

      assume A is Algebra of S;

      then

      consider ES be non void Extension of S such that

       A2: A is feasible MSAlgebra over ES by Def7;

      reconsider B = A as MSAlgebra over ES by A2;

      

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

      

       A4: S is Subsignature of ES by Def5;

      ( dom the Sorts of B) = the carrier of ES by PARTFUN1:def 2;

      hence the carrier of S c= the carrier of E by A4, A3, INSTALG1: 10;

      ( dom the Charact of B) = the carrier' of ES by PARTFUN1:def 2;

      hence thesis by A4, A1, INSTALG1: 10;

    end;

    theorem :: ALGSPEC1:58

    

     Th58: for S be non void Signature, E be non empty Signature holds for A be MSAlgebra over E st A is Algebra of S holds for o be OperSymbol of S holds (the Charact of A . o) is Function of ((the Sorts of A # ) . ( the_arity_of o)), (the Sorts of A . ( the_result_sort_of o))

    proof

      let S be non void Signature, E be non empty Signature;

      let A be MSAlgebra over E;

      

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

      assume A is Algebra of S;

      then

      consider ES be non void Extension of S such that

       A2: A is feasible MSAlgebra over ES by Def7;

      reconsider B = A as MSAlgebra over ES by A2;

      let o be OperSymbol of S;

      

       A3: ( dom the Sorts of B) = the carrier of ES by PARTFUN1:def 2;

      

       A4: S is Subsignature of ES by Def5;

      then

       A5: the carrier' of S c= the carrier' of ES by INSTALG1: 10;

      the ResultSort of S = (the ResultSort of ES | the carrier' of S) by A4, INSTALG1: 12;

      then

       A6: ( the_result_sort_of o) = (the ResultSort of ES . o) by FUNCT_1: 49;

      the Arity of S = (the Arity of ES | the carrier' of S) by A4, INSTALG1: 12;

      then

       A7: ( the_arity_of o) = (the Arity of ES . o) by FUNCT_1: 49;

      

       A8: (the Charact of B . o) is Function of (((the Sorts of B # ) * the Arity of ES) . o), ((the Sorts of B * the ResultSort of ES) . o) by A5, PBOOLE:def 15;

      the carrier' of ES = ( dom the ResultSort of ES) by FUNCT_2:def 1;

      then

       A9: ((the Sorts of B * the ResultSort of ES) . o) = (the Sorts of A . ( the_result_sort_of o)) by A5, A6, FUNCT_1: 13;

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

      then (((the Sorts of B # ) * the Arity of ES) . o) = ((the Sorts of A # ) . ( the_arity_of o)) by A5, A3, A1, A7, FUNCT_1: 13;

      hence thesis by A9, A8;

    end;

    theorem :: ALGSPEC1:59

    for S be non empty Signature, A be Algebra of S holds for E be non empty ManySortedSign st A is MSAlgebra over E holds A is MSAlgebra over (E +* S)

    proof

      let S be non empty Signature, A be Algebra of S;

      let E be non empty ManySortedSign;

      set T = (E +* S);

      

       A1: ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

      

       A2: the ResultSort of T = (the ResultSort of E +* the ResultSort of S) by CIRCCOMB:def 2;

      assume A is MSAlgebra over E;

      then

      reconsider B = A as MSAlgebra over E;

      

       A3: the Arity of T = (the Arity of E +* the Arity of S) by CIRCCOMB:def 2;

      B is Algebra of S;

      then

       A4: the carrier of S c= the carrier of E by Th57;

      the carrier of T = (the carrier of E \/ the carrier of S) by CIRCCOMB:def 2;

      then

       A5: the carrier of T = the carrier of E by A4, XBOOLE_1: 12;

      then

      reconsider Ss = the Sorts of B as ManySortedSet of the carrier of T;

      B is Algebra of S;

      then

       A6: the carrier' of S c= the carrier' of E by Th57;

      the carrier' of T = (the carrier' of E \/ the carrier' of S) by CIRCCOMB:def 2;

      then

       A7: the carrier' of T = the carrier' of E by A6, XBOOLE_1: 12;

      

       A8: ( dom the Arity of S) = the carrier' of S by FUNCT_2:def 1;

      now

        let i be object;

        assume

         A9: i in the carrier' of T;

        then

         A10: ((Ss * the ResultSort of T) . i) = (Ss . (the ResultSort of T . i)) by FUNCT_2: 15;

         A11:

        now

          assume

           A12: i in the carrier' of S;

          then

          reconsider S9 = S as non void Signature;

          reconsider o = i as OperSymbol of S9 by A12;

          

           A13: (the Arity of T . o) = ( the_arity_of o) by A8, A3, FUNCT_4: 13;

          (the ResultSort of T . o) = ( the_result_sort_of o) by A1, A2, FUNCT_4: 13;

          hence (the Charact of B . i) is Function of ((the Sorts of B # ) . (the Arity of T . i)), (the Sorts of B . (the ResultSort of T . i)) by A13, Th58;

        end;

        

         A14: not i in the carrier' of S implies (the Arity of T . i) = (the Arity of E . i) & (the ResultSort of T . i) = (the ResultSort of E . i) by A8, A1, A3, A2, FUNCT_4: 11;

        

         A15: (((Ss # ) * the Arity of E) . i) = ((Ss # ) . (the Arity of E . i)) by A7, A9, FUNCT_2: 15;

        

         A16: (((Ss # ) * the Arity of T) . i) = ((Ss # ) . (the Arity of T . i)) by A9, FUNCT_2: 15;

        ((Ss * the ResultSort of E) . i) = (Ss . (the ResultSort of E . i)) by A7, A9, FUNCT_2: 15;

        hence (the Charact of B . i) is Function of (((Ss # ) * the Arity of T) . i), ((Ss * the ResultSort of T) . i) by A5, A7, A9, A15, A10, A16, A11, A14, PBOOLE:def 15;

      end;

      then

      reconsider C = the Charact of B as ManySortedFunction of ((Ss # ) * the Arity of T), (Ss * the ResultSort of T) by A7, PBOOLE:def 15;

      set B9 = MSAlgebra (# Ss, C #);

      the Sorts of B9 = the Sorts of B;

      then B is MSAlgebra over T;

      hence thesis;

    end;

    theorem :: ALGSPEC1:60

    

     Th60: for S1,S2 be non empty Signature holds for A be MSAlgebra over S1 st A is MSAlgebra over S2 holds the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2

    proof

      let S1,S2 be non empty Signature;

      let A be MSAlgebra over S1;

      assume A is MSAlgebra over S2;

      then

      reconsider B = A as MSAlgebra over S2;

      the Sorts of A = the Sorts of B;

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

      hence the carrier of S1 = the carrier of S2 by PARTFUN1:def 2;

      the Charact of A = the Charact of B;

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

      hence thesis by PARTFUN1:def 2;

    end;

    registration

      let S be non void Signature, A be non-empty disjoint_valued MSAlgebra over S;

      cluster the Sorts of A -> one-to-one;

      coherence

      proof

        let x,y be object;

        assume that

         A1: x in ( dom the Sorts of A) and

         A2: y in ( dom the Sorts of A);

        reconsider a = x, b = y as SortSymbol of S by A1, A2;

        assume that

         A3: (the Sorts of A . x) = (the Sorts of A . y) and

         A4: x <> y;

        the Sorts of A is disjoint_valued by MSAFREE1:def 2;

        then (the Sorts of A . a) misses (the Sorts of A . b) by A4, PROB_2:def 2;

        hence thesis by A3;

      end;

    end

    theorem :: ALGSPEC1:61

    

     Th61: for S be non void Signature holds for A be disjoint_valued MSAlgebra over S holds for C1,C2 be Component of the Sorts of A holds C1 = C2 or C1 misses C2

    proof

      let S be non void Signature;

      let A be disjoint_valued MSAlgebra over S;

      let C1,C2 be Component of the Sorts of A;

      

       A1: ex y be object st y in ( dom the Sorts of A) & C2 = (the Sorts of A . y) by FUNCT_1:def 3;

      

       A2: the Sorts of A is disjoint_valued by MSAFREE1:def 2;

      ex x be object st x in ( dom the Sorts of A) & C1 = (the Sorts of A . x) by FUNCT_1:def 3;

      hence thesis by A1, A2, PROB_2:def 2;

    end;

    theorem :: ALGSPEC1:62

    

     Th62: for S,S9 be non void Signature holds for A be non-empty disjoint_valued MSAlgebra over S st A is MSAlgebra over S9 holds the ManySortedSign of S = the ManySortedSign of S9

    proof

      let S,E be non void Signature;

      let A be non-empty disjoint_valued MSAlgebra over S;

      

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

      assume

       A2: A is MSAlgebra over E;

      then

      reconsider B = A as MSAlgebra over E;

      

       A3: the carrier of S = the carrier of E by A2, Th60;

       A4:

      now

        let x be object;

        assume x in the carrier' of S;

        then

        reconsider o = x as OperSymbol of S;

        reconsider e = o as OperSymbol of E by A2, Th60;

        set p = the Element of ( Args (o,A));

        ( Den (e,B)) = (the Charact of B . e);

        then

         A5: ( rng ( Den (o,A))) c= ( Result (e,B)) by RELAT_1:def 19;

        (( Den (o,A)) . p) in ( rng ( Den (o,A))) by FUNCT_2: 4;

        then ( Result (o,A)) meets ( Result (e,B)) by A5, XBOOLE_0: 3;

        

        then ( Result (o,A)) = ((the Sorts of B * the ResultSort of E) . x) by Th61

        .= (the Sorts of B . (the ResultSort of E . e)) by FUNCT_2: 15;

        then (the Sorts of A . (the ResultSort of E . e)) = (the Sorts of A . (the ResultSort of S . o)) by FUNCT_2: 15;

        hence (the ResultSort of S . x) = (the ResultSort of E . x) by A3, A1, FUNCT_1:def 4;

      end;

       A6:

      now

        let x be object;

        assume x in the carrier' of S;

        then

        reconsider o = x as OperSymbol of S;

        reconsider e = o as OperSymbol of E by A2, Th60;

        reconsider p = (the Arity of E . e) as Element of (the carrier of E * );

        reconsider q = (the Arity of S . o) as Element of (the carrier of S * );

        ( Den (e,B)) = (the Charact of B . e);

        then

         A7: ( dom ( Den (o,A))) = ( Args (e,B)) by FUNCT_2:def 1;

        ( dom ( Den (o,A))) = ( Args (o,A)) by FUNCT_2:def 1;

        

        then ( Args (o,A)) = ((the Sorts of B # ) . p) by A7, FUNCT_2: 15

        .= ( product (the Sorts of B * p)) by FINSEQ_2:def 5;

        

        then ( product (the Sorts of A * p)) = ((the Sorts of A # ) . q) by FUNCT_2: 15

        .= ( product (the Sorts of A * q)) by FINSEQ_2:def 5;

        then

         A8: (the Sorts of B * p) = (the Sorts of A * q) by PUA2MSS1: 2;

        

         A9: ( rng q) c= the carrier of S;

        then

         A10: ( dom (the Sorts of A * q)) = ( dom q) by A1, RELAT_1: 27;

        

         A11: ( rng p) c= the carrier of E;

        then ( dom (the Sorts of B * p)) = ( dom p) by A3, A1, RELAT_1: 27;

        hence (the Arity of S . x) = (the Arity of E . x) by A3, A1, A8, A11, A9, A10, FUNCT_1: 27;

      end;

      

       A12: ( dom the Arity of E) = the carrier' of E by FUNCT_2:def 1;

      

       A13: ( dom the Arity of S) = the carrier' of S by FUNCT_2:def 1;

      the ResultSort of S = the ResultSort of E by A2, A4, Th60;

      hence thesis by A3, A13, A12, A6, FUNCT_1: 2;

    end;

    theorem :: ALGSPEC1:63

    for S9 be non void Signature holds for A be non-empty disjoint_valued MSAlgebra over S st A is Algebra of S9 holds S is Extension of S9

    proof

      let S9 be non void Signature;

      let A be non-empty disjoint_valued MSAlgebra over S;

      assume A is Algebra of S9;

      then

      consider E be non void Extension of S9 such that

       A1: A is feasible MSAlgebra over E by Def7;

      

       A2: S9 is Subsignature of E by Def5;

      

       A3: the ManySortedSign of S = the ManySortedSign of E by A1, Th62;

      then

       A4: the ResultSort of S9 c= the ResultSort of S by A2, INSTALG1: 11;

      the Arity of S9 c= the Arity of S by A2, A3, INSTALG1: 11;

      hence S9 is Subsignature of S by A2, A3, A4, INSTALG1: 10, INSTALG1: 13;

    end;