pralg_2.miz



    begin

    reserve I,J for set,

i,j,x for object,

S for non empty ManySortedSign;

    registration

      let X be with_common_domain functional non empty set;

      cluster -> ( DOM X) -defined for Element of X;

      coherence

      proof

        let x be Element of X;

        ( DOM X) = ( dom x) by CARD_3: 108;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let X be with_common_domain functional non empty set;

      cluster -> total for Element of X;

      coherence

      proof

        let x be Element of X;

        ( DOM X) = ( dom x) by CARD_3: 108;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    begin

    definition

      let F be Function;

      :: PRALG_2:def1

      func Commute F -> Function means

      : Def1: (for x holds x in ( dom it ) iff ex f be Function st f in ( dom F) & x = ( commute f)) & for f be Function st f in ( dom it ) holds (it . f) = (F . ( commute f));

      existence

      proof

        defpred P[ object, object] means ex f be Function st $1 = f & $2 = ( commute f);

        

         A1: for x,y1,y2 be object st P[x, y1] & P[x, y2] holds y1 = y2;

        consider X be set such that

         A2: for x be object holds x in X iff ex y be object st y in ( dom F) & P[y, x] from TARSKI:sch 1( A1);

        defpred P[ object, object] means for f be Function st $1 = f holds $2 = (F . ( commute f));

         A3:

        now

          let x be object;

          assume x in X;

          then ex y be object st y in ( dom F) & ex f be Function st y = f & x = ( commute f) by A2;

          then

          reconsider f = x as Function;

          reconsider y = (F . ( commute f)) as object;

          take y;

          thus P[x, y];

        end;

        consider G be Function such that

         A4: ( dom G) = X and

         A5: for x be object st x in X holds P[x, (G . x)] from CLASSES1:sch 1( A3);

        take G;

        hereby

          let x;

          hereby

            assume x in ( dom G);

            then

            consider y be object such that

             A6: y in ( dom F) and

             A7: ex f be Function st y = f & x = ( commute f) by A2, A4;

            reconsider f = y as Function by A7;

            take f;

            thus f in ( dom F) & x = ( commute f) by A6, A7;

          end;

          thus (ex f be Function st f in ( dom F) & x = ( commute f)) implies x in ( dom G) by A2, A4;

        end;

        thus thesis by A4, A5;

      end;

      uniqueness

      proof

        let m,n be Function such that

         A8: for x holds x in ( dom m) iff ex f be Function st f in ( dom F) & x = ( commute f) and

         A9: for f be Function st f in ( dom m) holds (m . f) = (F . ( commute f)) and

         A10: for x holds x in ( dom n) iff ex f be Function st f in ( dom F) & x = ( commute f) and

         A11: for f be Function st f in ( dom n) holds (n . f) = (F . ( commute f));

        now

          let x be object;

          x in ( dom m) iff ex f be Function st f in ( dom F) & x = ( commute f) by A8;

          hence x in ( dom m) iff x in ( dom n) by A10;

        end;

        then

         A12: ( dom m) = ( dom n) by TARSKI: 2;

        now

          let x be object;

          assume

           A13: x in ( dom m);

          then

          consider g be Function such that g in ( dom F) and

           A14: x = ( commute g) by A10, A12;

          

          thus (m . x) = (F . ( commute ( commute g))) by A9, A13, A14

          .= (n . x) by A11, A12, A13, A14;

        end;

        hence thesis by A12, FUNCT_1: 2;

      end;

    end

    theorem :: PRALG_2:1

    for F be Function st ( dom F) = { {} } holds ( Commute F) = F

    proof

      let F be Function;

      assume

       A1: ( dom F) = { {} };

      

       A2: ( dom ( Commute F)) = { {} }

      proof

        thus ( dom ( Commute F)) c= { {} }

        proof

          let x be object;

          assume x in ( dom ( Commute F));

          then ex f be Function st f in ( dom F) & x = ( commute f) by Def1;

          then x = {} by A1, FUNCT_6: 58, TARSKI:def 1;

          hence thesis by TARSKI:def 1;

        end;

        let x be object;

        assume x in { {} };

        then

         A3: x = {} by TARSKI:def 1;

         {} in ( dom F) by A1, TARSKI:def 1;

        hence thesis by A3, Def1, FUNCT_6: 58;

      end;

      for x be object st x in { {} } holds (( Commute F) . x) = (F . x)

      proof

        let x be object;

        assume

         A4: x in { {} };

        then x = {} by TARSKI:def 1;

        hence thesis by A2, A4, Def1, FUNCT_6: 58;

      end;

      hence thesis by A1, A2, FUNCT_1: 2;

    end;

    definition

      let f be Function-yielding Function;

      :: original: Frege

      redefine

      :: PRALG_2:def2

      func Frege f -> ManySortedFunction of ( product ( doms f)) means

      : Def2: for g be Function st g in ( product ( doms f)) holds (it . g) = (f .. g);

      coherence

      proof

        

         A1: ( dom ( Frege f)) = ( product ( doms f)) by FUNCT_6:def 7;

        ( Frege f) is Function-yielding

        proof

          let x be object;

          assume

           A2: x in ( dom ( Frege f));

          then

          reconsider g = x as Function by A1;

          ex h be Function st (( Frege f) . g) = h & ( dom h) = ( dom f) & for x st x in ( dom h) holds (h . x) = (( uncurry f) . (x,(g . x))) by A1, A2, FUNCT_6:def 7;

          hence thesis;

        end;

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

      end;

      compatibility

      proof

        let F be ManySortedFunction of ( product ( doms f));

        thus F = ( Frege f) implies for g be Function st g in ( product ( doms f)) holds (F . g) = (f .. g)

        proof

          assume

           A3: F = ( Frege f);

          let g be Function;

          assume

           A4: g in ( product ( doms f));

          then

          consider h be Function such that

           A5: (F . g) = h and

           A6: ( dom h) = ( dom f) and

           A7: for x st x in ( dom h) holds (h . x) = (( uncurry f) . (x,(g . x))) by A3, FUNCT_6:def 7;

          consider gg be Function such that

           a13: g = gg & ( dom gg) = ( dom ( doms f)) & for y be object st y in ( dom ( doms f)) holds (gg . y) in (( doms f) . y) by CARD_3:def 5, A4;

          ( dom g) = ( dom f) by a13, FUNCT_6:def 2;

          then

           A8: ( dom h) = (( dom f) /\ ( dom g)) by A6;

          for x be set st x in ( dom h) holds (h . x) = ((f . x) . (g . x))

          proof

            let x be set;

            assume

             A9: x in ( dom h);

            then x in ( dom ( doms f)) by A6, FUNCT_6:def 2;

            then (g . x) in (( doms f) . x) by A4, CARD_3: 9;

            then

             A10: (g . x) in ( dom (f . x)) by A9, A6, FUNCT_6: 22;

            

            thus (h . x) = (f .. (x,(g . x))) by A7, A9

            .= ((f . x) . (g . x)) by A9, A6, A10, FUNCT_5: 38;

          end;

          hence thesis by A5, A8, PRALG_1:def 19;

        end;

        assume

         A11: for g be Function st g in ( product ( doms f)) holds (F . g) = (f .. g);

        

         A12: for g be Function st g in ( product ( doms f)) holds ex h be Function st (F . g) = h & ( dom h) = ( dom f) & for x be object st x in ( dom h) holds (h . x) = (( uncurry f) . (x,(g . x)))

        proof

          let g be Function such that

           A13: g in ( product ( doms f));

          consider gg be Function such that

           a13: g = gg & ( dom gg) = ( dom ( doms f)) & for y be object st y in ( dom ( doms f)) holds (gg . y) in (( doms f) . y) by CARD_3:def 5, A13;

          

           a14: (F . g) = (f .. g) by A11, A13;

          then

           A14: ( dom (F . g)) = (( dom f) /\ ( dom g)) by PRALG_1:def 19;

          take (F . g);

          thus (F . g) = (F . g);

          

           WW: ( dom g) = ( dom f) by a13, FUNCT_6:def 2;

          hence ( dom (F . g)) = ( dom f) by A14;

          let x be object;

          assume

           A15: x in ( dom (F . g));

          then x in ( dom ( doms f)) by WW, A14, FUNCT_6:def 2;

          then (g . x) in (( doms f) . x) by A13, CARD_3: 9;

          then

           A16: (g . x) in ( dom (f . x)) by A14, A15, FUNCT_6: 22, WW;

          

          thus ((F . g) . x) = ((f .. g) . x) by A11, A13

          .= ((f . x) . (g . x)) by A15, PRALG_1:def 19, a14

          .= (( uncurry f) . (x,(g . x))) by A14, A15, A16, FUNCT_5: 38, WW;

        end;

        ( dom F) = ( product ( doms f)) by PARTFUN1:def 2;

        hence thesis by A12, FUNCT_6:def 7;

      end;

    end

    registration

      let I;

      let A,B be non-empty ManySortedSet of I;

      cluster [|A, B|] -> non-empty;

      coherence

      proof

        now

          let i be object;

          assume

           A1: i in I;

          then ( [|A, B|] . i) = [:(A . i), (B . i):] by PBOOLE:def 16;

          hence ( [|A, B|] . i) is non empty by A1, ZFMISC_1: 90;

        end;

        hence thesis;

      end;

    end

    theorem :: PRALG_2:2

    for I be non empty set, J be set, A,B be ManySortedSet of I, f be Function of J, I holds ( [|A, B|] * f) = [|(A * f), (B * f)|]

    proof

      let I be non empty set, J be set, A,B be ManySortedSet of I, f be Function of J, I;

      for i be object st i in J holds (( [|A, B|] * f) . i) = ( [|(A * f), (B * f)|] . i)

      proof

        

         A1: ( dom (B * f)) = J by PARTFUN1:def 2;

        let i be object;

        

         A2: ( dom (A * f)) = J by PARTFUN1:def 2;

        assume

         A3: i in J;

        then

         A4: (f . i) in I by FUNCT_2: 5;

        ( dom ( [|A, B|] * f)) = J by PARTFUN1:def 2;

        

        hence (( [|A, B|] * f) . i) = ( [|A, B|] . (f . i)) by A3, FUNCT_1: 12

        .= [:(A . (f . i)), (B . (f . i)):] by A4, PBOOLE:def 16

        .= [:((A * f) . i), (B . (f . i)):] by A3, A2, FUNCT_1: 12

        .= [:((A * f) . i), ((B * f) . i):] by A3, A1, FUNCT_1: 12

        .= ( [|(A * f), (B * f)|] . i) by A3, PBOOLE:def 16;

      end;

      hence thesis;

    end;

    definition

      let I be non empty set;

      let A,B be non-empty ManySortedSet of I, pj be Element of (I * ), rj be Element of I, f be Function of ((A # ) . pj), (A . rj), g be Function of ((B # ) . pj), (B . rj);

      :: PRALG_2:def3

      func [[:f,g:]] -> Function of (( [|A, B|] # ) . pj), ( [|A, B|] . rj) means for h be Function st h in (( [|A, B|] # ) . pj) holds (it . h) = [(f . ( pr1 h)), (g . ( pr2 h))];

      existence

      proof

        defpred P[ object, object] means for h be Function st h = $1 holds $2 = [(f . ( pr1 h)), (g . ( pr2 h))];

        set Y = ( [|A, B|] . rj), X = (( [|A, B|] # ) . pj);

        

         A1: X = ( product ( [|A, B|] * pj)) by FINSEQ_2:def 5;

        

         A2: for x be object st x in X holds ex y be object st y in Y & P[x, y]

        proof

          let x be object;

          

           A3: ( rng pj) c= I by FINSEQ_1:def 4;

          assume x in X;

          then

          consider h1 be Function such that

           A4: h1 = x and

           A5: ( dom h1) = ( dom ( [|A, B|] * pj)) and

           A6: for z be object st z in ( dom ( [|A, B|] * pj)) holds (h1 . z) in (( [|A, B|] * pj) . z) by A1, CARD_3:def 5;

          

           A7: ( dom [|A, B|]) = I by PARTFUN1:def 2;

          then

           A8: ( dom h1) = ( dom pj) by A5, A3, RELAT_1: 27;

          then

           A9: ( dom ( pr1 h1)) = ( dom pj) by MCART_1:def 12;

          ( dom A) = I by PARTFUN1:def 2;

          then

           A10: ( dom ( pr1 h1)) = ( dom (A * pj)) by A3, A9, RELAT_1: 27;

          for z be object st z in ( dom (A * pj)) holds (( pr1 h1) . z) in ((A * pj) . z)

          proof

            let z be object;

            assume

             A11: z in ( dom (A * pj));

            ( dom ( [|A, B|] * pj)) = ( dom pj) by A7, A3, RELAT_1: 27;

            then

             A12: (( [|A, B|] * pj) . z) = ( [|A, B|] . (pj . z)) by A9, A10, A11, FUNCT_1: 12;

            (h1 . z) in (( [|A, B|] * pj) . z) & (pj . z) in ( rng pj) by A5, A6, A8, A9, A10, A11, FUNCT_1:def 3;

            then (h1 . z) in [:(A . (pj . z)), (B . (pj . z)):] by A3, A12, PBOOLE:def 16;

            then

            consider a,b be object such that

             A13: a in (A . (pj . z)) and b in (B . (pj . z)) and

             A14: (h1 . z) = [a, b] by ZFMISC_1:def 2;

            (( pr1 h1) . z) = ((h1 . z) `1 ) by A8, A9, A10, A11, MCART_1:def 12

            .= a by A14;

            hence thesis by A11, A13, FUNCT_1: 12;

          end;

          then ( pr1 h1) in ( product (A * pj)) by A10, CARD_3: 9;

          then ( pr1 h1) in ((A # ) . pj) by FINSEQ_2:def 5;

          then ( pr1 h1) in ( dom f) by FUNCT_2:def 1;

          then

           A15: (f . ( pr1 h1)) in ( rng f) by FUNCT_1: 3;

          take y = [(f . ( pr1 h1)), (g . ( pr2 h1))];

          ( rng f) c= (A . rj) & ( rng g) c= (B . rj) by RELAT_1:def 19;

          then

           A16: [:( rng f), ( rng g):] c= [:(A . rj), (B . rj):] by ZFMISC_1: 96;

          

           A17: ( dom ( pr2 h1)) = ( dom pj) by A8, MCART_1:def 13;

          

           A18: ( dom B) = I by PARTFUN1:def 2;

          then

           A19: ( dom ( pr2 h1)) = ( dom (B * pj)) by A3, A17, RELAT_1: 27;

          

           A20: for z be object st z in ( dom (B * pj)) holds (( pr2 h1) . z) in ((B * pj) . z)

          proof

            let z be object;

            assume

             A21: z in ( dom (B * pj));

            ( dom ( [|A, B|] * pj)) = ( dom pj) by A7, A3, RELAT_1: 27;

            then

             A22: (( [|A, B|] * pj) . z) = ( [|A, B|] . (pj . z)) by A17, A19, A21, FUNCT_1: 12;

            (h1 . z) in (( [|A, B|] * pj) . z) & (pj . z) in ( rng pj) by A5, A6, A8, A17, A19, A21, FUNCT_1:def 3;

            then (h1 . z) in [:(A . (pj . z)), (B . (pj . z)):] by A3, A22, PBOOLE:def 16;

            then

            consider a,b be object such that a in (A . (pj . z)) and

             A23: b in (B . (pj . z)) and

             A24: (h1 . z) = [a, b] by ZFMISC_1:def 2;

            (( pr2 h1) . z) = ((h1 . z) `2 ) by A8, A17, A19, A21, MCART_1:def 13

            .= b by A24;

            hence thesis by A21, A23, FUNCT_1: 12;

          end;

          ( dom ( pr2 h1)) = ( dom pj) by A8, MCART_1:def 13;

          then ( dom ( pr2 h1)) = ( dom (B * pj)) by A18, A3, RELAT_1: 27;

          then ( pr2 h1) in ( product (B * pj)) by A20, CARD_3: 9;

          then ( pr2 h1) in ((B # ) . pj) by FINSEQ_2:def 5;

          then ( pr2 h1) in ( dom g) by FUNCT_2:def 1;

          then (g . ( pr2 h1)) in ( rng g) by FUNCT_1: 3;

          then [(f . ( pr1 h1)), (g . ( pr2 h1))] in [:( rng f), ( rng g):] by A15, ZFMISC_1: 87;

          then [(f . ( pr1 h1)), (g . ( pr2 h1))] in [:(A . rj), (B . rj):] by A16;

          hence y in Y by PBOOLE:def 16;

          let h be Function;

          assume x = h;

          hence thesis by A4;

        end;

        consider F be Function of X, Y such that

         A25: for x be object st x in X holds P[x, (F . x)] from FUNCT_2:sch 1( A2);

        take F;

        thus thesis by A25;

      end;

      uniqueness

      proof

        let x,y be Function of (( [|A, B|] # ) . pj), ( [|A, B|] . rj) such that

         A26: for h be Function st h in (( [|A, B|] # ) . pj) holds (x . h) = [(f . ( pr1 h)), (g . ( pr2 h))] and

         A27: for h be Function st h in (( [|A, B|] # ) . pj) holds (y . h) = [(f . ( pr1 h)), (g . ( pr2 h))];

        let h be Element of (( [|A, B|] # ) . pj);

        h in (( [|A, B|] # ) . pj);

        then h in ( product ( [|A, B|] * pj)) by FINSEQ_2:def 5;

        then

        consider h1 be Function such that

         A28: h1 = h and ( dom h1) = ( dom ( [|A, B|] * pj)) and for z be object st z in ( dom ( [|A, B|] * pj)) holds (h1 . z) in (( [|A, B|] * pj) . z) by CARD_3:def 5;

        (x . h1) = [(f . ( pr1 h1)), (g . ( pr2 h1))] by A26, A28;

        hence (x . h) = (y . h) by A27, A28;

      end;

    end

    definition

      let I be non empty set, J;

      let A,B be non-empty ManySortedSet of I, p be Function of J, (I * ), r be Function of J, I, F be ManySortedFunction of ((A # ) * p), (A * r), G be ManySortedFunction of ((B # ) * p), (B * r);

      :: PRALG_2:def4

      func [[:F,G:]] -> ManySortedFunction of (( [|A, B|] # ) * p), ( [|A, B|] * r) means for j st j in J holds for pj be Element of (I * ), rj be Element of I st pj = (p . j) & rj = (r . j) holds for f be Function of ((A # ) . pj), (A . rj), g be Function of ((B # ) . pj), (B . rj) st f = (F . j) & g = (G . j) holds (it . j) = [[:f, g:]];

      existence

      proof

        defpred P[ object, object] means for pj be Element of (I * ), rj be Element of I st pj = (p . $1) & rj = (r . $1) holds for f be Function of ((A # ) . pj), (A . rj), g be Function of ((B # ) . pj), (B . rj) st f = (F . $1) & g = (G . $1) holds $2 = [[:f, g:]];

        

         A1: for j be object st j in J holds ex i be object st P[j, i]

        proof

          let j be object;

          assume

           A2: j in J;

          then

          reconsider pj = (p . j) as Element of (I * ) by FUNCT_2: 5;

          reconsider rj = (r . j) as Element of I by A2, FUNCT_2: 5;

          

           A3: j in ( dom r) by A2, FUNCT_2:def 1;

          then

           A4: (A . (r . j)) = ((A * r) . j) by FUNCT_1: 13;

          

           A5: (B . (r . j)) = ((B * r) . j) by A3, FUNCT_1: 13;

          

           A6: j in ( dom p) by A2, FUNCT_2:def 1;

          then ((A # ) . (p . j)) = (((A # ) * p) . j) by FUNCT_1: 13;

          then

          reconsider f = (F . j) as Function of ((A # ) . pj), (A . rj) by A2, A4, PBOOLE:def 15;

          ((B # ) . (p . j)) = (((B # ) * p) . j) by A6, FUNCT_1: 13;

          then

          reconsider g = (G . j) as Function of ((B # ) . pj), (B . rj) by A2, A5, PBOOLE:def 15;

          take [[:f, g:]];

          thus thesis;

        end;

        consider h be Function such that

         A7: ( dom h) = J & for j be object st j in J holds P[j, (h . j)] from CLASSES1:sch 1( A1);

        reconsider h as ManySortedSet of J by A7, PARTFUN1:def 2, RELAT_1:def 18;

        for j be object st j in ( dom h) holds (h . j) is Function

        proof

          let j be object;

          assume

           A8: j in ( dom h);

          then

          reconsider pj = (p . j) as Element of (I * ) by A7, FUNCT_2: 5;

          reconsider rj = (r . j) as Element of I by A7, A8, FUNCT_2: 5;

          

           A9: j in ( dom r) by A7, A8, FUNCT_2:def 1;

          then

           A10: (A . (r . j)) = ((A * r) . j) by FUNCT_1: 13;

          

           A11: (B . (r . j)) = ((B * r) . j) by A9, FUNCT_1: 13;

          

           A12: j in ( dom p) by A7, A8, FUNCT_2:def 1;

          then ((A # ) . (p . j)) = (((A # ) * p) . j) by FUNCT_1: 13;

          then

          reconsider f = (F . j) as Function of ((A # ) . pj), (A . rj) by A7, A8, A10, PBOOLE:def 15;

          ((B # ) . (p . j)) = (((B # ) * p) . j) by A12, FUNCT_1: 13;

          then

          reconsider g = (G . j) as Function of ((B # ) . pj), (B . rj) by A7, A8, A11, PBOOLE:def 15;

          (h . j) = [[:f, g:]] by A7, A8;

          hence thesis;

        end;

        then

        reconsider h as ManySortedFunction of J by FUNCOP_1:def 6;

        for j st j in J holds (h . j) is Function of ((( [|A, B|] # ) * p) . j), (( [|A, B|] * r) . j)

        proof

          let j;

          assume

           A13: j in J;

          then

          reconsider pj = (p . j) as Element of (I * ) by FUNCT_2: 5;

          reconsider rj = (r . j) as Element of I by A13, FUNCT_2: 5;

          

           A14: j in ( dom p) by A13, FUNCT_2:def 1;

          then

           A15: ((( [|A, B|] # ) * p) . j) = (( [|A, B|] # ) . (p . j)) by FUNCT_1: 13;

          

           A16: j in ( dom r) by A13, FUNCT_2:def 1;

          then

           A17: (A . (r . j)) = ((A * r) . j) by FUNCT_1: 13;

          

           A18: (( [|A, B|] * r) . j) = ( [|A, B|] . (r . j)) by A16, FUNCT_1: 13;

          

           A19: (B . (r . j)) = ((B * r) . j) by A16, FUNCT_1: 13;

          ((B # ) . (p . j)) = (((B # ) * p) . j) by A14, FUNCT_1: 13;

          then

          reconsider g = (G . j) as Function of ((B # ) . pj), (B . rj) by A13, A19, PBOOLE:def 15;

          ((A # ) . (p . j)) = (((A # ) * p) . j) by A14, FUNCT_1: 13;

          then

          reconsider f = (F . j) as Function of ((A # ) . pj), (A . rj) by A13, A17, PBOOLE:def 15;

          (h . j) = [[:f, g:]] by A7, A13;

          hence thesis by A15, A18;

        end;

        then

        reconsider h as ManySortedFunction of (( [|A, B|] # ) * p), ( [|A, B|] * r) by PBOOLE:def 15;

        take h;

        thus thesis by A7;

      end;

      uniqueness

      proof

        let x,y be ManySortedFunction of (( [|A, B|] # ) * p), ( [|A, B|] * r);

        assume that

         A20: for j st j in J holds for pj be Element of (I * ), rj be Element of I st pj = (p . j) & rj = (r . j) holds for f be Function of ((A # ) . pj), (A . rj), g be Function of ((B # ) . pj), (B . rj) st f = (F . j) & g = (G . j) holds (x . j) = [[:f, g:]] and

         A21: for j st j in J holds for pj be Element of (I * ), rj be Element of I st pj = (p . j) & rj = (r . j) holds for f be Function of ((A # ) . pj), (A . rj), g be Function of ((B # ) . pj), (B . rj) st f = (F . j) & g = (G . j) holds (y . j) = [[:f, g:]];

        for j be object st j in J holds (x . j) = (y . j)

        proof

          let j be object;

          assume

           A22: j in J;

          then

          reconsider pj = (p . j) as Element of (I * ) by FUNCT_2: 5;

          reconsider rj = (r . j) as Element of I by A22, FUNCT_2: 5;

          

           A23: j in ( dom r) by A22, FUNCT_2:def 1;

          then

           A24: (A . (r . j)) = ((A * r) . j) by FUNCT_1: 13;

          

           A25: (B . (r . j)) = ((B * r) . j) by A23, FUNCT_1: 13;

          

           A26: j in ( dom p) by A22, FUNCT_2:def 1;

          then ((A # ) . (p . j)) = (((A # ) * p) . j) by FUNCT_1: 13;

          then

          reconsider f = (F . j) as Function of ((A # ) . pj), (A . rj) by A22, A24, PBOOLE:def 15;

          ((B # ) . (p . j)) = (((B # ) * p) . j) by A26, FUNCT_1: 13;

          then

          reconsider g = (G . j) as Function of ((B # ) . pj), (B . rj) by A22, A25, PBOOLE:def 15;

          (x . j) = [[:f, g:]] by A20, A22;

          hence thesis by A21, A22;

        end;

        hence thesis;

      end;

    end

    begin

    definition

      let I, S;

      :: PRALG_2:def5

      mode MSAlgebra-Family of I,S -> ManySortedSet of I means

      : Def5: for i st i in I holds (it . i) is non-empty MSAlgebra over S;

      existence

      proof

        set A = the non-empty MSAlgebra over S;

        set f = (I --> A);

        reconsider f as ManySortedSet of I;

        take f;

        let i;

        assume i in I;

        hence thesis by FUNCOP_1: 7;

      end;

    end

    definition

      let I be non empty set, S;

      let A be MSAlgebra-Family of I, S, i be Element of I;

      :: original: .

      redefine

      func A . i -> non-empty MSAlgebra over S ;

      coherence by Def5;

    end

    definition

      let S be non empty ManySortedSign, U1 be MSAlgebra over S;

      :: PRALG_2:def6

      func |.U1.| -> set equals ( union ( rng the Sorts of U1));

      coherence ;

    end

    registration

      let S be non empty ManySortedSign, U1 be non-empty MSAlgebra over S;

      cluster |.U1.| -> non empty;

      coherence

      proof

        reconsider St = the Sorts of U1 as non-empty ManySortedSet of the carrier of S;

        set s = the SortSymbol of S;

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

        then

         A1: (the Sorts of U1 . s) in ( rng the Sorts of U1) by FUNCT_1:def 3;

        ex x be object st x in (St . s) by XBOOLE_0:def 1;

        hence thesis by A1, TARSKI:def 4;

      end;

    end

    definition

      let I be non empty set, S be non empty ManySortedSign, A be MSAlgebra-Family of I, S;

      :: PRALG_2:def7

      func |.A.| -> set equals ( union the set of all |.(A . i).| where i be Element of I);

      coherence ;

    end

    registration

      let I be non empty set, S be non empty ManySortedSign, A be MSAlgebra-Family of I, S;

      cluster |.A.| -> non empty;

      coherence

      proof

        set a = the Element of I;

        set X = the set of all |.(A . i).| where i be Element of I;

         |.(A . a).| in X & ex x be object st x in |.(A . a).| by XBOOLE_0:def 1;

        hence thesis by TARSKI:def 4;

      end;

    end

    begin

    theorem :: PRALG_2:3

    

     Th3: for S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be OperSymbol of S holds ( Args (o,U0)) = ( product (the Sorts of U0 * ( the_arity_of o))) & ( dom (the Sorts of U0 * ( the_arity_of o))) = ( dom ( the_arity_of o)) & ( Result (o,U0)) = (the Sorts of U0 . ( the_result_sort_of o))

    proof

      let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be OperSymbol of S;

      set So = the Sorts of U0, Ar = the Arity of S, Rs = the ResultSort of S, ar = ( the_arity_of o), AS = ((So # ) * Ar), RS = (So * Rs), X = the carrier' of S, Cr = the carrier of S;

      

       A1: ( dom Ar) = X by FUNCT_2:def 1;

      then

       A2: ( dom AS) = ( dom Ar) by PARTFUN1:def 2;

      

      thus ( Args (o,U0)) = (AS . o) by MSUALG_1:def 4

      .= ((So # ) qua ManySortedSet of (Cr * ) . (Ar . o)) by A1, A2, FUNCT_1: 12

      .= ((So # ) qua ManySortedSet of (Cr * ) . ( the_arity_of o)) by MSUALG_1:def 1

      .= ( product (So * ( the_arity_of o))) by FINSEQ_2:def 5;

      ( rng ar) c= Cr & ( dom So) = Cr by FINSEQ_1:def 4, PARTFUN1:def 2;

      hence ( dom (So * ar)) = ( dom ar) by RELAT_1: 27;

      

       A3: ( dom Rs) = X by FUNCT_2:def 1;

      then

       A4: ( dom RS) = ( dom Rs) by PARTFUN1:def 2;

      

      thus ( Result (o,U0)) = (RS . o) by MSUALG_1:def 5

      .= (So . (Rs . o)) by A3, A4, FUNCT_1: 12

      .= (So . ( the_result_sort_of o)) by MSUALG_1:def 2;

    end;

    theorem :: PRALG_2:4

    

     Th4: for S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be OperSymbol of S st ( the_arity_of o) = {} holds ( Args (o,U0)) = { {} }

    proof

      let S be non void non empty ManySortedSign, U0 be MSAlgebra over S, o be OperSymbol of S;

      assume

       A1: ( the_arity_of o) = {} ;

      

      thus ( Args (o,U0)) = ( product (the Sorts of U0 * ( the_arity_of o))) by Th3

      .= { {} } by A1, CARD_3: 10;

    end;

    definition

      let S;

      let U1,U2 be non-empty MSAlgebra over S;

      :: PRALG_2:def8

      func [:U1,U2:] -> MSAlgebra over S equals MSAlgebra (# [|the Sorts of U1, the Sorts of U2|], [[:the Charact of U1, the Charact of U2:]] #);

      coherence ;

    end

    registration

      let S;

      let U1,U2 be non-empty MSAlgebra over S;

      cluster [:U1, U2:] -> strict;

      coherence ;

    end

    definition

      let I, S;

      let s be SortSymbol of S, A be MSAlgebra-Family of I, S;

      :: PRALG_2:def9

      func Carrier (A,s) -> ManySortedSet of I means

      : Def9: for i be set st i in I holds ex U0 be MSAlgebra over S st U0 = (A . i) & (it . i) = (the Sorts of U0 . s) if I <> {}

      otherwise it = {} ;

      existence

      proof

        hereby

          assume I <> {} ;

          then

          reconsider I9 = I as non empty set;

          reconsider A9 = A as MSAlgebra-Family of I9, S;

          deffunc F( Element of I9) = (the Sorts of (A9 . $1) . s);

          consider f be Function such that

           A1: ( dom f) = I9 & for i be Element of I9 holds (f . i) = F(i) from FUNCT_1:sch 4;

          reconsider f as ManySortedSet of I by A1, PARTFUN1:def 2, RELAT_1:def 18;

          take f;

          let i be set;

          assume i in I;

          then

          reconsider i9 = i as Element of I9;

          reconsider U0 = (A9 . i9) as MSAlgebra over S;

          take U0;

          thus U0 = (A . i) & (f . i) = (the Sorts of U0 . s) by A1;

        end;

        assume

         A2: I = {} ;

        take ( EmptyMS I);

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be ManySortedSet of I;

        hereby

          assume I <> {} ;

          assume

           A3: (for i be set st i in I holds ex U0 be MSAlgebra over S st U0 = (A . i) & (f . i) = (the Sorts of U0 . s)) & for i be set st i in I holds ex U0 be MSAlgebra over S st U0 = (A . i) & (g . i) = (the Sorts of U0 . s);

          for x be object st x in I holds (f . x) = (g . x)

          proof

            let x be object;

            assume

             A4: x in I;

            then

            reconsider i = x as Element of I;

            (ex U0 be MSAlgebra over S st U0 = (A . i) & (f . i) = (the Sorts of U0 . s)) & ex U0 be MSAlgebra over S st U0 = (A . i) & (g . i) = (the Sorts of U0 . s) by A3, A4;

            hence thesis;

          end;

          hence f = g;

        end;

        thus thesis;

      end;

      correctness ;

    end

    registration

      let I, S;

      let s be SortSymbol of S, A be MSAlgebra-Family of I, S;

      cluster ( Carrier (A,s)) -> non-empty;

      coherence

      proof

        let x be object;

        assume

         A1: x in I;

        then

        consider U0 be MSAlgebra over S such that

         A2: U0 = (A . x) and

         A3: (( Carrier (A,s)) . x) = (the Sorts of U0 . s) by Def9;

        U0 is non-empty MSAlgebra over S by A1, A2, Def5;

        hence thesis by A3;

      end;

    end

    definition

      let I, S;

      let A be MSAlgebra-Family of I, S;

      :: PRALG_2:def10

      func SORTS (A) -> ManySortedSet of the carrier of S means

      : Def10: for s be SortSymbol of S holds (it . s) = ( product ( Carrier (A,s)));

      existence

      proof

        deffunc F( SortSymbol of S) = ( product ( Carrier (A,$1)));

        consider f be Function such that

         A1: ( dom f) = the carrier of S & for s be SortSymbol of S holds (f . s) = F(s) from FUNCT_1:sch 4;

        reconsider f as ManySortedSet of the carrier of S by A1, PARTFUN1:def 2, RELAT_1:def 18;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,g be ManySortedSet of the carrier of S;

        assume that

         A2: for s be SortSymbol of S holds (f . s) = ( product ( Carrier (A,s))) and

         A3: for s be SortSymbol of S holds (g . s) = ( product ( Carrier (A,s)));

        for x be object st x in the carrier of S holds (f . x) = (g . x)

        proof

          let x be object;

          assume x in the carrier of S;

          then

          reconsider x1 = x as SortSymbol of S;

          (f . x1) = ( product ( Carrier (A,x1))) by A2;

          hence thesis by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let I, S;

      let A be MSAlgebra-Family of I, S;

      cluster ( SORTS A) -> non-empty;

      coherence

      proof

        let x be object;

        assume x in the carrier of S;

        then

        reconsider s = x as SortSymbol of S;

        (( SORTS A) . s) = ( product ( Carrier (A,s))) by Def10;

        hence thesis;

      end;

    end

    definition

      let I;

      let S be non empty ManySortedSign, A be MSAlgebra-Family of I, S;

      :: PRALG_2:def11

      func OPER (A) -> ManySortedFunction of I means

      : Def11: for i be set st i in I holds ex U0 be MSAlgebra over S st U0 = (A . i) & (it . i) = the Charact of U0 if I <> {}

      otherwise it = {} ;

      existence

      proof

        reconsider f = ( EmptyMS I) as ManySortedFunction of I;

        hereby

          assume I <> {} ;

          then

          reconsider I9 = I as non empty set;

          reconsider A9 = A as MSAlgebra-Family of I9, S;

          deffunc F( Element of I9) = the Charact of (A9 . $1);

          consider X be ManySortedSet of I9 such that

           A1: for i be Element of I9 holds (X . i) = F(i) from PBOOLE:sch 5;

          for x be object st x in ( dom X) holds (X . x) is Function

          proof

            let x be object;

            assume x in ( dom X);

            then

            reconsider i = x as Element of I9 by PARTFUN1:def 2;

            (X . i) = the Charact of (A9 . i) by A1;

            hence thesis;

          end;

          then

          reconsider X as ManySortedFunction of I by FUNCOP_1:def 6;

          take X;

          let i be set;

          assume i in I;

          then

          reconsider i9 = i as Element of I9;

          reconsider U0 = (A9 . i9) as MSAlgebra over S;

          take U0;

          thus U0 = (A . i) & (X . i) = the Charact of U0 by A1;

        end;

        assume

         A2: I = {} ;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be ManySortedFunction of I;

        hereby

          assume I <> {} ;

          assume

           A3: (for i be set st i in I holds ex U0 be MSAlgebra over S st U0 = (A . i) & (f . i) = the Charact of U0) & for i be set st i in I holds ex U0 be MSAlgebra over S st U0 = (A . i) & (g . i) = the Charact of U0;

          for x be object st x in I holds (f . x) = (g . x)

          proof

            let x be object;

            assume

             A4: x in I;

            then

            reconsider i = x as Element of I;

            (ex U0 be MSAlgebra over S st U0 = (A . i) & (f . i) = the Charact of U0) & ex U0 be MSAlgebra over S st U0 = (A . i) & (g . i) = the Charact of U0 by A3, A4;

            hence thesis;

          end;

          hence f = g;

        end;

        thus thesis;

      end;

      correctness ;

    end

    theorem :: PRALG_2:5

    

     Th5: for S be non empty ManySortedSign, A be MSAlgebra-Family of I, S holds ( dom ( uncurry ( OPER A))) = [:I, the carrier' of S:]

    proof

      let S be non empty ManySortedSign, A be MSAlgebra-Family of I, S;

      per cases ;

        suppose

         A1: I <> {} ;

        thus ( dom ( uncurry ( OPER A))) c= [:I, the carrier' of S:]

        proof

          let t be object;

          assume t in ( dom ( uncurry ( OPER A)));

          then

          consider x be object, g be Function, y be object such that

           A2: t = [x, y] and

           A3: x in ( dom ( OPER A)) and

           A4: g = (( OPER A) . x) & y in ( dom g) by FUNCT_5:def 2;

          reconsider x as Element of I by A3, PARTFUN1:def 2;

          ex U0 be MSAlgebra over S st U0 = (A . x) & (( OPER A) . x) = the Charact of U0 by A1, Def11;

          then

           A5: y in the carrier' of S by A4, PARTFUN1:def 2;

          x in I by A3, PARTFUN1:def 2;

          hence thesis by A2, A5, ZFMISC_1: 87;

        end;

        let x be object;

        assume

         A6: x in [:I, the carrier' of S:];

        then

        consider y,z be object such that

         A7: x = [y, z] by RELAT_1:def 1;

        

         A8: z in the carrier' of S by A6, A7, ZFMISC_1: 87;

        reconsider y as Element of I by A6, A7, ZFMISC_1: 87;

        consider U0 be MSAlgebra over S such that U0 = (A . y) and

         A9: (( OPER A) . y) = the Charact of U0 by A1, Def11;

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

        hence thesis by A1, A7, A8, A9, FUNCT_5:def 2;

      end;

        suppose

         A10: I = {} ;

        then ( OPER A) = {} ;

        hence thesis by A10, FUNCT_5: 43, RELAT_1: 38, ZFMISC_1: 90;

      end;

    end;

    theorem :: PRALG_2:6

    

     Th6: for I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S holds ( commute ( OPER A)) in ( Funcs (the carrier' of S,( Funcs (I,( rng ( uncurry ( OPER A)))))))

    proof

      let I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S;

      set f = ( uncurry ( OPER A));

      ( dom f) = [:I, the carrier' of S:] by Th5;

      then [:I, the carrier' of S:] <> {} & f in ( Funcs ( [:I, the carrier' of S:],( rng f))) by FUNCT_2:def 2, ZFMISC_1: 90;

      hence thesis by FUNCT_6: 10;

    end;

    definition

      let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S;

      :: PRALG_2:def12

      func A ?. o -> ManySortedFunction of I equals (( commute ( OPER A)) . o);

      coherence

      proof

        set f = ( uncurry ( OPER A)), C = ( commute ( OPER A));

        

         A1: ( dom f) = [:I, the carrier' of S:] by Th5;

        per cases ;

          suppose

           A2: I <> {} ;

          then C in ( Funcs (the carrier' of S,( Funcs (I,( rng f))))) by Th6;

          then

           A3: ex a be Function st a = C & ( dom a) = the carrier' of S & ( rng a) c= ( Funcs (I,( rng f))) by FUNCT_2:def 2;

          then (C . o) in ( rng C) by FUNCT_1:def 3;

          then

          consider g be Function such that

           A4: g = (C . o) and

           A5: ( dom g) = I and ( rng g) c= ( rng f) by A3, FUNCT_2:def 2;

          reconsider g as ManySortedSet of I by A5, PARTFUN1:def 2, RELAT_1:def 18;

          for x be object st x in ( dom g) holds (g . x) is Function

          proof

            let x be object;

            assume x in ( dom g);

            then

            reconsider i = x as Element of I by A5;

            

             A6: ( [i, o] `1 ) = i & ( [i, o] `2 ) = o;

            consider U0 be MSAlgebra over S such that U0 = (A . i) and

             A7: (( OPER A) . i) = the Charact of U0 by A2, Def11;

            

             A8: [i, o] in ( dom f) by A1, A2, ZFMISC_1: 87;

            then (g . i) = (f . (i,o)) by A4, FUNCT_5: 22;

            

            then (g . i) = (the Charact of U0 . o) by A8, A6, A7, FUNCT_5:def 2

            .= ( Den (o,U0)) by MSUALG_1:def 6;

            hence thesis;

          end;

          hence thesis by A4, FUNCOP_1:def 6;

        end;

          suppose

           A9: I = {} ;

          reconsider f = ( EmptyMS I) as ManySortedFunction of I;

          f = {} by A9

          .= (( commute {} ) . o) by FUNCT_6: 58

          .= (( commute ( OPER A)) . o) by A9;

          hence thesis;

        end;

      end;

    end

    theorem :: PRALG_2:7

    

     Th7: for I be non empty set, i be Element of I, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S holds ((A ?. o) . i) = ( Den (o,(A . i)))

    proof

      let I be non empty set, i be Element of I, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S;

      set O = the carrier' of S, f = ( uncurry ( OPER A));

      

       A1: ( [i, o] `1 ) = i & ( [i, o] `2 ) = o;

      

       A2: ex U0 be MSAlgebra over S st U0 = (A . i) & (( OPER A) . i) = the Charact of U0 by Def11;

      

       A3: ( dom f) = [:I, O:] by Th5;

      then

       A4: [i, o] in ( dom f) by ZFMISC_1: 87;

      consider g be Function such that

       A5: (( curry' f) . o) = g and ( dom g) = I and ( rng g) c= ( rng f) and

       A6: for x st x in I holds (g . x) = (f . (x,o)) by A3, FUNCT_5: 32, ZFMISC_1: 90;

      (g . i) = (f . (i,o)) by A6;

      

      then (g . i) = (the Charact of (A . i) . o) by A4, A1, A2, FUNCT_5:def 2

      .= ( Den (o,(A . i))) by MSUALG_1:def 6;

      hence thesis by A5;

    end;

    theorem :: PRALG_2:8

    for I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S, x be set st x in ( rng ( Frege (A ?. o))) holds x is Function

    proof

      let I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S, x be set;

      assume x in ( rng ( Frege (A ?. o)));

      then ex y be object st y in ( dom ( Frege (A ?. o))) & (( Frege (A ?. o)) . y) = x by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: PRALG_2:9

    

     Th9: for I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S, f be Function st f in ( rng ( Frege (A ?. o))) holds ( dom f) = I & for i be Element of I holds (f . i) in ( Result (o,(A . i)))

    proof

      let I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S, f be Function;

      

       A1: ( dom (A ?. o)) = I by PARTFUN1:def 2;

      assume f in ( rng ( Frege (A ?. o)));

      then

      consider y be object such that

       A2: y in ( dom ( Frege (A ?. o))) and

       A3: (( Frege (A ?. o)) . y) = f by FUNCT_1:def 3;

      

       A4: ( dom ( Frege (A ?. o))) = ( product ( doms (A ?. o))) by PARTFUN1:def 2;

      then

      consider g be Function such that

       A5: g = y and

       a5: ( dom g) = ( dom ( doms (A ?. o))) and

       A6: for i be object st i in ( dom ( doms (A ?. o))) holds (g . i) in (( doms (A ?. o)) . i) by A2, CARD_3:def 5;

      

       ab: ( dom ( doms (A ?. o))) = ( dom (A ?. o)) by FUNCT_6:def 2

      .= I by PARTFUN1:def 2;

      

       A7: f = ((A ?. o) .. g) by A2, A3, A4, A5, Def2;

      then ( dom f) = (( dom (A ?. o)) /\ ( dom g)) by PRALG_1:def 19;

      

      hence

       a8: ( dom f) = (I /\ ( dom g)) by PARTFUN1:def 2

      .= I by ab, a5;

      let i be Element of I;

      

       A8: ((A ?. o) . i) = ( Den (o,(A . i))) by Th7;

      ( dom ( doms (A ?. o))) = ( dom (A ?. o)) by FUNCT_6:def 2;

      then (g . i) in (( doms (A ?. o)) . i) by A6, A1;

      then

       A9: (g . i) in ( dom ( Den (o,(A . i)))) by A1, A8, FUNCT_6: 22;

      (f . i) = (( Den (o,(A . i))) . (g . i)) by a8, A7, A8, PRALG_1:def 19;

      then

       A10: (f . i) in ( rng ( Den (o,(A . i)))) by A9, FUNCT_1:def 3;

      ( rng ( Den (o,(A . i)))) c= ( Result (o,(A . i))) by RELAT_1:def 19;

      hence thesis by A10;

    end;

    theorem :: PRALG_2:10

    

     Th10: for I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S, f be Function st f in ( dom ( Frege (A ?. o))) holds ( dom f) = I & (for i be Element of I holds (f . i) in ( Args (o,(A . i)))) & ( rng f) c= ( Funcs (( dom ( the_arity_of o)), |.A.|))

    proof

      let I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S, f be Function;

      assume

       A1: f in ( dom ( Frege (A ?. o)));

      

       A2: ( dom (A ?. o)) = I by PARTFUN1:def 2;

      

       A3: ( dom ( Frege (A ?. o))) = ( product ( doms (A ?. o))) by PARTFUN1:def 2;

      

       A4: ( dom ( doms (A ?. o))) = ( dom (A ?. o)) by FUNCT_6:def 2;

      hence ( dom f) = I by A1, A3, A2, CARD_3: 9;

      thus

       A5: for i be Element of I holds (f . i) in ( Args (o,(A . i)))

      proof

        let i be Element of I;

        ((A ?. o) . i) = ( Den (o,(A . i))) & (f . i) in (( doms (A ?. o)) . i) by A1, A3, A2, A4, Th7, CARD_3: 9;

        then (f . i) in ( dom ( Den (o,(A . i)))) by A2, FUNCT_6: 22;

        hence thesis by FUNCT_2:def 1;

      end;

      let x be object;

      assume x in ( rng f);

      then

      consider y be object such that

       A6: y in ( dom f) and

       A7: x = (f . y) by FUNCT_1:def 3;

      reconsider y as Element of I by A1, A3, A2, A4, A6, CARD_3: 9;

      set X = the carrier' of S, AS = ((the Sorts of (A . y) # ) * the Arity of S), Ar = the Arity of S, Cr = the carrier of S, So = the Sorts of (A . y), a = ( the_arity_of o);

      

       A8: ( dom Ar) = X by FUNCT_2:def 1;

      then

       A9: ( dom AS) = ( dom Ar) by PARTFUN1:def 2;

      

       A10: ( Args (o,(A . y))) = (AS . o) by MSUALG_1:def 4

      .= ((So # ) qua ManySortedSet of (Cr * ) . (Ar . o)) by A8, A9, FUNCT_1: 12

      .= ((So # ) qua ManySortedSet of (Cr * ) . ( the_arity_of o)) by MSUALG_1:def 1

      .= ( product (So * ( the_arity_of o))) by FINSEQ_2:def 5;

      x in ( Args (o,(A . y))) by A5, A7;

      then

      consider g be Function such that

       A11: g = x and

       A12: ( dom g) = ( dom (So * a)) and

       A13: for i be object st i in ( dom (So * a)) holds (g . i) in ((So * a) . i) by A10, CARD_3:def 5;

      

       A14: ( rng a) c= Cr & ( dom So) = Cr by FINSEQ_1:def 4, PARTFUN1:def 2;

      then

       A15: ( dom (So * a)) = ( dom a) by RELAT_1: 27;

      

       A16: ( rng g) c= |.(A . y).|

      proof

        let i be object;

        assume i in ( rng g);

        then

        consider j be object such that

         A17: j in ( dom g) and

         A18: (g . j) = i by FUNCT_1:def 3;

        (a . j) in ( rng a) by A12, A15, A17, FUNCT_1:def 3;

        then

         A19: (So . (a . j)) in ( rng So) by A14, FUNCT_1:def 3;

        i in ((So * a) . j) by A12, A13, A17, A18;

        then i in (So . (a . j)) by A12, A17, FUNCT_1: 12;

        hence thesis by A19, TARSKI:def 4;

      end;

       |.(A . y).| in the set of all |.(A . i).| where i be Element of I;

      then |.(A . y).| c= ( union the set of all |.(A . i).| where i be Element of I) by ZFMISC_1: 74;

      then ( rng g) c= |.A.| by A16;

      hence thesis by A11, A12, A15, FUNCT_2:def 2;

    end;

    theorem :: PRALG_2:11

    

     Th11: for I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S holds ( dom ( doms (A ?. o))) = I & for i be Element of I holds (( doms (A ?. o)) . i) = ( Args (o,(A . i)))

    proof

      let I be non empty set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S, o be OperSymbol of S;

      

       A1: ( dom (A ?. o)) = I by PARTFUN1:def 2;

      for i be Element of I holds (( doms (A ?. o)) . i) = ( Args (o,(A . i)))

      proof

        let i be Element of I;

        ((A ?. o) . i) = ( Den (o,(A . i))) by Th7;

        then (( doms (A ?. o)) . i) = ( dom ( Den (o,(A . i)))) by A1, FUNCT_6: 22;

        hence thesis by FUNCT_2:def 1;

      end;

      hence thesis by A1, FUNCT_6:def 2;

    end;

    definition

      let I;

      let S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S;

      :: PRALG_2:def13

      func OPS (A) -> ManySortedFunction of ((( SORTS A) # ) * the Arity of S), (( SORTS A) * the ResultSort of S) means for o be OperSymbol of S holds (it . o) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) if I <> {}

      otherwise not contradiction;

      existence

      proof

        defpred P[ object, object] means for o be OperSymbol of S st $1 = o holds $2 = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o)))));

        set X = the carrier' of S, AS = ((( SORTS A) # ) * the Arity of S), RS = (( SORTS A) * the ResultSort of S);

        

         A1: for x be object st x in X holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in X;

          then

          reconsider o = x as OperSymbol of S;

          take ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o)))));

          let o1 be OperSymbol of S;

          assume x = o1;

          hence thesis;

        end;

        consider f be Function such that

         A2: ( dom f) = X & for x be object st x in X holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        reconsider f as ManySortedSet of X by A2, PARTFUN1:def 2, RELAT_1:def 18;

        for x be object st x in ( dom f) holds (f . x) is Function

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider o = x as OperSymbol of S by A2;

          per cases ;

            suppose

             A3: ( the_arity_of o) = {} ;

            (f . x) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by A2

            .= ( commute (A ?. o)) by A3, FUNCOP_1:def 8;

            hence thesis;

          end;

            suppose

             A4: ( the_arity_of o) <> {} ;

            (f . x) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by A2

            .= ( Commute ( Frege (A ?. o))) by A4, FUNCOP_1:def 8;

            hence thesis;

          end;

        end;

        then

        reconsider f as ManySortedFunction of X by FUNCOP_1:def 6;

        hereby

          assume I <> {} ;

          then

          reconsider I9 = I as non empty set;

          reconsider A9 = A as MSAlgebra-Family of I9, S;

          for x st x in X holds (f . x) is Function of (AS . x), (RS . x)

          proof

            let x;

            assume x in X;

            then

            reconsider o = x as OperSymbol of S;

            set ar = ( the_arity_of o);

            set C = ( Commute ( Frege (A ?. o))), F = ( Frege (A ?. o)), Ar = the Arity of S, Rs = the ResultSort of S, Cr = the carrier of S, co = ( commute (A ?. o));

            

             A5: ( rng ar) c= Cr by FINSEQ_1:def 4;

            

             A6: ( dom Ar) = X by FUNCT_2:def 1;

            then ( dom AS) = ( dom Ar) by PARTFUN1:def 2;

            

            then

             A7: (AS . o) = ((( SORTS A) # ) qua ManySortedSet of (Cr * ) . (Ar . o)) by A6, FUNCT_1: 12

            .= ((( SORTS A) # ) qua ManySortedSet of (Cr * ) . ( the_arity_of o)) by MSUALG_1:def 1

            .= ( product (( SORTS A) * ( the_arity_of o))) by FINSEQ_2:def 5;

            

             A8: ( dom Rs) = X by FUNCT_2:def 1;

            then ( dom RS) = ( dom Rs) by PARTFUN1:def 2;

            

            then

             A9: (RS . o) = (( SORTS A) . (Rs . o)) by A8, FUNCT_1: 12

            .= (( SORTS A) . ( the_result_sort_of o)) by MSUALG_1:def 2

            .= ( product ( Carrier (A,( the_result_sort_of o)))) by Def10;

            ( dom ( SORTS A)) = Cr by PARTFUN1:def 2;

            then

             A10: ( dom (( SORTS A) * ar)) = ( dom ar) by A5, RELAT_1: 27;

            per cases ;

              suppose

               A11: ( the_arity_of o) = {} ;

              set rs = ( the_result_sort_of o);

              

               A12: ( rng (A ?. o)) c= ( Funcs ( { {} }, |.A9.|))

              proof

                let j be object;

                assume j in ( rng (A ?. o));

                then

                consider a be object such that

                 A13: a in ( dom (A ?. o)) and

                 A14: ((A ?. o) . a) = j by FUNCT_1:def 3;

                reconsider i = a as Element of I9 by A13, PARTFUN1:def 2;

                set So = the Sorts of (A9 . i);

                 |.(A9 . i).| in the set of all |.(A9 . d).| where d be Element of I9;

                then

                 A15: |.(A9 . i).| c= ( union the set of all |.(A9 . d).| where d be Element of I9) by ZFMISC_1: 74;

                ( dom the Sorts of (A9 . i)) = the carrier of S by PARTFUN1:def 2;

                then (So . rs) in ( rng the Sorts of (A9 . i)) by FUNCT_1:def 3;

                then

                 A16: (So . rs) c= ( union ( rng the Sorts of (A9 . i))) by ZFMISC_1: 74;

                ( rng ( Den (o,(A9 . i)))) c= ( Result (o,(A9 . i))) & ( Result (o,(A9 . i))) = (So . rs) by Th3, RELAT_1:def 19;

                then

                 A17: ( rng ( Den (o,(A9 . i)))) c= |.A9.| by A15, A16;

                

                 A18: ( dom ( Den (o,(A9 . i)))) = ( Args (o,(A9 . i))) & ( Args (o,(A9 . i))) = { {} } by A11, Th4, FUNCT_2:def 1;

                j = ( Den (o,(A9 . i))) by A14, Th7;

                hence thesis by A18, A17, FUNCT_2:def 2;

              end;

              ( dom (A ?. o)) = I by PARTFUN1:def 2;

              then

               A19: (A ?. o) in ( Funcs (I,( Funcs ( { {} }, |.A9.|)))) by A12, FUNCT_2:def 2;

              then ( commute (A ?. o)) in ( Funcs ( { {} },( Funcs (I, |.A9.|)))) by FUNCT_6: 55;

              then

               A20: ex h be Function st h = co & ( dom h) = { {} } & ( rng h) c= ( Funcs (I, |.A9.|)) by FUNCT_2:def 2;

              

               A21: ( rng co) c= (RS . o)

              proof

                let j be object;

                

                 A22: ( dom ( Carrier (A,rs))) = I by PARTFUN1:def 2;

                assume

                 A23: j in ( rng co);

                then

                consider a be object such that

                 A24: a in ( dom co) and

                 A25: (co . a) = j by FUNCT_1:def 3;

                reconsider h = j as Function by A25;

                

                 A26: for b be object st b in ( dom ( Carrier (A,rs))) holds (h . b) in (( Carrier (A,rs)) . b)

                proof

                  let b be object;

                  assume b in ( dom ( Carrier (A,rs)));

                  then

                  reconsider i = b as Element of I9 by PARTFUN1:def 2;

                  

                   A27: ex U0 be MSAlgebra over S st U0 = (A . i) & (( Carrier (A,rs)) . i) = (the Sorts of U0 . rs) by Def9;

                  ( dom ( Den (o,(A9 . i)))) = ( Args (o,(A9 . i))) by FUNCT_2:def 1

                  .= { {} } by A11, Th4;

                  then

                   A28: (( Den (o,(A9 . i))) . a) in ( rng ( Den (o,(A9 . i)))) by A20, A24, FUNCT_1:def 3;

                  ((A ?. o) . i) = ( Den (o,(A9 . i))) by Th7;

                  then

                   A29: (( Den (o,(A9 . i))) . a) = (h . i) by A19, A20, A24, A25, FUNCT_6: 56;

                  ( rng ( Den (o,(A9 . i)))) c= ( Result (o,(A9 . i))) by RELAT_1:def 19;

                  then (h . i) in ( Result (o,(A9 . i))) by A29, A28;

                  hence thesis by A27, Th3;

                end;

                ex k be Function st k = h & ( dom k) = I & ( rng k) c= |.A9.| by A20, A23, FUNCT_2:def 2;

                hence thesis by A9, A22, A26, CARD_3: 9;

              end;

              

               A30: (AS . o) = { {} } by A7, A11, CARD_3: 10;

              (f . x) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by A2

              .= ( commute (A ?. o)) by A11, FUNCOP_1:def 8;

              hence thesis by A30, A20, A21, FUNCT_2: 2;

            end;

              suppose

               A31: ( the_arity_of o) <> {} ;

              

               A32: ( dom C) = (AS . o)

              proof

                thus ( dom C) c= (AS . o)

                proof

                  let j be object;

                  assume j in ( dom C);

                  then

                  consider g be Function such that

                   A33: g in ( dom F) and

                   A34: j = ( commute g) by Def1;

                  set cg = ( commute g);

                  

                   A35: ( rng g) c= ( Funcs (( dom ar), |.A9.|)) by A33, Th10;

                  

                   A36: ( dom g) = I9 by A33, Th10;

                  then

                   A37: g in ( Funcs (I,( Funcs (( dom ar), |.A9.|)))) by A35, FUNCT_2:def 2;

                  then ( commute g) in ( Funcs (( dom ar),( Funcs (I, |.A9.|)))) by A31, FUNCT_6: 55;

                  then

                   A38: ex h be Function st h = ( commute g) & ( dom h) = ( dom ar) & ( rng h) c= ( Funcs (I, |.A9.|)) by FUNCT_2:def 2;

                  for y be object st y in ( dom (( SORTS A) * ar)) holds (cg . y) in ((( SORTS A) * ar) . y)

                  proof

                    let y be object;

                    assume

                     A39: y in ( dom (( SORTS A) * ar));

                    then (ar . y) in ( rng ar) by A10, FUNCT_1:def 3;

                    then

                    reconsider s = (ar . y) as SortSymbol of S by A5;

                    (cg . y) in ( rng cg) by A10, A38, A39, FUNCT_1:def 3;

                    then

                    consider h be Function such that

                     A40: h = (cg . y) and

                     A41: ( dom h) = I and ( rng h) c= |.A9.| by A38, FUNCT_2:def 2;

                    

                     A42: for z be object st z in ( dom ( Carrier (A,s))) holds (h . z) in (( Carrier (A,s)) . z)

                    proof

                      let z be object;

                      assume z in ( dom ( Carrier (A,s)));

                      then

                      reconsider i = z as Element of I9 by PARTFUN1:def 2;

                      

                       A43: ( dom ((the Sorts of (A9 . i) # ) * Ar)) = X by PARTFUN1:def 2;

                      

                       A44: ( Args (o,(A9 . i))) = (((the Sorts of (A9 . i) # ) * Ar) . o) by MSUALG_1:def 4

                      .= ((the Sorts of (A9 . i) # ) qua ManySortedSet of (Cr * ) . (Ar . o)) by A43, FUNCT_1: 12

                      .= ((the Sorts of (A9 . i) # ) qua ManySortedSet of (Cr * ) . ar) by MSUALG_1:def 1

                      .= ( product (the Sorts of (A9 . i) * ar)) by FINSEQ_2:def 5;

                      (g . i) in ( rng g) by A36, FUNCT_1:def 3;

                      then

                      consider f be Function such that

                       A45: f = (g . i) and ( dom f) = ( dom ar) and ( rng f) c= |.A9.| by A35, FUNCT_2:def 2;

                      

                       A46: ex U0 be MSAlgebra over S st U0 = (A . i) & (( Carrier (A,s)) . i) = (the Sorts of U0 . s) by Def9;

                      ( dom the Sorts of (A9 . i)) = Cr by PARTFUN1:def 2;

                      then

                       A47: ( dom (the Sorts of (A9 . i) * ar)) = ( dom ar) by A5, RELAT_1: 27;

                      then

                       A48: ((the Sorts of (A9 . i) * ar) . y) = (the Sorts of (A9 . i) . s) by A10, A39, FUNCT_1: 12;

                      (g . i) in ( Args (o,(A9 . i))) by A33, Th10;

                      then (f . y) in ((the Sorts of (A9 . i) * ar) . y) by A10, A39, A45, A44, A47, CARD_3: 9;

                      hence thesis by A10, A37, A39, A40, A46, A45, A48, FUNCT_6: 56;

                    end;

                    

                     A49: ( dom ( Carrier (A,s))) = I by PARTFUN1:def 2;

                    ((( SORTS A) * ar) . y) = (( SORTS A) . s) by A39, FUNCT_1: 12

                    .= ( product ( Carrier (A,s))) by Def10;

                    hence thesis by A49, A40, A41, A42, CARD_3: 9;

                  end;

                  hence thesis by A7, A10, A34, A38, CARD_3: 9;

                end;

                let i be object;

                assume i in (AS . o);

                then

                consider g be Function such that

                 A50: g = i and

                 A51: ( dom g) = ( dom (( SORTS A) * ar)) and

                 A52: for x be object st x in ( dom (( SORTS A) * ar)) holds (g . x) in ((( SORTS A) * ar) . x) by A7, CARD_3:def 5;

                

                 A53: ( rng g) c= ( Funcs (I, |.A9.|))

                proof

                  let a be object;

                  assume a in ( rng g);

                  then

                  consider b be object such that

                   A54: b in ( dom g) and

                   A55: (g . b) = a by FUNCT_1:def 3;

                  (ar . b) in ( rng ar) by A10, A51, A54, FUNCT_1:def 3;

                  then

                  reconsider cr = (ar . b) as SortSymbol of S by A5;

                  

                   A56: ((( SORTS A) * ar) . b) = (( SORTS A) . cr) by A51, A54, FUNCT_1: 12

                  .= ( product ( Carrier (A,cr))) by Def10;

                  a in ((( SORTS A) * ar) . b) by A51, A52, A54, A55;

                  then

                  consider h be Function such that

                   A57: h = a and

                   A58: ( dom h) = ( dom ( Carrier (A,cr))) and

                   A59: for j be object st j in ( dom ( Carrier (A,cr))) holds (h . j) in (( Carrier (A,cr)) . j) by A56, CARD_3:def 5;

                  

                   A60: ( rng h) c= |.A9.|

                  proof

                    let j be object;

                    assume j in ( rng h);

                    then

                    consider c be object such that

                     A61: c in ( dom h) and

                     A62: (h . c) = j by FUNCT_1:def 3;

                    reconsider i = c as Element of I9 by A58, A61, PARTFUN1:def 2;

                    (ex U0 be MSAlgebra over S st U0 = (A . i) & (( Carrier (A,cr)) . i) = (the Sorts of U0 . cr)) & ( dom the Sorts of (A9 . i)) = the carrier of S by Def9, PARTFUN1:def 2;

                    then

                     A63: (( Carrier (A,cr)) . i) in ( rng the Sorts of (A9 . i)) by FUNCT_1:def 3;

                    (h . i) in (( Carrier (A,cr)) . i) by A58, A59, A61;

                    then

                     A64: (h . i) in |.(A9 . i).| by A63, TARSKI:def 4;

                     |.(A9 . i).| in the set of all |.(A9 . d).| where d be Element of I9;

                    hence thesis by A62, A64, TARSKI:def 4;

                  end;

                  ( dom ( Carrier (A,cr))) = I by PARTFUN1:def 2;

                  hence thesis by A57, A58, A60, FUNCT_2:def 2;

                end;

                then

                 A65: g in ( Funcs (( dom ar),( Funcs (I, |.A9.|)))) by A10, A51, FUNCT_2:def 2;

                then

                 A66: ( commute ( commute g)) = g by A31, FUNCT_6: 57;

                ( commute g) in ( Funcs (I,( Funcs (( dom ar), |.A9.|)))) by A31, A65, FUNCT_6: 55;

                then

                 A67: ex h be Function st h = ( commute g) & ( dom h) = I & ( rng h) c= ( Funcs (( dom ar), |.A9.|)) by FUNCT_2:def 2;

                

                 A68: for j be object st j in ( dom ( doms (A ?. o))) holds (( commute g) . j) in (( doms (A ?. o)) . j)

                proof

                  set cg = ( commute g);

                  let j be object;

                  assume j in ( dom ( doms (A ?. o)));

                  then

                  reconsider ii = j as Element of I9 by Th11;

                  set So = the Sorts of (A9 . ii);

                  reconsider h = (cg . ii) as Function;

                  h in ( rng cg) by A67, FUNCT_1:def 3;

                  then

                   A69: ex s be Function st s = h & ( dom s) = ( dom ar) & ( rng s) c= |.A9.| by A67, FUNCT_2:def 2;

                  

                   A70: ( dom (the Sorts of (A9 . ii) * ar)) = ( dom ar) by Th3;

                  

                   A71: for a be object st a in ( dom (So * ar)) holds (h . a) in ((So * ar) . a)

                  proof

                    let a be object;

                    assume

                     A72: a in ( dom (So * ar));

                    then (ar . a) in ( rng ar) by A70, FUNCT_1:def 3;

                    then

                    reconsider s = (ar . a) as SortSymbol of S by A5;

                    

                     A73: ((So * ar) . a) = (So . s) by A72, FUNCT_1: 12;

                    (g . a) in ( rng g) by A10, A51, A70, A72, FUNCT_1:def 3;

                    then

                    consider k be Function such that

                     A74: k = (g . a) and ( dom k) = I and ( rng k) c= |.A9.| by A53, FUNCT_2:def 2;

                    

                     A75: (ex U0 be MSAlgebra over S st U0 = (A9 . ii) & (( Carrier (A,s)) . ii) = (the Sorts of U0 . s)) & ( dom ( Carrier (A,s))) = I by Def9, PARTFUN1:def 2;

                    

                     A76: ((( SORTS A) * ar) . a) = (( SORTS A) . s) by A10, A70, A72, FUNCT_1: 12

                    .= ( product ( Carrier (A,s))) by Def10;

                    (k . ii) = (h . a) & k in ((( SORTS A) * ar) . a) by A10, A52, A65, A70, A72, A74, FUNCT_6: 56;

                    hence thesis by A73, A76, A75, CARD_3: 9;

                  end;

                  (( doms (A ?. o)) . ii) = ( Args (o,(A9 . ii))) & ( Args (o,(A9 . ii))) = ( product (the Sorts of (A9 . ii) * ar)) by Th3, Th11;

                  hence thesis by A70, A69, A71, CARD_3: 9;

                end;

                ( dom F) = ( product ( doms (A ?. o))) & ( dom ( doms (A ?. o))) = I9 by Th11, PARTFUN1:def 2;

                then ( commute g) in ( dom F) by A67, A68, CARD_3: 9;

                hence thesis by A50, A66, Def1;

              end;

              set rs = ( the_result_sort_of o), CA = ( Carrier (A,rs));

              

               A77: ( rng C) c= (RS . o)

              proof

                let x be object;

                

                 A78: ( dom CA) = I by PARTFUN1:def 2;

                assume x in ( rng C);

                then

                consider g be object such that

                 A79: g in ( dom C) and

                 A80: (C . g) = x by FUNCT_1:def 3;

                consider f be Function such that

                 A81: f in ( dom ( Frege (A ?. o))) and

                 A82: g = ( commute f) by A79, Def1;

                reconsider g as Function by A82;

                ( dom f) = I9 & ( rng f) c= ( Funcs (( dom ( the_arity_of o)), |.A9.|)) by A81, Th10;

                then f in ( Funcs (I,( Funcs (( dom ( the_arity_of o)), |.A9.|)))) by FUNCT_2:def 2;

                then ( commute g) = f by A31, A82, FUNCT_6: 57;

                then

                 A83: x = (F . f) by A79, A80, Def1;

                then

                reconsider h = x as Function;

                

                 A84: (F . f) in ( rng F) by A81, FUNCT_1:def 3;

                

                 A85: for j be object st j in ( dom CA) holds (h . j) in (CA . j)

                proof

                  let j be object;

                  assume j in ( dom CA);

                  then

                  reconsider i = j as Element of I9 by PARTFUN1:def 2;

                  

                   A86: ( dom (the Sorts of (A9 . i) * Rs)) = ( dom Rs) by A8, PARTFUN1:def 2;

                  

                   A87: ex U0 be MSAlgebra over S st U0 = (A9 . i) & (CA . i) = (the Sorts of U0 . rs) by Def9;

                  ( Result (o,(A9 . i))) = ((the Sorts of (A9 . i) * Rs) . o) by MSUALG_1:def 5

                  .= (the Sorts of (A9 . i) . (Rs . o)) by A8, A86, FUNCT_1: 12

                  .= (CA . i) by A87, MSUALG_1:def 2;

                  hence thesis by A83, A84, Th9;

                end;

                ( dom h) = I9 by A83, A84, Th9;

                hence thesis by A9, A78, A85, CARD_3: 9;

              end;

              (f . x) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by A2

              .= ( Commute ( Frege (A ?. o))) by A31, FUNCOP_1:def 8;

              hence thesis by A32, A77, FUNCT_2: 2;

            end;

          end;

          then

          reconsider f as ManySortedFunction of AS, RS by PBOOLE:def 15;

          take f;

          let o be OperSymbol of S;

          thus (f . o) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by A2;

        end;

        assume I = {} ;

        set f = the ManySortedFunction of ((( SORTS A) # ) * the Arity of S), (( SORTS A) * the ResultSort of S);

        take f;

      end;

      uniqueness

      proof

        let f,g be ManySortedFunction of ((( SORTS A) # ) * the Arity of S), (( SORTS A) * the ResultSort of S);

        hereby

          assume I <> {} ;

          assume that

           A88: for o be OperSymbol of S holds (f . o) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) and

           A89: for o be OperSymbol of S holds (g . o) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o)))));

          for i be object st i in the carrier' of S holds (f . i) = (g . i)

          proof

            let i be object;

            assume i in the carrier' of S;

            then

            reconsider o = i as Element of the carrier' of S;

            (f . o) = ( IFEQ (( the_arity_of o), {} ,( commute (A ?. o)),( Commute ( Frege (A ?. o))))) by A88;

            hence thesis by A89;

          end;

          hence f = g;

        end;

        assume

         A90: I = {} ;

         A91:

        now

          let o be object;

          assume

           A92: o in the carrier' of S;

          then

          reconsider s = (the ResultSort of S . o) as SortSymbol of S by FUNCT_2: 5;

          o in ( dom the ResultSort of S) by A92, FUNCT_2:def 1;

          

          then

           A93: ((( SORTS A) * the ResultSort of S) . o) = (( SORTS A) . s) by FUNCT_1: 13

          .= ( product ( Carrier (A,s))) by Def10

          .= { {} } by A90, CARD_3: 10;

          (f . o) is Function of (((( SORTS A) # ) * the Arity of S) . o), ((( SORTS A) * the ResultSort of S) . o) & (g . o) is Function of (((( SORTS A) # ) * the Arity of S) . o), ((( SORTS A) * the ResultSort of S) . o) by A92, PBOOLE:def 15;

          hence (f . o) = (g . o) by A93, FUNCT_2: 51;

        end;

        thus thesis by A91;

      end;

      correctness ;

    end

    definition

      let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S;

      :: PRALG_2:def14

      func product A -> MSAlgebra over S equals MSAlgebra (# ( SORTS A), ( OPS A) #);

      coherence ;

    end

    registration

      let I be set, S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S;

      cluster ( product A) -> strict;

      coherence ;

    end

    theorem :: PRALG_2:12

    for S be non void non empty ManySortedSign, A be MSAlgebra-Family of I, S holds the Sorts of ( product A) = ( SORTS A) & the Charact of ( product A) = ( OPS A);