pua2mss1.miz



    begin

    

     Lm1: for p be FinSequence, f be Function st ( dom f) = ( dom p) holds f is FinSequence

    proof

      let p be FinSequence;

      ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 2;

    end;

    

     Lm2: for X be set, Y be non empty set holds for p be FinSequence of X, f be Function of X, Y holds (f * p) is FinSequence of Y

    proof

      let X be set, Y be non empty set;

      let p be FinSequence of X, f be Function of X, Y;

      

       A1: ( rng p) c= X;

      ( dom f) = X by FUNCT_2:def 1;

      then ( dom (f * p)) = ( dom p) by A1, RELAT_1: 27;

      then

       A2: (f * p) is FinSequence by Lm1;

      ( rng (f * p)) c= Y;

      hence thesis by A2, FINSEQ_1:def 4;

    end;

    registration

      let X be with_non-empty_elements set;

      cluster -> non-empty for FinSequence of X;

      coherence

      proof

        let p be FinSequence of X;

        let x be object;

        assume x in ( dom p);

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

        hence thesis;

      end;

    end

    registration

      let A be non empty set;

      cluster homogeneous quasi_total non-empty non empty for PFuncFinSequence of A;

      existence

      proof

        set a = the homogeneous quasi_total non empty PartFunc of (A * ), A;

        reconsider a as Element of ( PFuncs ((A * ),A)) by PARTFUN1: 45;

        take <*a*>;

        hereby

          let n be Nat, h be PartFunc of (A * ), A;

          assume n in ( dom <*a*>);

          then n in ( Seg 1) by FINSEQ_1: 38;

          then n = 1 by FINSEQ_1: 2, TARSKI:def 1;

          hence h = ( <*a*> . n) implies h is homogeneous by FINSEQ_1: 40;

        end;

        hereby

          let n be Nat, h be PartFunc of (A * ), A;

          assume n in ( dom <*a*>);

          then n in ( Seg 1) by FINSEQ_1: 38;

          then n = 1 by FINSEQ_1: 2, TARSKI:def 1;

          hence h = ( <*a*> . n) implies h is quasi_total by FINSEQ_1: 40;

        end;

        hereby

          let n be object;

          assume n in ( dom <*a*>);

          then n in ( Seg 1) by FINSEQ_1: 38;

          then n = 1 by FINSEQ_1: 2, TARSKI:def 1;

          hence ( <*a*> . n) is non empty by FINSEQ_1: 40;

        end;

        thus thesis;

      end;

    end

    registration

      cluster non-empty -> non empty for UAStr;

      coherence

      proof

        let A be UAStr;

        assume that

         A1: the charact of A <> {} and

         A2: the charact of A is non-empty;

        reconsider f = the charact of A as non empty Function by A1;

        set x = the Element of ( dom f);

        reconsider y = (f . x) as non empty set by A2;

        

         A3: y in ( rng f) by FUNCT_1:def 3;

        ( rng f) c= ( PFuncs ((the carrier of A * ),the carrier of A)) by FINSEQ_1:def 4;

        then

         A4: y is PartFunc of (the carrier of A * ), the carrier of A by A3, PARTFUN1: 47;

        reconsider y as non empty Function;

        thus the carrier of A is non empty by A4;

      end;

    end

    theorem :: PUA2MSS1:1

    

     Th1: for f,g be non-empty Function st ( product f) c= ( product g) holds ( dom f) = ( dom g) & for x be set st x in ( dom f) holds (f . x) c= (g . x)

    proof

      let f,g be non-empty Function;

      assume

       A1: ( product f) c= ( product g);

      set h = the Element of ( product f);

      h in ( product f);

      then

       A2: ex i be Function st h = i & ( dom i) = ( dom g) & for x be object st x in ( dom g) holds (i . x) in (g . x) by A1, CARD_3:def 5;

      

       A3: ex i be Function st h = i & ( dom i) = ( dom f) & for x be object st x in ( dom f) holds (i . x) in (f . x) by CARD_3:def 5;

      hence ( dom f) = ( dom g) by A2;

      let x be set;

      assume

       A4: x in ( dom f);

      let z be object;

      reconsider zz = z as set by TARSKI: 1;

      set k = the Element of ( product f);

      reconsider k as Function;

      defpred P[ object] means $1 = x;

      deffunc F1( object) = zz;

      deffunc F2( object) = (k . $1);

      consider h be Function such that

       A5: ( dom h) = ( dom f) & for y be object st y in ( dom f) holds ( P[y] implies (h . y) = F1(y)) & ( not P[y] implies (h . y) = F2(y)) from PARTFUN1:sch 1;

      assume

       A6: z in (f . x);

      now

        let y be object;

        assume

         A7: y in ( dom f);

        then y <> x implies (h . y) = (k . y) by A5;

        hence (h . y) in (f . y) by A5, A6, A7, CARD_3: 9;

      end;

      then h in ( product f) by A5, CARD_3: 9;

      then (h . x) in (g . x) by A1, A2, A3, A4, CARD_3: 9;

      hence thesis by A4, A5;

    end;

    theorem :: PUA2MSS1:2

    

     Th2: for f,g be non-empty Function st ( product f) = ( product g) holds f = g

    proof

      let f,g be non-empty Function;

      assume

       A1: ( product f) = ( product g);

      set h = the Element of ( product f);

      

       A2: ex i be Function st h = i & ( dom i) = ( dom g) & for x be object st x in ( dom g) holds (i . x) in (g . x) by A1, CARD_3:def 5;

      

       A3: ex i be Function st h = i & ( dom i) = ( dom f) & for x be object st x in ( dom f) holds (i . x) in (f . x) by CARD_3:def 5;

      then for x be object st x in ( dom f) holds (f . x) = (g . x) by A1, A2, Th1;

      hence thesis by A2, A3;

    end;

    definition

      let A be non empty set;

      let f be PFuncFinSequence of A;

      :: original: rng

      redefine

      func rng f -> Subset of ( PFuncs ((A * ),A)) ;

      coherence by FINSEQ_1:def 4;

    end

    definition

      let A,B be non empty set;

      let S be non empty Subset of ( PFuncs (A,B));

      :: original: Element

      redefine

      mode Element of S -> PartFunc of A, B ;

      coherence

      proof

        let s be Element of S;

        thus thesis by PARTFUN1: 46;

      end;

    end

    definition

      let A be non-empty UAStr;

      mode OperSymbol of A is Element of ( dom the charact of A);

      mode operation of A is Element of ( rng the charact of A);

    end

    definition

      let A be non-empty UAStr;

      let o be OperSymbol of A;

      :: PUA2MSS1:def1

      func Den (o,A) -> operation of A equals (the charact of A . o);

      correctness by FUNCT_1:def 3;

    end

    begin

    ::$Canceled

    

     Lm3: for X be set, P be a_partition of X, x,a,b be set st x in a & a in P & x in b & b in P holds a = b by EQREL_1: 70;

    theorem :: PUA2MSS1:4

    

     Th3: for X,Y be set st X is_finer_than Y holds for p be FinSequence of X holds ex q be FinSequence of Y st ( product p) c= ( product q)

    proof

      let X,Y be set;

      assume

       A1: for a be set st a in X holds ex b be set st b in Y & a c= b;

      let p be FinSequence of X;

      defpred P[ object, object] means ex D2 be set st D2 = $2 & (p . $1) c= D2;

      

       A2: for i be object st i in ( dom p) holds ex y be object st y in Y & P[i, y]

      proof

        let i be object;

        assume

         A3: i in ( dom p);

        reconsider i as set by TARSKI: 1;

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

        then (p . i) in X;

        then

        consider b be set such that

         A4: b in Y & (p . i) c= b by A1;

        take b;

        thus thesis by A4;

      end;

      consider q be Function such that

       A5: ( dom q) = ( dom p) & ( rng q) c= Y & for i be object st i in ( dom p) holds P[i, (q . i)] from FUNCT_1:sch 6( A2);

      ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

      then q is FinSequence by A5, FINSEQ_1:def 2;

      then

       A6: q is FinSequence of Y by A5, FINSEQ_1:def 4;

      for i be object st i in ( dom p) holds (p . i) c= (q . i)

      proof

        let i be object;

        assume i in ( dom p);

        then P[i, (q . i)] by A5;

        hence thesis;

      end;

      then ( product p) c= ( product q) by A5, CARD_3: 27;

      hence thesis by A6;

    end;

    theorem :: PUA2MSS1:5

    

     Th4: for X be set, P,Q be a_partition of X holds for f be Function of P, Q st for a be set st a in P holds a c= (f . a) holds for p be FinSequence of P, q be FinSequence of Q holds ( product p) c= ( product q) iff (f * p) = q

    proof

      let X be set, P,Q be a_partition of X;

      let f be Function of P, Q such that

       A1: for a be set st a in P holds a c= (f . a);

      let p be FinSequence of P, q be FinSequence of Q;

      

       A2: ( rng p) c= P;

      now

        assume P <> {} ;

        then

        reconsider X as non empty set;

        Q is a_partition of X;

        hence Q <> {} ;

      end;

      then ( dom f) = P by FUNCT_2:def 1;

      then

       A3: ( dom (f * p)) = ( dom p) by A2, RELAT_1: 27;

      hereby

        assume

         A4: ( product p) c= ( product q);

        then

         A5: ( dom p) = ( dom q) by Th1;

        now

          let x be object;

          assume

           A6: x in ( dom p);

          then

           A7: (p . x) c= (q . x) by A4, Th1;

          

           A8: (p . x) in ( rng p) by A6, FUNCT_1:def 3;

          

           A9: (q . x) in ( rng q) by A5, A6, FUNCT_1:def 3;

          reconsider Y = X as non empty set by A8;

          reconsider P9 = P, Q9 = Q as a_partition of Y;

          reconsider a = (p . x) as Element of P9 by A8;

          set z = the Element of a;

          

           A10: a c= (f . a) by A1;

          

           A11: z in a;

          (f . a) in Q9 by FUNCT_2: 5;

          then (q . x) = (f . a) by A7, A9, A10, A11, Lm3;

          hence ((f * p) . x) = (q . x) by A6, FUNCT_1: 13;

        end;

        hence (f * p) = q by A3, A5;

      end;

      assume

       A12: (f * p) = q;

      now

        let x be object;

        assume

         A13: x in ( dom p);

        then

         A14: (q . x) = (f . (p . x)) by A12, FUNCT_1: 13;

        (p . x) in ( rng p) by A13, FUNCT_1:def 3;

        hence (p . x) c= (q . x) by A1, A14;

      end;

      hence thesis by A3, A12, CARD_3: 27;

    end;

    theorem :: PUA2MSS1:6

    

     Th5: for P be set, f be Function st ( rng f) c= ( union P) holds ex p be Function st ( dom p) = ( dom f) & ( rng p) c= P & f in ( product p)

    proof

      let P be set, f be Function;

      assume

       A1: ( rng f) c= ( union P);

      defpred P[ object, object] means ex D2 be set st D2 = $2 & (f . $1) in D2;

      

       A2: for x be object st x in ( dom f) holds ex a be object st a in P & P[x, a]

      proof

        let x be object;

        assume x in ( dom f);

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

        then ex a be set st (f . x) in a & a in P by A1, TARSKI:def 4;

        hence thesis;

      end;

      consider p be Function such that

       A3: ( dom p) = ( dom f) & ( rng p) c= P and

       A4: for x be object st x in ( dom f) holds P[x, (p . x)] from FUNCT_1:sch 6( A2);

      take p;

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

      proof

        let x be object;

        assume x in ( dom f);

        then P[x, (p . x)] by A4;

        hence (f . x) in (p . x);

      end;

      hence thesis by A3, CARD_3:def 5;

    end;

    theorem :: PUA2MSS1:7

    

     Th6: for X be set, P be a_partition of X, f be FinSequence of X holds ex p be FinSequence of P st f in ( product p)

    proof

      let X be set, P be a_partition of X, f be FinSequence of X;

      

       A1: ( rng f) c= X;

      ( union P) = X by EQREL_1:def 4;

      then

      consider p be Function such that

       A2: ( dom p) = ( dom f) and

       A3: ( rng p) c= P and

       A4: f in ( product p) by A1, Th5;

      ( dom p) = ( Seg ( len f)) by A2, FINSEQ_1:def 3;

      then p is FinSequence by FINSEQ_1:def 2;

      then p is FinSequence of P by A3, FINSEQ_1:def 4;

      hence thesis by A4;

    end;

    theorem :: PUA2MSS1:8

    for X,Y be non empty set holds for P be a_partition of X, Q be a_partition of Y holds the set of all [:p, q:] where p be Element of P, q be Element of Q is a_partition of [:X, Y:]

    proof

      let X,Y be non empty set;

      let P be a_partition of X, Q be a_partition of Y;

      set PQ = the set of all [:p, q:] where p be Element of P, q be Element of Q;

      PQ c= ( bool [:X, Y:])

      proof

        let x be object;

        assume x in PQ;

        then ex p be Element of P, q be Element of Q st (x = [:p, q:]);

        hence thesis;

      end;

      then

      reconsider PQ as Subset-Family of [:X, Y:];

      PQ is a_partition of [:X, Y:]

      proof

        thus ( union PQ) = [:X, Y:]

        proof

          let x,y be object;

          thus [x, y] in ( union PQ) implies [x, y] in [:X, Y:];

          assume

           A1: [x, y] in [:X, Y:];

          then

           A2: x in X by ZFMISC_1: 87;

          

           A3: y in Y by A1, ZFMISC_1: 87;

          X = ( union P) by EQREL_1:def 4;

          then

          consider p be set such that

           A4: x in p and

           A5: p in P by A2, TARSKI:def 4;

          Y = ( union Q) by EQREL_1:def 4;

          then

          consider q be set such that

           A6: y in q and

           A7: q in Q by A3, TARSKI:def 4;

          

           A8: [x, y] in [:p, q:] by A4, A6, ZFMISC_1: 87;

           [:p, q:] in PQ by A5, A7;

          hence thesis by A8, TARSKI:def 4;

        end;

        let A be Subset of [:X, Y:];

        assume A in PQ;

        then

        consider p be Element of P, q be Element of Q such that

         A9: A = [:p, q:];

        thus A <> {} by A9;

        let B be Subset of [:X, Y:];

        assume B in PQ;

        then

        consider p1 be Element of P, q1 be Element of Q such that

         A10: B = [:p1, q1:];

        assume A <> B;

        then p <> p1 or q <> q1 by A9, A10;

        then p misses p1 or q misses q1 by EQREL_1:def 4;

        then (p /\ p1) = {} or (q /\ q1) = {} ;

        then (A /\ B) = [: {} , (q /\ q1):] or (A /\ B) = [:(p /\ p1), {} :] by A9, A10, ZFMISC_1: 100;

        then (A /\ B) = {} ;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: PUA2MSS1:9

    

     Th8: for X be non empty set holds for P be a_partition of X holds the set of all ( product p) where p be Element of (P * ) is a_partition of (X * )

    proof

      let X be non empty set;

      let P be a_partition of X;

      set PP = the set of all ( product p) where p be Element of (P * );

      PP c= ( bool (X * ))

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in PP;

        then

        consider p be Element of (P * ) such that

         A1: x = ( product p);

        xx c= (X * )

        proof

          let y be object;

          assume y in xx;

          then

          consider f be Function such that

           A2: y = f and

           A3: ( dom f) = ( dom p) and

           A4: for z be object st z in ( dom p) holds (f . z) in (p . z) by A1, CARD_3:def 5;

          ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

          then

           A5: y is FinSequence by A2, A3, FINSEQ_1:def 2;

          ( rng f) c= X

          proof

            let z be object;

            assume z in ( rng f);

            then

            consider v be object such that

             A6: v in ( dom p) and

             A7: z = (f . v) by A3, FUNCT_1:def 3;

            (p . v) in ( rng p) by A6, FUNCT_1:def 3;

            then

             A8: (p . v) in P;

            z in (p . v) by A4, A6, A7;

            hence thesis by A8;

          end;

          then y is FinSequence of X by A2, A5, FINSEQ_1:def 4;

          hence thesis by FINSEQ_1:def 11;

        end;

        hence thesis;

      end;

      then

      reconsider PP as Subset-Family of (X * );

      PP is a_partition of (X * )

      proof

        thus ( union PP) c= (X * );

        thus (X * ) c= ( union PP)

        proof

          let x be object;

          assume x in (X * );

          then

          reconsider x as FinSequence of X by FINSEQ_1:def 11;

          

           A9: ( rng x) c= X;

          ( union P) = X by EQREL_1:def 4;

          then

          consider p be Function such that

           A10: ( dom p) = ( dom x) and

           A11: ( rng p) c= P and

           A12: x in ( product p) by A9, Th5;

          ( dom p) = ( Seg ( len x)) by A10, FINSEQ_1:def 3;

          then

          reconsider p as FinSequence by FINSEQ_1:def 2;

          reconsider p as FinSequence of P by A11, FINSEQ_1:def 4;

          reconsider p as Element of (P * ) by FINSEQ_1:def 11;

          ( product p) in PP;

          hence thesis by A12, TARSKI:def 4;

        end;

        let A be Subset of (X * );

        assume A in PP;

        then

        consider p be Element of (P * ) such that

         A13: A = ( product p);

        thus A <> {} by A13;

        let B be Subset of (X * );

        assume B in PP;

        then

        consider q be Element of (P * ) such that

         A14: B = ( product q);

        assume

         A15: A <> B;

        assume A meets B;

        then

        consider x be object such that

         A16: x in A and

         A17: x in B by XBOOLE_0: 3;

        consider f be Function such that

         A18: x = f and

         A19: ( dom f) = ( dom p) and

         A20: for z be object st z in ( dom p) holds (f . z) in (p . z) by A13, A16, CARD_3:def 5;

        

         A21: ex g be Function st (x = g) & (( dom g) = ( dom q)) & (for z be object st z in ( dom q) holds (g . z) in (q . z)) by A14, A17, CARD_3:def 5;

        now

          let z be object;

          assume

           A22: z in ( dom p);

          then

           A23: (f . z) in (p . z) by A20;

          

           A24: (f . z) in (q . z) by A18, A19, A21, A22;

          

           A25: (p . z) in ( rng p) by A22, FUNCT_1:def 3;

          

           A26: (q . z) in ( rng q) by A18, A19, A21, A22, FUNCT_1:def 3;

          

           A27: (p . z) meets (q . z) by A23, A24, XBOOLE_0: 3;

          

           A28: (p . z) in P by A25;

          (q . z) in P by A26;

          hence (p . z) = (q . z) by A27, A28, EQREL_1:def 4;

        end;

        hence contradiction by A13, A14, A15, A18, A19, A21, FUNCT_1: 2;

      end;

      hence thesis;

    end;

    theorem :: PUA2MSS1:10

    for X be non empty set, n be Element of NAT holds for P be a_partition of X holds the set of all ( product p) where p be Element of (n -tuples_on P) is a_partition of (n -tuples_on X)

    proof

      let X be non empty set, n be Element of NAT ;

      let P be a_partition of X;

      set nP = (n -tuples_on P), nX = (n -tuples_on X);

      set PP = the set of all ( product p) where p be Element of nP;

      PP c= ( bool nX)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in PP;

        then

        consider p be Element of nP such that

         A1: x = ( product p);

        xx c= nX

        proof

          let y be object;

          assume y in xx;

          then

          consider f be Function such that

           A2: y = f and

           A3: ( dom f) = ( dom p) and

           A4: for z be object st z in ( dom p) holds (f . z) in (p . z) by A1, CARD_3:def 5;

          

           A5: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

          then

          reconsider y as FinSequence by A2, A3, FINSEQ_1:def 2;

          ( rng f) c= X

          proof

            let z be object;

            assume z in ( rng f);

            then

            consider v be object such that

             A6: v in ( dom p) and

             A7: z = (f . v) by A3, FUNCT_1:def 3;

            (p . v) in ( rng p) by A6, FUNCT_1:def 3;

            then

             A8: (p . v) in P;

            z in (p . v) by A4, A6, A7;

            hence thesis by A8;

          end;

          then

           A9: y is FinSequence of X by A2, FINSEQ_1:def 4;

          

           A10: ( len y) = ( len p) by A2, A3, A5, FINSEQ_1:def 3;

          ( len p) = n by CARD_1:def 7;

          then y is Element of nX by A9, A10, FINSEQ_2: 92;

          hence thesis;

        end;

        hence thesis;

      end;

      then

      reconsider PP as Subset-Family of nX;

      PP is a_partition of nX

      proof

        thus ( union PP) c= nX;

        thus nX c= ( union PP)

        proof

          let x be object;

          assume x in nX;

          then

          reconsider x as Element of nX;

          

           A11: ( rng x) c= X;

          ( union P) = X by EQREL_1:def 4;

          then

          consider p be Function such that

           A12: ( dom p) = ( dom x) and

           A13: ( rng p) c= P and

           A14: x in ( product p) by A11, Th5;

          

           A15: ( dom p) = ( Seg ( len x)) by A12, FINSEQ_1:def 3;

          then

          reconsider p as FinSequence by FINSEQ_1:def 2;

          reconsider p as FinSequence of P by A13, FINSEQ_1:def 4;

          

           A16: ( len p) = ( len x) by A15, FINSEQ_1:def 3;

          ( len x) = n by CARD_1:def 7;

          then

          reconsider p as Element of nP by A16, FINSEQ_2: 92;

          ( product p) in PP;

          hence thesis by A14, TARSKI:def 4;

        end;

        let A be Subset of nX;

        assume A in PP;

        then

        consider p be Element of nP such that

         A17: A = ( product p);

        thus A <> {} by A17;

        let B be Subset of nX;

        assume B in PP;

        then

        consider q be Element of nP such that

         A18: B = ( product q);

        assume

         A19: A <> B;

        assume A meets B;

        then

        consider x be object such that

         A20: x in A and

         A21: x in B by XBOOLE_0: 3;

        consider f be Function such that

         A22: x = f and

         A23: ( dom f) = ( dom p) and

         A24: for z be object st z in ( dom p) holds (f . z) in (p . z) by A17, A20, CARD_3:def 5;

        

         A25: ex g be Function st (x = g) & (( dom g) = ( dom q)) & (for z be object st z in ( dom q) holds (g . z) in (q . z)) by A18, A21, CARD_3:def 5;

        now

          let z be object;

          assume

           A26: z in ( dom p);

          then

           A27: (f . z) in (p . z) by A24;

          

           A28: (f . z) in (q . z) by A22, A23, A25, A26;

          

           A29: (p . z) in ( rng p) by A26, FUNCT_1:def 3;

          

           A30: (q . z) in ( rng q) by A22, A23, A25, A26, FUNCT_1:def 3;

          

           A31: (p . z) meets (q . z) by A27, A28, XBOOLE_0: 3;

          

           A32: (p . z) in P by A29;

          (q . z) in P by A30;

          hence (p . z) = (q . z) by A31, A32, EQREL_1:def 4;

        end;

        hence contradiction by A17, A18, A19, A22, A23, A25, FUNCT_1: 2;

      end;

      hence thesis;

    end;

    theorem :: PUA2MSS1:11

    

     Th10: for X be non empty set, Y be set st Y c= X holds for P be a_partition of X holds { (a /\ Y) where a be Element of P : a meets Y } is a_partition of Y

    proof

      let X be non empty set, Y be set;

      assume

       A1: Y c= X;

      let P be a_partition of X;

      set Q = { (a /\ Y) where a be Element of P : a meets Y };

      Q c= ( bool Y)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in Q;

        then ex p be Element of P st (x = (p /\ Y)) & (p meets Y);

        then

         A2: xx c= (X /\ Y) by XBOOLE_1: 26;

        (X /\ Y) = Y by A1, XBOOLE_1: 28;

        hence thesis by A2;

      end;

      then

      reconsider Q as Subset-Family of Y;

      Q is a_partition of Y

      proof

        thus ( union Q) c= Y;

        thus Y c= ( union Q)

        proof

          let x be object;

          assume

           A3: x in Y;

          X = ( union P) by EQREL_1:def 4;

          then

          consider p be set such that

           A4: x in p and

           A5: p in P by A1, A3, TARSKI:def 4;

          

           A6: p meets Y by A3, A4, XBOOLE_0: 3;

          

           A7: x in (p /\ Y) by A3, A4, XBOOLE_0:def 4;

          (p /\ Y) in Q by A5, A6;

          hence thesis by A7, TARSKI:def 4;

        end;

        let A be Subset of Y;

        assume A in Q;

        then

        consider p be Element of P such that

         A8: A = (p /\ Y) and

         A9: p meets Y;

        thus A <> {} by A8, A9;

        let B be Subset of Y;

        assume B in Q;

        then

        consider p1 be Element of P such that

         A10: B = (p1 /\ Y) and p1 meets Y;

        assume A <> B;

        then p misses p1 by A8, A10, EQREL_1:def 4;

        then A misses p1 by A8, XBOOLE_1: 74;

        hence thesis by A10, XBOOLE_1: 74;

      end;

      hence thesis;

    end;

    theorem :: PUA2MSS1:12

    

     Th11: for f be non empty Function, P be a_partition of ( dom f) holds the set of all (f | a) where a be Element of P is a_partition of f

    proof

      let f be non empty Function;

      set X = ( dom f);

      let P be a_partition of X;

      set Y = f;

      set Q = the set of all (f | a) where a be Element of P;

      Q c= ( bool Y)

      proof

        let x be object;

        reconsider xx = x as set by TARSKI: 1;

        assume x in Q;

        then ex p be Element of P st (x = (f | p));

        then xx c= f by RELAT_1: 59;

        hence thesis;

      end;

      then

      reconsider Q as Subset-Family of Y;

      Q is a_partition of Y

      proof

        Y c= ( union Q)

        proof

          let y,z be object;

          assume

           A1: [y, z] in f;

          then

           A2: y in X by XTUPLE_0:def 12;

          X = ( union P) by EQREL_1:def 4;

          then

          consider p be set such that

           A3: y in p and

           A4: p in P by A2, TARSKI:def 4;

          

           A5: [y, z] in (f | p) by A1, A3, RELAT_1:def 11;

          (f | p) in Q by A4;

          hence thesis by A5, TARSKI:def 4;

        end;

        hence Y = ( union Q);

        let A be Subset of Y;

        assume A in Q;

        then

        consider p be Element of P such that

         A6: A = (f | p);

        reconsider p as non empty Subset of X;

        thus A <> {} by A6;

        let B be Subset of Y;

        assume B in Q;

        then

        consider p1 be Element of P such that

         A7: B = (f | p1);

        assume A <> B;

        then

         A8: p misses p1 by A6, A7, EQREL_1:def 4;

        assume A meets B;

        then

        consider x be object such that

         A9: x in A and

         A10: x in B by XBOOLE_0: 3;

        consider y,z be object such that

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

        

         A12: y in p by A6, A9, A11, RELAT_1:def 11;

        y in p1 by A7, A10, A11, RELAT_1:def 11;

        hence contradiction by A8, A12, XBOOLE_0: 3;

      end;

      hence thesis;

    end;

    theorem :: PUA2MSS1:13

    

     Th12: for X be set, p be FinSequence of ( SmallestPartition X) holds ex q be FinSequence of X st ( product p) = {q}

    proof

      let X be set;

      set P = ( SmallestPartition X);

      let p be FinSequence of P;

      set q = the Element of ( product p);

      

       A1: ( dom q) = ( dom p) by CARD_3: 9;

      then

      reconsider q as FinSequence by Lm1;

      

       A2: q in ( product p);

      

       A3: ( product p) c= ( Funcs (( dom p),( Union p))) by FUNCT_6: 1;

      

       A4: ( Union p) = ( union ( rng p)) by CARD_3:def 4;

      

       A5: ex f be Function st q = f & ( dom f) = ( dom p) & ( rng f) c= ( Union p) by A2, A3, FUNCT_2:def 2;

      ( Union p) c= ( union P) by A4, ZFMISC_1: 77;

      then ( rng q) c= ( union P) by A5;

      then ( rng q) c= X by EQREL_1:def 4;

      then

      reconsider q as FinSequence of X by FINSEQ_1:def 4;

      take q;

      thus ( product p) c= {q}

      proof

        let x be object;

        assume x in ( product p);

        then

        consider g be Function such that

         A6: x = g and

         A7: ( dom g) = ( dom p) and

         A8: for x be object st x in ( dom p) holds (g . x) in (p . x) by CARD_3:def 5;

        now

          let y be object;

          assume

           A9: y in ( dom p);

          then

           A10: (g . y) in (p . y) by A8;

          

           A11: (q . y) in (p . y) by A9, CARD_3: 9;

          

           A12: (p . y) in ( rng p) by A9, FUNCT_1:def 3;

          then

           A13: (p . y) in P;

          reconsider X as non empty set by A12;

          P = the set of all {z} where z be Element of X by EQREL_1: 37;

          then

          consider z be Element of X such that

           A14: (p . y) = {z} by A13;

          

          thus (g . y) = z by A10, A14, TARSKI:def 1

          .= (q . y) by A11, A14, TARSKI:def 1;

        end;

        then x = q by A1, A6, A7, FUNCT_1: 2;

        hence thesis by TARSKI:def 1;

      end;

      thus thesis by ZFMISC_1: 31;

    end;

    definition

      let X be set;

      :: PUA2MSS1:def2

      mode IndexedPartition of X -> Function means

      : Def2: ( rng it ) is a_partition of X & it is one-to-one;

      existence

      proof

        set p = the a_partition of X;

        take ( id p);

        thus thesis;

      end;

    end

    definition

      let X be set;

      let P be IndexedPartition of X;

      :: original: rng

      redefine

      func rng P -> a_partition of X ;

      coherence by Def2;

    end

    registration

      let X be set;

      cluster -> one-to-one non-empty for IndexedPartition of X;

      coherence

      proof

        let P be IndexedPartition of X;

        thus P is one-to-one by Def2;

        let x be object;

        assume x in ( dom P);

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

        hence thesis;

      end;

    end

    registration

      let X be non empty set;

      cluster -> non empty for IndexedPartition of X;

      coherence

      proof

        let P be IndexedPartition of X;

        set a = the Element of ( rng P);

        ex b be object st [b, a] in P by XTUPLE_0:def 13;

        hence thesis;

      end;

    end

    definition

      let X be set, P be a_partition of X;

      :: original: id

      redefine

      func id P -> IndexedPartition of X ;

      coherence

      proof

        ( rng ( id P)) = P;

        hence thesis by Def2;

      end;

    end

    definition

      let X be set;

      let P be IndexedPartition of X;

      let x be object;

      assume

       A1: x in X;

      

       A2: ( union ( rng P)) = X by EQREL_1:def 4;

      :: PUA2MSS1:def3

      func P -index_of x -> set means

      : Def3: it in ( dom P) & x in (P . it );

      existence

      proof

        consider a be set such that

         A3: x in a and

         A4: a in ( rng P) by A1, A2, TARSKI:def 4;

        ex y be object st y in ( dom P) & a = (P . y) by A4, FUNCT_1:def 3;

        hence thesis by A3;

      end;

      correctness

      proof

        let y1,y2 be set;

        assume that

         A5: y1 in ( dom P) and

         A6: x in (P . y1) and

         A7: y2 in ( dom P) and

         A8: x in (P . y2);

        

         A9: (P . y1) in ( rng P) by A5, FUNCT_1:def 3;

        

         A10: (P . y2) in ( rng P) by A7, FUNCT_1:def 3;

        (P . y1) meets (P . y2) by A6, A8, XBOOLE_0: 3;

        then (P . y1) = (P . y2) by A9, A10, EQREL_1:def 4;

        hence thesis by A5, A7, FUNCT_1:def 4;

      end;

    end

    theorem :: PUA2MSS1:14

    

     Th13: for X be set, P be non-empty Function st ( Union P) = X & for x,y be set st x in ( dom P) & y in ( dom P) & x <> y holds (P . x) misses (P . y) holds P is IndexedPartition of X

    proof

      let X be set, P be non-empty Function such that

       A1: ( Union P) = X and

       A2: for x,y be set st x in ( dom P) & y in ( dom P) & x <> y holds (P . x) misses (P . y);

      ( rng P) c= ( bool X)

      proof

        let y be object;

        reconsider yy = y as set by TARSKI: 1;

        assume y in ( rng P);

        then yy c= ( union ( rng P)) by ZFMISC_1: 74;

        then yy c= X by A1, CARD_3:def 4;

        hence thesis;

      end;

      then

      reconsider Y = ( rng P) as Subset-Family of X;

      Y is a_partition of X

      proof

        thus ( union Y) = X by A1, CARD_3:def 4;

        let A be Subset of X;

        assume

         A3: A in Y;

        then

         A4: ex x be object st x in ( dom P) & A = (P . x) by FUNCT_1:def 3;

        thus A <> {} by A3;

        let B be Subset of X;

        assume B in Y;

        then ex y be object st y in ( dom P) & B = (P . y) by FUNCT_1:def 3;

        hence thesis by A2, A4;

      end;

      hence ( rng P) is a_partition of X;

      let x,y be object;

      assume that

       A5: x in ( dom P) and

       A6: y in ( dom P) and

       A7: (P . x) = (P . y) and

       A8: x <> y;

      reconsider Px = (P . x), Py = (P . y) as non empty set by A5, A6, FUNCT_1:def 9;

      set a = the Element of Px;

      (P . x) misses (P . y) by A2, A5, A6, A8;

      then not a in Py by XBOOLE_0: 3;

      hence contradiction by A7;

    end;

    theorem :: PUA2MSS1:15

    

     Th14: for X,Y be non empty set, P be a_partition of Y holds for f be Function of X, P st P c= ( rng f) & f is one-to-one holds f is IndexedPartition of Y

    proof

      let X,Y be non empty set, P be a_partition of Y;

      let f be Function of X, P;

      assume P c= ( rng f);

      then ( rng f) = P;

      hence thesis by Def2;

    end;

    begin

    scheme :: PUA2MSS1:sch1

    IndRelationEx { A,B() -> non empty set , i() -> Nat , R0() -> Relation of A(), B() , RR( set, set) -> Relation of A(), B() } :

ex R be Relation of A(), B(), F be ManySortedSet of NAT st R = (F . i()) & (F . 0 ) = R0() & for i be Nat, R be Relation of A(), B() st R = (F . i) holds (F . (i + 1)) = RR(R,i);

      deffunc G( set, set) = RR($2,$1);

      consider F be Function such that

       A1: ( dom F) = NAT and

       A2: (F . 0 ) = R0() & for n be Nat holds (F . (n + 1)) = G(n,.) from NAT_1:sch 11;

      reconsider F as ManySortedSet of NAT by A1, PARTFUN1:def 2, RELAT_1:def 18;

      defpred P[ Nat] means (F . $1) is Relation of A(), B();

      

       A3: P[ 0 ] by A2;

       A4:

      now

        let i be Nat;

        assume P[i];

        then

        reconsider R = (F . i) as Relation of A(), B();

        (F . (i + 1)) = RR(R,i) by A2;

        hence P[(i + 1)];

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A3, A4);

      then

      reconsider R = (F . i()) as Relation of A(), B();

      take R, F;

      thus thesis by A2;

    end;

    scheme :: PUA2MSS1:sch2

    RelationUniq { A,B() -> non empty set , P[ set, set] } :

for R1,R2 be Relation of A(), B() st (for x be Element of A(), y be Element of B() holds [x, y] in R1 iff P[x, y]) & (for x be Element of A(), y be Element of B() holds [x, y] in R2 iff P[x, y]) holds R1 = R2;

      let R1,R2 be Relation of A(), B() such that

       A1: for x be Element of A(), y be Element of B() holds [x, y] in R1 iff P[x, y] and

       A2: for x be Element of A(), y be Element of B() holds [x, y] in R2 iff P[x, y];

      let x,y be object;

      hereby

        assume

         A3: [x, y] in R1;

        then

        reconsider a = x as Element of A() by ZFMISC_1: 87;

        reconsider b = y as Element of B() by A3, ZFMISC_1: 87;

        P[a, b] by A1, A3;

        hence [x, y] in R2 by A2;

      end;

      assume

       A4: [x, y] in R2;

      then

      reconsider a = x as Element of A() by ZFMISC_1: 87;

      reconsider b = y as Element of B() by A4, ZFMISC_1: 87;

      P[a, b] by A2, A4;

      hence thesis by A1;

    end;

    scheme :: PUA2MSS1:sch3

    IndRelationUniq { A,B() -> non empty set , i() -> Nat , R0() -> Relation of A(), B() , RR( set, set) -> Relation of A(), B() } :

for R1,R2 be Relation of A(), B() st (ex F be ManySortedSet of NAT st R1 = (F . i()) & (F . 0 ) = R0() & for i be Nat, R be Relation of A(), B() st R = (F . i) holds (F . (i + 1)) = RR(R,i)) & (ex F be ManySortedSet of NAT st R2 = (F . i()) & (F . 0 ) = R0() & for i be Nat, R be Relation of A(), B() st R = (F . i) holds (F . (i + 1)) = RR(R,i)) holds R1 = R2;

      let R1,R2 be Relation of A(), B();

      given F1 be ManySortedSet of NAT such that

       A1: R1 = (F1 . i()) and

       A2: (F1 . 0 ) = R0() and

       A3: for i be Nat, R be Relation of A(), B() st R = (F1 . i) holds (F1 . (i + 1)) = RR(R,i);

      given F2 be ManySortedSet of NAT such that

       A4: R2 = (F2 . i()) and

       A5: (F2 . 0 ) = R0() and

       A6: for i be Nat, R be Relation of A(), B() st R = (F2 . i) holds (F2 . (i + 1)) = RR(R,i);

      defpred P[ Nat] means (F1 . $1) = (F2 . $1) & (F1 . $1) is Relation of A(), B();

      

       A7: P[ 0 ] by A2, A5;

       A8:

      now

        let i be Nat;

        assume

         A9: P[i];

        then

        reconsider R = (F1 . i) as Relation of A(), B();

        (F1 . (i + 1)) = RR(R,i) by A3;

        hence P[(i + 1)] by A6, A9;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A7, A8);

      hence thesis by A1, A4;

    end;

    definition

      let A be partial non-empty UAStr;

      :: PUA2MSS1:def4

      func DomRel A -> Relation of the carrier of A means

      : Def4: for x,y be Element of A holds [x, y] in it iff for f be operation of A, p,q be FinSequence holds ((p ^ <*x*>) ^ q) in ( dom f) iff ((p ^ <*y*>) ^ q) in ( dom f);

      existence

      proof

        defpred P[ set, set] means for f be operation of A, p,q be FinSequence holds ((p ^ <*$1*>) ^ q) in ( dom f) iff ((p ^ <*$2*>) ^ q) in ( dom f);

        thus ex D be Relation of the carrier of A st for x,y be Element of A holds [x, y] in D iff P[x, y] from RELSET_1:sch 2;

      end;

      uniqueness

      proof

        defpred P[ set, set] means for f be operation of A, p,q be FinSequence holds ((p ^ <*$1*>) ^ q) in ( dom f) iff ((p ^ <*$2*>) ^ q) in ( dom f);

        thus for D1,D2 be Relation of the carrier of A st (for x,y be Element of A holds [x, y] in D1 iff P[x, y]) & (for x,y be Element of A holds [x, y] in D2 iff P[x, y]) holds D1 = D2 from RelationUniq;

      end;

    end

    registration

      let A be partial non-empty UAStr;

      cluster ( DomRel A) -> total symmetric transitive;

      coherence

      proof

        set X = the carrier of A;

        

         A1: ( DomRel A) is_reflexive_in X

        proof

          let x be object;

          for f be operation of A holds for a,b be FinSequence holds ((a ^ <*x*>) ^ b) in ( dom f) iff ((a ^ <*x*>) ^ b) in ( dom f);

          hence thesis by Def4;

        end;

        then

         A2: ( dom ( DomRel A)) = X by ORDERS_1: 13;

        

         A3: ( field ( DomRel A)) = X by A1, ORDERS_1: 13;

        thus ( DomRel A) is total by A2, PARTFUN1:def 2;

        ( DomRel A) is_symmetric_in X

        proof

          let x,y be object;

          assume that

           A4: x in X and

           A5: y in X;

          reconsider x9 = x, y9 = y as Element of X by A4, A5;

          assume [x, y] in ( DomRel A);

          then for f be operation of A holds for a,b be FinSequence holds ((a ^ <*x9*>) ^ b) in ( dom f) iff ((a ^ <*y9*>) ^ b) in ( dom f) by Def4;

          hence thesis by Def4;

        end;

        hence ( DomRel A) is symmetric by A3;

        ( DomRel A) is_transitive_in X

        proof

          let x,y,z be object;

          assume that

           A6: x in X and

           A7: y in X and

           A8: z in X;

          reconsider x9 = x, y9 = y, z9 = z as Element of X by A6, A7, A8;

          assume that

           A9: [x, y] in ( DomRel A) and

           A10: [y, z] in ( DomRel A);

          now

            let f be operation of A, a,b be FinSequence;

            ((a ^ <*x9*>) ^ b) in ( dom f) iff ((a ^ <*y9*>) ^ b) in ( dom f) by A9, Def4;

            hence ((a ^ <*x9*>) ^ b) in ( dom f) iff ((a ^ <*z9*>) ^ b) in ( dom f) by A10, Def4;

          end;

          hence thesis by Def4;

        end;

        hence thesis by A3;

      end;

    end

    definition

      let A be non-empty partial UAStr;

      let R be Relation of the carrier of A;

      :: PUA2MSS1:def5

      func R |^ A -> Relation of the carrier of A means

      : Def5: for x,y be Element of A holds [x, y] in it iff [x, y] in R & for f be operation of A holds for p,q be FinSequence st ((p ^ <*x*>) ^ q) in ( dom f) & ((p ^ <*y*>) ^ q) in ( dom f) holds [(f . ((p ^ <*x*>) ^ q)), (f . ((p ^ <*y*>) ^ q))] in R;

      existence

      proof

        defpred P[ set, set] means [$1, $2] in R & for f be operation of A holds for p,q be FinSequence st ((p ^ <*$1*>) ^ q) in ( dom f) & ((p ^ <*$2*>) ^ q) in ( dom f) holds [(f . ((p ^ <*$1*>) ^ q)), (f . ((p ^ <*$2*>) ^ q))] in R;

        thus ex D be Relation of the carrier of A st for x,y be Element of A holds [x, y] in D iff P[x, y] from RELSET_1:sch 2;

      end;

      uniqueness

      proof

        defpred P[ set, set] means [$1, $2] in R & for f be operation of A holds for p,q be FinSequence st ((p ^ <*$1*>) ^ q) in ( dom f) & ((p ^ <*$2*>) ^ q) in ( dom f) holds [(f . ((p ^ <*$1*>) ^ q)), (f . ((p ^ <*$2*>) ^ q))] in R;

        thus for D1,D2 be Relation of the carrier of A st (for x,y be Element of A holds [x, y] in D1 iff P[x, y]) & (for x,y be Element of A holds [x, y] in D2 iff P[x, y]) holds D1 = D2 from RelationUniq;

      end;

    end

    definition

      let A be non-empty partial UAStr;

      let R be Relation of the carrier of A;

      let i be Nat;

      :: PUA2MSS1:def6

      func R |^ (A,i) -> Relation of the carrier of A means

      : Def6: ex F be ManySortedSet of NAT st it = (F . i) & (F . 0 ) = R & for i be Nat, R be Relation of the carrier of A st R = (F . i) holds (F . (i + 1)) = (R |^ A);

      existence

      proof

        deffunc RR( Relation of the carrier of A, the carrier of A, Nat) = ($1 |^ A);

        thus ex D be Relation of the carrier of A st ex F be ManySortedSet of NAT st D = (F . i) & (F . 0 ) = R & for i be Nat, R be Relation of the carrier of A st R = (F . i) holds (F . (i + 1)) = RR(R,i) from IndRelationEx;

      end;

      uniqueness

      proof

        deffunc RR( Relation of the carrier of A, the carrier of A, Nat) = ($1 |^ A);

        thus for D1,D2 be Relation of the carrier of A st (ex F be ManySortedSet of NAT st D1 = (F . i) & (F . 0 ) = R & for i be Nat, R be Relation of the carrier of A st R = (F . i) holds (F . (i + 1)) = RR(R,i)) & (ex F be ManySortedSet of NAT st D2 = (F . i) & (F . 0 ) = R & for i be Nat, R be Relation of the carrier of A st R = (F . i) holds (F . (i + 1)) = RR(R,i)) holds D1 = D2 from IndRelationUniq;

      end;

    end

    theorem :: PUA2MSS1:16

    

     Th15: for A be non-empty partial UAStr, R be Relation of the carrier of A holds (R |^ (A, 0 )) = R & (R |^ (A,1)) = (R |^ A)

    proof

      let A be non-empty partial UAStr;

      let R be Relation of the carrier of A;

      consider F be ManySortedSet of NAT such that (R |^ (A, 0 )) = (F . 0 ) and

       A1: (F . 0 ) = R and

       A2: for i be Nat, R be Relation of the carrier of A st R = (F . i) holds (F . (i + 1)) = (R |^ A) by Def6;

      (F . ( 0 + 1)) = (R |^ A) by A1, A2;

      hence thesis by A1, A2, Def6;

    end;

    theorem :: PUA2MSS1:17

    

     Th16: for A be non-empty partial UAStr, i be Nat, R be Relation of the carrier of A holds (R |^ (A,(i + 1))) = ((R |^ (A,i)) |^ A)

    proof

      let A be non-empty partial UAStr;

      let i be Nat;

      let R be Relation of the carrier of A;

      consider F be ManySortedSet of NAT such that

       A1: (R |^ (A,i)) = (F . i) and

       A2: (F . 0 ) = R and

       A3: for i be Nat, R be Relation of the carrier of A st R = (F . i) holds (F . (i + 1)) = (R |^ A) by Def6;

      (F . (i + 1)) = ((R |^ (A,i)) |^ A) by A1, A3;

      hence thesis by A2, A3, Def6;

    end;

    theorem :: PUA2MSS1:18

    for A be non-empty partial UAStr, i,j be Element of NAT , R be Relation of the carrier of A holds (R |^ (A,(i + j))) = ((R |^ (A,i)) |^ (A,j))

    proof

      let A be non-empty partial UAStr;

      let i,j be Element of NAT ;

      let R be Relation of the carrier of A;

      defpred P[ Nat] means (R |^ (A,(i + $1))) = ((R |^ (A,i)) |^ (A,$1));

      

       A1: P[ 0 ] by Th15;

       A2:

      now

        let j be Nat;

        assume

         A3: P[j];

        (R |^ (A,(i + (j + 1)))) = (R |^ (A,((i + j) + 1)))

        .= ((R |^ (A,(i + j))) |^ A) by Th16

        .= ((R |^ (A,i)) |^ (A,(j + 1))) by A3, Th16;

        hence P[(j + 1)];

      end;

      for j be Nat holds P[j] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: PUA2MSS1:19

    

     Th18: for A be non-empty partial UAStr holds for R be Equivalence_Relation of the carrier of A st R c= ( DomRel A) holds (R |^ A) is total symmetric transitive

    proof

      let A be non-empty partial UAStr;

      let R be Equivalence_Relation of the carrier of A;

      assume

       A1: R c= ( DomRel A);

      now

        let x be object;

        assume x in the carrier of A;

        then

        reconsider a = x as Element of A;

        

         A2: [a, a] in R by EQREL_1: 5;

        now

          let f be operation of A, p,q be FinSequence;

          assume that

           A3: ((p ^ <*a*>) ^ q) in ( dom f) and ((p ^ <*a*>) ^ q) in ( dom f);

          (f . ((p ^ <*a*>) ^ q)) in ( rng f) by A3, FUNCT_1:def 3;

          hence [(f . ((p ^ <*a*>) ^ q)), (f . ((p ^ <*a*>) ^ q))] in R by EQREL_1: 5;

        end;

        hence [x, x] in (R |^ A) by A2, Def5;

      end;

      then

       A4: (R |^ A) is_reflexive_in the carrier of A;

      then

       A5: ( dom (R |^ A)) = the carrier of A by ORDERS_1: 13;

      

       A6: ( field (R |^ A)) = the carrier of A by A4, ORDERS_1: 13;

      thus (R |^ A) is total by A5, PARTFUN1:def 2;

      now

        let x,y be object;

        assume that

         A7: x in the carrier of A and

         A8: y in the carrier of A;

        reconsider a = x, b = y as Element of A by A7, A8;

        assume

         A9: [x, y] in (R |^ A);

        then

         A10: [a, b] in R by Def5;

        now

          thus [b, a] in R by A10, EQREL_1: 6;

          let f be operation of A;

          let p,q be FinSequence;

          assume that

           A11: ((p ^ <*b*>) ^ q) in ( dom f) and

           A12: ((p ^ <*a*>) ^ q) in ( dom f);

           [(f . ((p ^ <*a*>) ^ q)), (f . ((p ^ <*b*>) ^ q))] in R by A9, A11, A12, Def5;

          hence [(f . ((p ^ <*b*>) ^ q)), (f . ((p ^ <*a*>) ^ q))] in R by EQREL_1: 6;

        end;

        hence [y, x] in (R |^ A) by Def5;

      end;

      then (R |^ A) is_symmetric_in the carrier of A;

      hence (R |^ A) is symmetric by A6;

      now

        let x,y,z be object;

        assume that

         A13: x in the carrier of A and

         A14: y in the carrier of A and

         A15: z in the carrier of A;

        reconsider a = x, b = y, c = z as Element of A by A13, A14, A15;

        assume that

         A16: [x, y] in (R |^ A) and

         A17: [y, z] in (R |^ A);

         A18:

        now

          let f be operation of A;

          let p,q be FinSequence;

          

           A19: [a, b] in R by A16, Def5;

          

           A20: ((p ^ <*a*>) ^ q) in ( dom f) & ((p ^ <*b*>) ^ q) in ( dom f) implies [(f . ((p ^ <*a*>) ^ q)), (f . ((p ^ <*b*>) ^ q))] in R by A16, Def5;

          ((p ^ <*b*>) ^ q) in ( dom f) & ((p ^ <*c*>) ^ q) in ( dom f) implies [(f . ((p ^ <*b*>) ^ q)), (f . ((p ^ <*c*>) ^ q))] in R by A17, Def5;

          hence ((p ^ <*a*>) ^ q) in ( dom f) & ((p ^ <*c*>) ^ q) in ( dom f) implies [(f . ((p ^ <*a*>) ^ q)), (f . ((p ^ <*c*>) ^ q))] in R by A1, A19, A20, Def4, EQREL_1: 7;

        end;

        

         A21: [a, b] in R by A16, Def5;

         [b, c] in R by A17, Def5;

        then [a, c] in R by A21, EQREL_1: 7;

        hence [x, z] in (R |^ A) by A18, Def5;

      end;

      then (R |^ A) is_transitive_in the carrier of A;

      hence thesis by A6;

    end;

    theorem :: PUA2MSS1:20

    

     Th19: for A be non-empty partial UAStr holds for R be Relation of the carrier of A holds (R |^ A) c= R

    proof

      let A be non-empty partial UAStr;

      let R be Relation of the carrier of A;

      let x,y be object;

      assume

       A1: [x, y] in (R |^ A);

      then

       A2: x in the carrier of A by ZFMISC_1: 87;

      y in the carrier of A by A1, ZFMISC_1: 87;

      hence thesis by A1, A2, Def5;

    end;

    theorem :: PUA2MSS1:21

    

     Th20: for A be non-empty partial UAStr holds for R be Equivalence_Relation of the carrier of A st R c= ( DomRel A) holds for i be Element of NAT holds (R |^ (A,i)) is total symmetric transitive

    proof

      let A be non-empty partial UAStr;

      let R be Equivalence_Relation of the carrier of A such that

       A1: R c= ( DomRel A);

      defpred P[ Nat] means (R |^ (A,$1)) c= ( DomRel A) & (R |^ (A,$1)) is total symmetric transitive;

      

       A2: P[ 0 ] by A1, Th15;

       A3:

      now

        let i be Nat;

        assume

         A4: P[i];

        

         A5: ((R |^ (A,i)) |^ A) c= (R |^ (A,i)) by Th19;

        ((R |^ (A,i)) |^ A) = (R |^ (A,(i + 1))) by Th16;

        hence P[(i + 1)] by A4, A5, Th18, XBOOLE_1: 1;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    definition

      let A be non-empty partial UAStr;

      defpred P[ set, set] means for i be Element of NAT holds [$1, $2] in (( DomRel A) |^ (A,i));

      :: PUA2MSS1:def7

      func LimDomRel A -> Relation of the carrier of A means

      : Def7: for x,y be Element of A holds [x, y] in it iff for i be Element of NAT holds [x, y] in (( DomRel A) |^ (A,i));

      existence

      proof

        thus ex D be Relation of the carrier of A st for x,y be Element of A holds [x, y] in D iff P[x, y] from RELSET_1:sch 2;

      end;

      uniqueness

      proof

        thus for D1,D2 be Relation of the carrier of A st (for x,y be Element of A holds [x, y] in D1 iff P[x, y]) & (for x,y be Element of A holds [x, y] in D2 iff P[x, y]) holds D1 = D2 from RelationUniq;

      end;

    end

    theorem :: PUA2MSS1:22

    

     Th21: for A be non-empty partial UAStr holds ( LimDomRel A) c= ( DomRel A)

    proof

      let A be non-empty partial UAStr, x,y be object;

      assume

       A1: [x, y] in ( LimDomRel A);

      then

       A2: x in the carrier of A by ZFMISC_1: 87;

      y in the carrier of A by A1, ZFMISC_1: 87;

      then [x, y] in (( DomRel A) |^ (A, 0 )) by A1, A2, Def7;

      hence thesis by Th15;

    end;

    registration

      let A be non-empty partial UAStr;

      cluster ( LimDomRel A) -> total symmetric transitive;

      coherence

      proof

        now

          let x be object;

          assume x in the carrier of A;

          then

          reconsider a = x as Element of A;

          now

            let i be Element of NAT ;

            (( DomRel A) |^ (A,i)) is total symmetric transitive by Th20;

            hence [a, a] in (( DomRel A) |^ (A,i)) by EQREL_1: 5;

          end;

          hence [x, x] in ( LimDomRel A) by Def7;

        end;

        then

         A1: ( LimDomRel A) is_reflexive_in the carrier of A;

        then

         A2: ( dom ( LimDomRel A)) = the carrier of A by ORDERS_1: 13;

        

         A3: ( field ( LimDomRel A)) = the carrier of A by A1, ORDERS_1: 13;

        thus ( LimDomRel A) is total by A2, PARTFUN1:def 2;

        now

          let x,y be object;

          assume that

           A4: x in the carrier of A and

           A5: y in the carrier of A;

          reconsider a = x, b = y as Element of A by A4, A5;

          assume

           A6: [x, y] in ( LimDomRel A);

          now

            let i be Element of NAT ;

            

             A7: (( DomRel A) |^ (A,i)) is total symmetric transitive by Th20;

             [a, b] in (( DomRel A) |^ (A,i)) by A6, Def7;

            hence [b, a] in (( DomRel A) |^ (A,i)) by A7, EQREL_1: 6;

          end;

          hence [y, x] in ( LimDomRel A) by Def7;

        end;

        then ( LimDomRel A) is_symmetric_in the carrier of A;

        hence ( LimDomRel A) is symmetric by A3;

        now

          let x,y,z be object;

          assume that

           A8: x in the carrier of A and

           A9: y in the carrier of A and

           A10: z in the carrier of A;

          reconsider a = x, b = y, c = z as Element of A by A8, A9, A10;

          assume that

           A11: [x, y] in ( LimDomRel A) and

           A12: [y, z] in ( LimDomRel A);

          now

            let i be Element of NAT ;

            

             A13: (( DomRel A) |^ (A,i)) is total symmetric transitive by Th20;

            

             A14: [a, b] in (( DomRel A) |^ (A,i)) by A11, Def7;

             [b, c] in (( DomRel A) |^ (A,i)) by A12, Def7;

            hence [a, c] in (( DomRel A) |^ (A,i)) by A13, A14, EQREL_1: 7;

          end;

          hence [x, z] in ( LimDomRel A) by Def7;

        end;

        then ( LimDomRel A) is_transitive_in the carrier of A;

        hence thesis by A3;

      end;

    end

    begin

    definition

      let X be non empty set;

      let f be PartFunc of (X * ), X;

      let P be a_partition of X;

      :: PUA2MSS1:def8

      pred f is_partitable_wrt P means for p be FinSequence of P holds ex a be Element of P st (f .: ( product p)) c= a;

    end

    definition

      let X be non empty set;

      let f be PartFunc of (X * ), X;

      let P be a_partition of X;

      :: PUA2MSS1:def9

      pred f is_exactly_partitable_wrt P means f is_partitable_wrt P & for p be FinSequence of P st ( product p) meets ( dom f) holds ( product p) c= ( dom f);

    end

    theorem :: PUA2MSS1:23

    for A be non-empty partial UAStr holds for f be operation of A holds f is_exactly_partitable_wrt ( SmallestPartition the carrier of A)

    proof

      let A be non-empty partial UAStr;

      set P = ( SmallestPartition the carrier of A);

      let f be operation of A;

      hereby

        let p be FinSequence of P;

        consider q be FinSequence of the carrier of A such that

         A1: ( product p) = {q} by Th12;

        q in ( dom f) & (f . q) in ( rng f) & ( rng f) c= the carrier of A or not q in ( dom f) by FUNCT_1:def 3;

        then

        consider x be Element of A such that

         A2: q in ( dom f) & x = (f . q) or not q in ( dom f);

        P = the set of all {z} where z be Element of A by EQREL_1: 37;

        then {x} in P;

        then

        reconsider a = {x} as Element of P;

        take a;

        thus (f .: ( product p)) c= a

        proof

          let z be object;

          assume z in (f .: ( product p));

          then

          consider y be object such that

           A3: y in ( dom f) and

           A4: y in ( product p) and

           A5: z = (f . y) by FUNCT_1:def 6;

          y = q by A1, A4, TARSKI:def 1;

          hence thesis by A2, A3, A5, TARSKI:def 1;

        end;

      end;

      let p be FinSequence of P;

      consider q be FinSequence of the carrier of A such that

       A6: ( product p) = {q} by Th12;

      assume ( product p) meets ( dom f);

      then

       A7: ex x be object st x in ( product p) & x in ( dom f) by XBOOLE_0: 3;

      let z be object;

      assume z in ( product p);

      then z = q by A6, TARSKI:def 1;

      hence thesis by A6, A7, TARSKI:def 1;

    end;

    scheme :: PUA2MSS1:sch4

    FiniteTransitivity { x,y() -> FinSequence , P[ set], R[ set, set] } :

P[y()]

      provided

       A1: P[x()]

       and

       A2: ( len x()) = ( len y())

       and

       A3: for p,q be FinSequence, z1,z2 be set st P[((p ^ <*z1*>) ^ q)] & R[z1, z2] holds P[((p ^ <*z2*>) ^ q)]

       and

       A4: for i be Element of NAT st i in ( dom x()) holds R[(x() . i), (y() . i)];

      defpred Q[ Nat] means for x1,x2,y1,y2 be FinSequence st ( len x1) = $1 & x() = (x1 ^ x2) & ( len y1) = $1 & y() = (y1 ^ y2) holds P[(y1 ^ x2)];

      

       A5: Q[ 0 ]

      proof

        let x1,x2,y1,y2 be FinSequence;

        assume that

         A6: ( len x1) = 0 and

         A7: x() = (x1 ^ x2) and

         A8: ( len y1) = 0 and y() = (y1 ^ y2);

        

         A9: x1 = {} by A6;

        y1 = {} by A8;

        hence thesis by A1, A7, A9;

      end;

      

       A10: for i be Nat st Q[i] holds Q[(i + 1)]

      proof

        let i be Nat such that

         A11: for x1,x2,y1,y2 be FinSequence st ( len x1) = i & x() = (x1 ^ x2) & ( len y1) = i & y() = (y1 ^ y2) holds P[(y1 ^ x2)];

        let x1,x2,y1,y2 be FinSequence such that

         A12: ( len x1) = (i + 1) and

         A13: x() = (x1 ^ x2) and

         A14: ( len y1) = (i + 1) and

         A15: y() = (y1 ^ y2);

        

         A16: x1 <> {} by A12;

        

         A17: y1 <> {} by A14;

        consider x9 be FinSequence, xx be object such that

         A18: x1 = (x9 ^ <*xx*>) by A16, FINSEQ_1: 46;

        consider y9 be FinSequence, yy be object such that

         A19: y1 = (y9 ^ <*yy*>) by A17, FINSEQ_1: 46;

        

         A20: ( dom x1) = ( Seg ( len x1)) by FINSEQ_1:def 3;

        

         A21: ( dom y1) = ( Seg ( len y1)) by FINSEQ_1:def 3;

        

         A22: ( len <*xx*>) = 1 by FINSEQ_1: 40;

        

         A23: ( len <*yy*>) = 1 by FINSEQ_1: 40;

        

         A24: ( len x1) = (( len x9) + 1) by A18, A22, FINSEQ_1: 22;

        

         A25: ( len y1) = (( len y9) + 1) by A19, A23, FINSEQ_1: 22;

        

         A26: x() = (x9 ^ ( <*xx*> ^ x2)) by A13, A18, FINSEQ_1: 32;

        

         A27: y() = (y9 ^ ( <*yy*> ^ y2)) by A15, A19, FINSEQ_1: 32;

        

         A28: (i + 1) in ( dom x1) by A12, A20, FINSEQ_1: 4;

        

         A29: ( dom x1) c= ( dom x()) by A13, FINSEQ_1: 26;

        

         A30: (x1 . (( len x9) + 1)) = xx by A18, FINSEQ_1: 42;

        

         A31: (y1 . (( len y9) + 1)) = yy by A19, FINSEQ_1: 42;

        

         A32: P[(y9 ^ ( <*xx*> ^ x2))] by A11, A12, A14, A24, A25, A26, A27;

        

         A33: (x() . (i + 1)) = xx by A12, A13, A24, A28, A30, FINSEQ_1:def 7;

        

         A34: (y() . (i + 1)) = yy by A12, A14, A15, A20, A21, A25, A28, A31, FINSEQ_1:def 7;

        P[((y9 ^ <*xx*>) ^ x2)] by A32, FINSEQ_1: 32;

        hence thesis by A3, A4, A19, A28, A29, A33, A34;

      end;

      

       A35: for i be Nat holds Q[i] from NAT_1:sch 2( A5, A10);

      

       A36: x() = (x() ^ {} ) by FINSEQ_1: 34;

      y() = (y() ^ {} ) by FINSEQ_1: 34;

      hence thesis by A2, A35, A36;

    end;

    theorem :: PUA2MSS1:24

    

     Th23: for A be non-empty partial UAStr holds for f be operation of A holds f is_exactly_partitable_wrt ( Class ( LimDomRel A))

    proof

      let A be non-empty partial UAStr;

      set P = ( Class ( LimDomRel A));

      let f be operation of A;

      hereby

        let p be FinSequence of P;

        set a0 = the Element of P;

        per cases ;

          suppose ( product p) meets ( dom f);

          then

          consider x be object such that

           A1: x in ( product p) and

           A2: x in ( dom f) by XBOOLE_0: 3;

          (f . x) in the carrier of A by A2, PARTFUN1: 4;

          then

          reconsider a = ( Class (( LimDomRel A),(f . x))) as Element of P by EQREL_1:def 3;

          take a;

          thus (f .: ( product p)) c= a

          proof

            let y be object;

            assume y in (f .: ( product p));

            then

            consider z be object such that z in ( dom f) and

             A3: z in ( product p) and

             A4: y = (f . z) by FUNCT_1:def 6;

            

             A5: ( product p) c= ( Funcs (( dom p),( Union p))) by FUNCT_6: 1;

            then

             A6: ex f be Function st x = f & ( dom f) = ( dom p) & ( rng f) c= ( Union p) by A1, FUNCT_2:def 2;

            

             A7: ex f be Function st z = f & ( dom f) = ( dom p) & ( rng f) c= ( Union p) by A3, A5, FUNCT_2:def 2;

            reconsider x, z as Function by A1, A3;

            

             A8: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

            then

            reconsider x, z as FinSequence by A6, A7, FINSEQ_1:def 2;

            defpred P[ set] means $1 in ( dom f) & (f . $1) in a;

            defpred R[ set, set] means [$1, $2] in ( LimDomRel A);

            ( len x) = ( len p) by A6, A8, FINSEQ_1:def 3;

            then

             A9: ( len x) = ( len z) by A7, A8, FINSEQ_1:def 3;

            

             A10: P[x] by A2, EQREL_1: 20, PARTFUN1: 4;

            

             A11: for p1,q1 be FinSequence, z1,z2 be set st P[((p1 ^ <*z1*>) ^ q1)] & R[z1, z2] holds P[((p1 ^ <*z2*>) ^ q1)]

            proof

              let p1,q1 be FinSequence, z1,z2 be set;

              assume that

               A12: ((p1 ^ <*z1*>) ^ q1) in ( dom f) and

               A13: (f . ((p1 ^ <*z1*>) ^ q1)) in a and

               A14: [z1, z2] in ( LimDomRel A);

              

               A15: [(f . ((p1 ^ <*z1*>) ^ q1)), (f . x)] in ( LimDomRel A) by A13, EQREL_1: 19;

              

               A16: ( LimDomRel A) c= ( DomRel A) by Th21;

              

               A17: z1 in the carrier of A by A14, ZFMISC_1: 87;

              

               A18: z2 in the carrier of A by A14, ZFMISC_1: 87;

              hence

               A19: ((p1 ^ <*z2*>) ^ q1) in ( dom f) by A12, A14, A16, A17, Def4;

              

               A20: (f . ((p1 ^ <*z1*>) ^ q1)) in ( rng f) by A12, FUNCT_1:def 3;

              

               A21: (f . ((p1 ^ <*z2*>) ^ q1)) in ( rng f) by A19, FUNCT_1:def 3;

              now

                let i be Element of NAT ;

                 [z1, z2] in (( DomRel A) |^ (A,(i + 1))) by A14, A17, A18, Def7;

                then [z1, z2] in ((( DomRel A) |^ (A,i)) |^ A) by Th16;

                then

                 A22: [(f . ((p1 ^ <*z1*>) ^ q1)), (f . ((p1 ^ <*z2*>) ^ q1))] in (( DomRel A) |^ (A,i)) by A12, A17, A18, A19, Def5;

                (( DomRel A) |^ (A,i)) is total symmetric transitive by Th20;

                hence [(f . ((p1 ^ <*z2*>) ^ q1)), (f . ((p1 ^ <*z1*>) ^ q1))] in (( DomRel A) |^ (A,i)) by A22, EQREL_1: 6;

              end;

              then [(f . ((p1 ^ <*z2*>) ^ q1)), (f . ((p1 ^ <*z1*>) ^ q1))] in ( LimDomRel A) by A20, A21, Def7;

              then [(f . ((p1 ^ <*z2*>) ^ q1)), (f . x)] in ( LimDomRel A) by A15, EQREL_1: 7;

              hence thesis by EQREL_1: 19;

            end;

            

             A23: for i be Element of NAT st i in ( dom x) holds R[(x . i), (z . i)]

            proof

              let i be Element of NAT ;

              assume

               A24: i in ( dom x);

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

              then

              reconsider a = (p . i) as Element of P;

              

               A25: ex g be Function st x = g & ( dom g) = ( dom p) & for x be object st x in ( dom p) holds (g . x) in (p . x) by A1, CARD_3:def 5;

              

               A26: ex g be Function st z = g & ( dom g) = ( dom p) & for x be object st x in ( dom p) holds (g . x) in (p . x) by A3, CARD_3:def 5;

              

               A27: ex b be object st b in the carrier of A & a = ( Class (( LimDomRel A),b)) by EQREL_1:def 3;

              

               A28: (x . i) in a by A24, A25;

              (z . i) in a by A24, A25, A26;

              hence thesis by A27, A28, EQREL_1: 22;

            end;

             P[z] from FiniteTransitivity( A10, A9, A11, A23);

            hence thesis by A4;

          end;

        end;

          suppose ( product p) misses ( dom f);

          then (( product p) /\ ( dom f)) = {} ;

          

          then (f .: ( product p)) = (f .: {} ) by RELAT_1: 112

          .= {} ;

          then (f .: ( product p)) c= a0;

          hence ex a be Element of P st (f .: ( product p)) c= a;

        end;

      end;

      let p be FinSequence of P;

      assume ( product p) meets ( dom f);

      then

      consider x be object such that

       A29: x in ( product p) and

       A30: x in ( dom f) by XBOOLE_0: 3;

      let y be object;

      assume

       A31: y in ( product p);

      

       A32: ( product p) c= ( Funcs (( dom p),( Union p))) by FUNCT_6: 1;

      then

       A33: ex f be Function st x = f & ( dom f) = ( dom p) & ( rng f) c= ( Union p) by A29, FUNCT_2:def 2;

      

       A34: ex f be Function st y = f & ( dom f) = ( dom p) & ( rng f) c= ( Union p) by A31, A32, FUNCT_2:def 2;

      reconsider x, z = y as Function by A29, A31;

      

       A35: ( dom p) = ( Seg ( len p)) by FINSEQ_1:def 3;

      then

      reconsider x, z as FinSequence by A33, A34, FINSEQ_1:def 2;

      defpred P[ set] means $1 in ( dom f);

      defpred R[ set, set] means [$1, $2] in ( LimDomRel A);

      ( len x) = ( len p) by A33, A35, FINSEQ_1:def 3;

      then

       A36: ( len x) = ( len z) by A34, A35, FINSEQ_1:def 3;

      

       A37: P[x] by A30;

      

       A38: for p1,q1 be FinSequence, z1,z2 be set st P[((p1 ^ <*z1*>) ^ q1)] & R[z1, z2] holds P[((p1 ^ <*z2*>) ^ q1)]

      proof

        let p1,q1 be FinSequence, z1,z2 be set;

        assume that

         A39: ((p1 ^ <*z1*>) ^ q1) in ( dom f) and

         A40: [z1, z2] in ( LimDomRel A);

        

         A41: ( LimDomRel A) c= ( DomRel A) by Th21;

        

         A42: z1 in the carrier of A by A40, ZFMISC_1: 87;

        z2 in the carrier of A by A40, ZFMISC_1: 87;

        hence thesis by A39, A40, A41, A42, Def4;

      end;

      

       A43: for i be Element of NAT st i in ( dom x) holds R[(x . i), (z . i)]

      proof

        let i be Element of NAT ;

        assume

         A44: i in ( dom x);

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

        then

        reconsider a = (p . i) as Element of P;

        

         A45: ex g be Function st x = g & ( dom g) = ( dom p) & for x be object st x in ( dom p) holds (g . x) in (p . x) by A29, CARD_3:def 5;

        

         A46: ex g be Function st z = g & ( dom g) = ( dom p) & for x be object st x in ( dom p) holds (g . x) in (p . x) by A31, CARD_3:def 5;

        

         A47: ex b be object st b in the carrier of A & a = ( Class (( LimDomRel A),b)) by EQREL_1:def 3;

        

         A48: (x . i) in a by A44, A45;

        (z . i) in a by A44, A45, A46;

        hence thesis by A47, A48, EQREL_1: 22;

      end;

       P[z] from FiniteTransitivity( A37, A36, A38, A43);

      hence thesis;

    end;

    definition

      let A be partial non-empty UAStr;

      :: PUA2MSS1:def10

      mode a_partition of A -> a_partition of the carrier of A means

      : Def10: for f be operation of A holds f is_exactly_partitable_wrt it ;

      existence

      proof

        for f be operation of A holds f is_exactly_partitable_wrt ( Class ( LimDomRel A)) by Th23;

        hence thesis;

      end;

    end

    definition

      let A be partial non-empty UAStr;

      :: PUA2MSS1:def11

      mode IndexedPartition of A -> IndexedPartition of the carrier of A means

      : Def11: ( rng it ) is a_partition of A;

      existence

      proof

        set P = the a_partition of A;

        take ( id P);

        thus thesis;

      end;

    end

    definition

      let A be partial non-empty UAStr;

      let P be IndexedPartition of A;

      :: original: rng

      redefine

      func rng P -> a_partition of A ;

      coherence by Def11;

    end

    theorem :: PUA2MSS1:25

    for A be non-empty partial UAStr holds ( Class ( LimDomRel A)) is a_partition of A

    proof

      let A be partial non-empty UAStr;

      thus for f be operation of A holds f is_exactly_partitable_wrt ( Class ( LimDomRel A)) by Th23;

    end;

    theorem :: PUA2MSS1:26

    

     Th25: for X be non empty set, P be a_partition of X holds for p be FinSequence of P, q1,q2 be FinSequence, x,y be set st ((q1 ^ <*x*>) ^ q2) in ( product p) & ex a be Element of P st x in a & y in a holds ((q1 ^ <*y*>) ^ q2) in ( product p)

    proof

      let X be non empty set, P be a_partition of X;

      let pp be FinSequence of P;

      let p,q be FinSequence;

      let x,y be set;

      assume

       A1: ((p ^ <*x*>) ^ q) in ( product pp);

      given a be Element of P such that

       A2: x in a and

       A3: y in a;

      reconsider x, y as Element of a by A2, A3;

      now

        

         A4: ex g be Function st ((p ^ <*x*>) ^ q) = g & ( dom g) = ( dom pp) & for x be object st x in ( dom pp) holds (g . x) in (pp . x) by A1, CARD_3:def 5;

        

        thus ( dom ((p ^ <*y*>) ^ q)) = ( Seg ( len ((p ^ <*y*>) ^ q))) by FINSEQ_1:def 3

        .= ( Seg (( len (p ^ <*y*>)) + ( len q))) by FINSEQ_1: 22

        .= ( Seg ((( len p) + ( len <*y*>)) + ( len q))) by FINSEQ_1: 22

        .= ( Seg ((( len p) + 1) + ( len q))) by FINSEQ_1: 40

        .= ( Seg ((( len p) + ( len <*x*>)) + ( len q))) by FINSEQ_1: 40

        .= ( Seg (( len (p ^ <*x*>)) + ( len q))) by FINSEQ_1: 22

        .= ( Seg ( len ((p ^ <*x*>) ^ q))) by FINSEQ_1: 22

        .= ( dom pp) by A4, FINSEQ_1:def 3;

        let i be object;

        assume

         A5: i in ( dom pp);

        then

        reconsider ii = i as Element of NAT ;

        

         A6: ( len <*x*>) = 1 by FINSEQ_1: 40;

        

         A7: ( len <*y*>) = 1 by FINSEQ_1: 40;

        

         A8: ( dom <*x*>) = ( Seg 1) by FINSEQ_1: 38;

        

         A9: ( len (p ^ <*x*>)) = (( len p) + 1) by A6, FINSEQ_1: 22;

        

         A10: ( len (p ^ <*y*>)) = (( len p) + 1) by A7, FINSEQ_1: 22;

        

         A11: ( dom (p ^ <*x*>)) = ( Seg (( len p) + 1)) by A9, FINSEQ_1:def 3;

        

         A12: ( dom (p ^ <*y*>)) = ( Seg (( len p) + 1)) by A10, FINSEQ_1:def 3;

        

         A13: ii in ( dom (p ^ <*x*>)) or ex n be Nat st n in ( dom q) & ii = (( len (p ^ <*x*>)) + n) by A4, A5, FINSEQ_1: 25;

        

         A14: ( dom p) c= ( dom (p ^ <*y*>)) by FINSEQ_1: 26;

        per cases by A13, FINSEQ_1: 25;

          suppose

           A15: ii in ( dom p);

          then

           A16: ((p ^ <*y*>) . i) = (p . i) by FINSEQ_1:def 7;

          

           A17: ((p ^ <*x*>) . i) = (p . i) by A15, FINSEQ_1:def 7;

          

           A18: (((p ^ <*y*>) ^ q) . i) = (p . i) by A14, A15, A16, FINSEQ_1:def 7;

          (((p ^ <*x*>) ^ q) . i) = (p . i) by A11, A12, A14, A15, A17, FINSEQ_1:def 7;

          hence (((p ^ <*y*>) ^ q) . i) in (pp . i) by A4, A5, A18;

        end;

          suppose ex n be Nat st n in ( dom <*x*>) & ii = (( len p) + n);

          then

          consider n be Nat such that

           A19: n in ( Seg 1) and

           A20: ii = (( len p) + n) by A8;

          

           A21: n = 1 by A19, FINSEQ_1: 2, TARSKI:def 1;

          then

           A22: ((p ^ <*x*>) . ii) = x by A20, FINSEQ_1: 42;

          

           A23: ((p ^ <*y*>) . ii) = y by A20, A21, FINSEQ_1: 42;

          

           A24: ii in ( dom (p ^ <*y*>)) by A12, A20, A21, FINSEQ_1: 4;

          then

           A25: (((p ^ <*x*>) ^ q) . ii) = x by A11, A12, A22, FINSEQ_1:def 7;

          

           A26: (((p ^ <*y*>) ^ q) . ii) = y by A23, A24, FINSEQ_1:def 7;

          

           A27: x in (pp . i) by A4, A5, A25;

          (pp . i) in ( rng pp) by A5, FUNCT_1:def 3;

          then

           A28: (pp . i) in P;

          a meets (pp . i) by A27, XBOOLE_0: 3;

          then (pp . i) = a by A28, EQREL_1:def 4;

          hence (((p ^ <*y*>) ^ q) . i) in (pp . i) by A26;

        end;

          suppose ex n be Element of NAT st n in ( dom q) & ii = (( len (p ^ <*x*>)) + n);

          then

          consider n be Element of NAT such that

           A29: n in ( dom q) and

           A30: ii = (( len (p ^ <*x*>)) + n);

          

           A31: (((p ^ <*y*>) ^ q) . i) = (q . n) by A9, A10, A29, A30, FINSEQ_1:def 7;

          (((p ^ <*x*>) ^ q) . i) = (q . n) by A29, A30, FINSEQ_1:def 7;

          hence (((p ^ <*y*>) ^ q) . i) in (pp . i) by A4, A5, A31;

        end;

      end;

      hence thesis by CARD_3:def 5;

    end;

    theorem :: PUA2MSS1:27

    

     Th26: for A be partial non-empty UAStr, P be a_partition of A holds P is_finer_than ( Class ( LimDomRel A))

    proof

      let A be partial non-empty UAStr;

      let P be a_partition of A;

      consider EP be Equivalence_Relation of the carrier of A such that

       A1: P = ( Class EP) by EQREL_1: 34;

      let a be set;

      assume a in P;

      then

      reconsider aa = a as Element of P;

      set x = the Element of aa;

      take ( Class (( LimDomRel A),x));

      thus ( Class (( LimDomRel A),x)) in ( Class ( LimDomRel A)) by EQREL_1:def 3;

      let y be object;

      assume y in a;

      then

      reconsider y as Element of aa;

      reconsider x, y as Element of A;

      defpred P[ Nat] means EP c= (( DomRel A) |^ (A,$1));

      

       A2: P[ 0 ]

      proof

        let x,y be object;

        assume

         A3: [x, y] in EP;

        then

        reconsider x, y as Element of A by ZFMISC_1: 87;

        reconsider a = ( Class (EP,y)) as Element of P by A1, EQREL_1:def 3;

        

         A4: x in a by A3, EQREL_1: 19;

        

         A5: y in a by EQREL_1: 20;

        for f be operation of A, p,q be FinSequence holds ((p ^ <*x*>) ^ q) in ( dom f) iff ((p ^ <*y*>) ^ q) in ( dom f)

        proof

          let f be operation of A, p,q be FinSequence;

          

           A6: f is_exactly_partitable_wrt P by Def10;

          now

            let p,q be FinSequence, x,y be Element of a;

            assume

             A7: ((p ^ <*x*>) ^ q) in ( dom f);

            then ((p ^ <*x*>) ^ q) is FinSequence of the carrier of A by FINSEQ_1:def 11;

            then

            consider pp be FinSequence of P such that

             A8: ((p ^ <*x*>) ^ q) in ( product pp) by Th6;

            ( product pp) meets ( dom f) by A7, A8, XBOOLE_0: 3;

            then

             A9: ( product pp) c= ( dom f) by A6;

            ((p ^ <*y*>) ^ q) in ( product pp) by A8, Th25;

            hence ((p ^ <*y*>) ^ q) in ( dom f) by A9;

          end;

          hence thesis by A4, A5;

        end;

        then [x, y] in ( DomRel A) by Def4;

        hence thesis by Th15;

      end;

      

       A10: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        assume

         A11: EP c= (( DomRel A) |^ (A,i));

        let x,y be object;

        assume

         A12: [x, y] in EP;

        then

        reconsider x, y as Element of A by ZFMISC_1: 87;

        reconsider a = ( Class (EP,y)) as Element of P by A1, EQREL_1:def 3;

        now

          let f be operation of A, p,q be FinSequence;

          assume that

           A13: ((p ^ <*x*>) ^ q) in ( dom f) and

           A14: ((p ^ <*y*>) ^ q) in ( dom f);

          ((p ^ <*x*>) ^ q) is FinSequence of the carrier of A by A13, FINSEQ_1:def 11;

          then

          consider pp be FinSequence of P such that

           A15: ((p ^ <*x*>) ^ q) in ( product pp) by Th6;

          f is_exactly_partitable_wrt P by Def10;

          then f is_partitable_wrt P;

          then

          consider c be Element of P such that

           A16: (f .: ( product pp)) c= c;

          

           A17: x in a by A12, EQREL_1: 19;

          y in a by EQREL_1: 20;

          then

           A18: ((p ^ <*y*>) ^ q) in ( product pp) by A15, A17, Th25;

          

           A19: (f . ((p ^ <*x*>) ^ q)) in (f .: ( product pp)) by A13, A15, FUNCT_1:def 6;

          

           A20: (f . ((p ^ <*y*>) ^ q)) in (f .: ( product pp)) by A14, A18, FUNCT_1:def 6;

          ex x be object st x in the carrier of A & c = ( Class (EP,x)) by A1, EQREL_1:def 3;

          then [(f . ((p ^ <*x*>) ^ q)), (f . ((p ^ <*y*>) ^ q))] in EP by A16, A19, A20, EQREL_1: 22;

          hence [(f . ((p ^ <*x*>) ^ q)), (f . ((p ^ <*y*>) ^ q))] in (( DomRel A) |^ (A,i)) by A11;

        end;

        then [x, y] in ((( DomRel A) |^ (A,i)) |^ A) by A11, A12, Def5;

        hence thesis by Th16;

      end;

      

       A21: for i be Nat holds P[i] from NAT_1:sch 2( A2, A10);

      now

        let i be Element of NAT ;

        ex x be object st x in the carrier of A & aa = ( Class (EP,x)) by A1, EQREL_1:def 3;

        then

         A22: [x, y] in EP by EQREL_1: 22;

        EP c= (( DomRel A) |^ (A,i)) by A21;

        hence [x, y] in (( DomRel A) |^ (A,i)) by A22;

      end;

      then [x, y] in ( LimDomRel A) by Def7;

      then [y, x] in ( LimDomRel A) by EQREL_1: 6;

      hence thesis by EQREL_1: 19;

    end;

    begin

    definition

      let S1,S2 be ManySortedSign;

      let f,g be Function;

      :: PUA2MSS1:def12

      pred f,g form_morphism_between S1,S2 means ( dom f) = the carrier of S1 & ( dom g) = the carrier' of S1 & ( rng f) c= the carrier of S2 & ( rng g) c= the carrier' of S2 & (f * the ResultSort of S1) = (the ResultSort of S2 * g) & for o be set, p be Function st o in the carrier' of S1 & p = (the Arity of S1 . o) holds (f * p) = (the Arity of S2 . (g . o));

    end

    theorem :: PUA2MSS1:28

    

     Th27: for S be non void non empty ManySortedSign holds (( id the carrier of S),( id the carrier' of S)) form_morphism_between (S,S)

    proof

      let S be non void non empty ManySortedSign;

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

      

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

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

      then (f * the ResultSort of S) = the ResultSort of S by RELAT_1: 53;

      hence ( dom f) = the carrier of S & ( dom g) = the carrier' of S & ( rng f) c= the carrier of S & ( rng g) c= the carrier' of S & (f * the ResultSort of S) = (the ResultSort of S * g) by A1, RELAT_1: 52;

      let o be set, p be Function;

      assume that

       A2: o in the carrier' of S and

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

      

       A4: (g . o) = o by A2, FUNCT_1: 17;

      p in (the carrier of S * ) by A2, A3, FUNCT_2: 5;

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

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

      hence thesis by A3, A4, RELAT_1: 53;

    end;

    theorem :: PUA2MSS1:29

    

     Th28: for S1,S2,S3 be ManySortedSign holds for f1,f2,g1,g2 be Function st (f1,g1) form_morphism_between (S1,S2) & (f2,g2) form_morphism_between (S2,S3) holds ((f2 * f1),(g2 * g1)) form_morphism_between (S1,S3)

    proof

      let S1,S2,S3 be ManySortedSign;

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

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

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

       A3: ( rng f1) c= the carrier of S2 and

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

       A5: (f1 * the ResultSort of S1) = (the ResultSort of S2 * g1) and

       A6: 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 S2 . (g1 . o)) and

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

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

       A9: ( rng f2) c= the carrier of S3 and

       A10: ( rng g2) c= the carrier' of S3 and

       A11: (f2 * the ResultSort of S2) = (the ResultSort of S3 * g2) and

       A12: 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 S3 . (g2 . o));

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

      thus ( dom f) = the carrier of S1 & ( dom g) = the carrier' of S1 by A1, A2, A3, A4, A7, A8, RELAT_1: 27;

      

       A13: ( rng f) c= ( rng f2) by RELAT_1: 26;

      ( rng g) c= ( rng g2) by RELAT_1: 26;

      hence ( rng f) c= the carrier of S3 & ( rng g) c= the carrier' of S3 by A9, A10, A13;

      

      thus (f * the ResultSort of S1) = (f2 * (the ResultSort of S2 * g1)) by A5, RELAT_1: 36

      .= ((f2 * the ResultSort of S2) * g1) by RELAT_1: 36

      .= (the ResultSort of S3 * g) by A11, RELAT_1: 36;

      let o be set, p be Function;

      assume that

       A14: o in the carrier' of S1 and

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

      

       A16: (f1 * p) = (the Arity of S2 . (g1 . o)) by A6, A14, A15;

      

       A17: (g1 . o) in ( rng g1) by A2, A14, FUNCT_1:def 3;

      

       A18: (f * p) = (f2 * (f1 * p)) by RELAT_1: 36;

      (g . o) = (g2 . (g1 . o)) by A2, A14, FUNCT_1: 13;

      hence thesis by A4, A12, A16, A17, A18;

    end;

    definition

      let S1,S2 be ManySortedSign;

      :: PUA2MSS1:def13

      pred S1 is_rougher_than S2 means ex f,g be Function st (f,g) form_morphism_between (S2,S1) & ( rng f) = the carrier of S1 & ( rng g) = the carrier' of S1;

    end

    definition

      let S1,S2 be non void non empty ManySortedSign;

      :: original: is_rougher_than

      redefine

      pred S1 is_rougher_than S2;

      reflexivity

      proof

        let S be non void non empty ManySortedSign;

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

        thus (f,g) form_morphism_between (S,S) & ( rng f) = the carrier of S & ( rng g) = the carrier' of S by Th27;

      end;

    end

    theorem :: PUA2MSS1:30

    for S1,S2,S3 be ManySortedSign st S1 is_rougher_than S2 & S2 is_rougher_than S3 holds S1 is_rougher_than S3

    proof

      let S1,S2,S3 be ManySortedSign;

      given f1,g1 be Function such that

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

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

       A3: ( rng g1) = the carrier' of S1;

      given f2,g2 be Function such that

       A4: (f2,g2) form_morphism_between (S3,S2) and

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

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

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

      thus (f,g) form_morphism_between (S3,S1) by A1, A4, Th28;

      

       A7: ( dom f1) = the carrier of S2 by A1;

      ( dom g1) = the carrier' of S2 by A1;

      hence thesis by A2, A3, A5, A6, A7, RELAT_1: 28;

    end;

    begin

    definition

      let A be partial non-empty UAStr;

      let P be a_partition of A;

      :: PUA2MSS1:def14

      func MSSign (A,P) -> strict ManySortedSign means

      : Def14: the carrier of it = P & the carrier' of it = { [o, p] where o be OperSymbol of A, p be Element of (P * ) : ( product p) meets ( dom ( Den (o,A))) } & for o be OperSymbol of A, p be Element of (P * ) st ( product p) meets ( dom ( Den (o,A))) holds (the Arity of it . [o, p]) = p & (( Den (o,A)) .: ( product p)) c= (the ResultSort of it . [o, p]);

      existence

      proof

        set O = { [f, p] where f be OperSymbol of A, p be Element of (P * ) : ( product p) meets ( dom ( Den (f,A))) };

        defpred Q[ object, object] means ex f be OperSymbol of A, q be Element of (P * ) st q = $2 & $1 = [f, q];

        

         A1: for o be object st o in O holds ex p be object st p in (P * ) & Q[o, p]

        proof

          let o be object;

          assume o in O;

          then

          consider f be OperSymbol of A, p be Element of (P * ) such that

           A2: o = [f, p] and ( product p) meets ( dom ( Den (f,A)));

          take p;

          thus thesis by A2;

        end;

        defpred S[ object, object] means ex D2 be set, f be OperSymbol of A, p be Element of (P * ) st D2 = $2 & $1 = [f, p] & (( Den (f,A)) .: ( product p)) c= D2;

        

         A3: for o be object st o in O holds ex r be object st r in P & S[o, r]

        proof

          let o be object;

          assume o in O;

          then

          consider f be OperSymbol of A, p be Element of (P * ) such that

           A4: o = [f, p] and ( product p) meets ( dom ( Den (f,A)));

          ( Den (f,A)) is_exactly_partitable_wrt P by Def10;

          then ( Den (f,A)) is_partitable_wrt P;

          then ex a be Element of P st (( Den (f,A)) .: ( product p)) c= a;

          hence thesis by A4;

        end;

        consider Ar be Function such that

         A5: ( dom Ar) = O & ( rng Ar) c= (P * ) and

         A6: for o be object st o in O holds Q[o, (Ar . o)] from FUNCT_1:sch 6( A1);

        reconsider Ar as Function of O, (P * ) by A5, FUNCT_2: 2;

        consider R be Function such that

         A7: ( dom R) = O & ( rng R) c= P and

         A8: for o be object st o in O holds S[o, (R . o)] from FUNCT_1:sch 6( A3);

        reconsider R as Function of O, P by A7, FUNCT_2: 2;

        take S = ManySortedSign (# P, O, Ar, R #);

        thus the carrier of S = P & the carrier' of S = O;

        let f be OperSymbol of A, p be Element of (P * );

        set o = [f, p];

        assume ( product p) meets ( dom ( Den (f,A)));

        then

         A9: o in O;

        then

         A10: ex f1 be OperSymbol of A, q1 be Element of (P * ) st (q1 = (Ar . o)) & (o = [f1, q1]) by A6;

         S[o, (R . o)] by A8, A9;

        then

        consider f2 be OperSymbol of A, q2 be Element of (P * ) such that

         A11: o = [f2, q2] and

         A12: (( Den (f2,A)) .: ( product q2)) c= (R . o);

        q2 = p by A11, XTUPLE_0: 1;

        hence thesis by A10, A11, A12, XTUPLE_0: 1;

      end;

      correctness

      proof

        set O = { [f, p] where f be OperSymbol of A, p be Element of (P * ) : ( product p) meets ( dom ( Den (f,A))) };

        let S1,S2 be strict ManySortedSign such that

         A13: the carrier of S1 = P and

         A14: the carrier' of S1 = O and

         A15: for f be OperSymbol of A, p be Element of (P * ) st ( product p) meets ( dom ( Den (f,A))) holds (the Arity of S1 . [f, p]) = p & (( Den (f,A)) .: ( product p)) c= (the ResultSort of S1 . [f, p]) and

         A16: the carrier of S2 = P and

         A17: the carrier' of S2 = O and

         A18: for f be OperSymbol of A, p be Element of (P * ) st ( product p) meets ( dom ( Den (f,A))) holds (the Arity of S2 . [f, p]) = p & (( Den (f,A)) .: ( product p)) c= (the ResultSort of S2 . [f, p]);

        

         A19: ( dom the Arity of S1) = O by A14, FUNCT_2:def 1;

        

         A20: ( dom the Arity of S2) = O by A17, FUNCT_2:def 1;

        now

          let o be object;

          assume o in O;

          then

          consider f be OperSymbol of A, p be Element of (P * ) such that

           A21: o = [f, p] and

           A22: ( product p) meets ( dom ( Den (f,A)));

          

          thus (the Arity of S1 . o) = p by A15, A21, A22

          .= (the Arity of S2 . o) by A18, A21, A22;

        end;

        then

         A23: the Arity of S1 = the Arity of S2 by A19, A20;

        

         A24: ( dom the ResultSort of S1) = O by A13, A14, FUNCT_2:def 1;

        

         A25: ( dom the ResultSort of S2) = O by A16, A17, FUNCT_2:def 1;

        consider R be Equivalence_Relation of the carrier of A such that

         A26: P = ( Class R) by EQREL_1: 34;

        now

          let o be object;

          assume

           A27: o in O;

          then

          consider f be OperSymbol of A, p be Element of (P * ) such that

           A28: o = [f, p] and

           A29: ( product p) meets ( dom ( Den (f,A)));

          consider x be object such that

           A30: x in ( product p) and

           A31: x in ( dom ( Den (f,A))) by A29, XBOOLE_0: 3;

          

           A32: (( Den (f,A)) . x) in (( Den (f,A)) .: ( product p)) by A30, A31, FUNCT_1:def 6;

          

           A33: (( Den (f,A)) .: ( product p)) c= (the ResultSort of S1 . o) by A15, A28, A29;

          

           A34: (( Den (f,A)) .: ( product p)) c= (the ResultSort of S2 . o) by A18, A28, A29;

          

           A35: (the ResultSort of S1 . o) in P by A13, A14, A27, FUNCT_2: 5;

          

           A36: (the ResultSort of S2 . o) in P by A16, A17, A27, FUNCT_2: 5;

          

           A37: ex y be object st y in the carrier of A & (the ResultSort of S1 . o) = ( Class (R,y)) by A26, A35, EQREL_1:def 3;

          

           A38: ex y be object st y in the carrier of A & (the ResultSort of S2 . o) = ( Class (R,y)) by A26, A36, EQREL_1:def 3;

          (the ResultSort of S1 . o) = ( Class (R,(( Den (f,A)) . x))) by A32, A33, A37, EQREL_1: 23;

          hence (the ResultSort of S1 . o) = (the ResultSort of S2 . o) by A32, A34, A38, EQREL_1: 23;

        end;

        hence thesis by A13, A14, A16, A17, A23, A24, A25, FUNCT_1: 2;

      end;

    end

    registration

      let A be partial non-empty UAStr;

      let P be a_partition of A;

      cluster ( MSSign (A,P)) -> non empty non void;

      coherence

      proof

        thus the carrier of ( MSSign (A,P)) is non empty by Def14;

        set g = the OperSymbol of A;

        set x = the Element of ( dom ( Den (g,A)));

        reconsider x as Element of (the carrier of A * );

        

         A1: ( union P) = the carrier of A by EQREL_1:def 4;

        ( rng x) c= the carrier of A;

        then

        consider q be Function such that

         A2: ( dom q) = ( dom x) and

         A3: ( rng q) c= P and

         A4: x in ( product q) by A1, Th5;

        ( dom x) = ( Seg ( len x)) by FINSEQ_1:def 3;

        then

        reconsider q as FinSequence by A2, FINSEQ_1:def 2;

        reconsider q as FinSequence of P by A3, FINSEQ_1:def 4;

        reconsider q as Element of (P * ) by FINSEQ_1:def 11;

        

         A5: ( product q) meets ( dom ( Den (g,A))) by A4, XBOOLE_0: 3;

        the carrier' of ( MSSign (A,P)) = { [f, p] where f be OperSymbol of A, p be Element of (P * ) : ( product p) meets ( dom ( Den (f,A))) } by Def14;

        then [g, q] in the carrier' of ( MSSign (A,P)) by A5;

        hence the carrier' of ( MSSign (A,P)) is non empty;

      end;

    end

    definition

      let A be partial non-empty UAStr;

      let P be a_partition of A;

      let o be OperSymbol of ( MSSign (A,P));

      :: original: `1

      redefine

      func o `1 -> OperSymbol of A ;

      coherence

      proof

        

         A1: o in the carrier' of ( MSSign (A,P));

        the carrier' of ( MSSign (A,P)) = { [f, p] where f be OperSymbol of A, p be Element of (P * ) : ( product p) meets ( dom ( Den (f,A))) } by Def14;

        then ex f be OperSymbol of A, p be Element of (P * ) st o = [f, p] & ( product p) meets ( dom ( Den (f,A))) by A1;

        hence thesis;

      end;

      :: original: `2

      redefine

      func o `2 -> Element of (P * ) ;

      coherence

      proof

        

         A2: o in the carrier' of ( MSSign (A,P));

        the carrier' of ( MSSign (A,P)) = { [f, p] where f be OperSymbol of A, p be Element of (P * ) : ( product p) meets ( dom ( Den (f,A))) } by Def14;

        then ex f be OperSymbol of A, p be Element of (P * ) st o = [f, p] & ( product p) meets ( dom ( Den (f,A))) by A2;

        hence thesis;

      end;

    end

    definition

      let A be partial non-empty UAStr;

      let S be non void non empty ManySortedSign;

      let G be MSAlgebra over S;

      let P be IndexedPartition of the carrier' of S;

      :: PUA2MSS1:def15

      pred A can_be_characterized_by S,G,P means the Sorts of G is IndexedPartition of A & ( dom P) = ( dom the charact of A) & for o be OperSymbol of A holds (the Charact of G | (P . o)) is IndexedPartition of ( Den (o,A));

    end

    definition

      let A be partial non-empty UAStr;

      let S be non void non empty ManySortedSign;

      :: PUA2MSS1:def16

      pred A can_be_characterized_by S means ex G be MSAlgebra over S, P be IndexedPartition of the carrier' of S st A can_be_characterized_by (S,G,P);

    end

    theorem :: PUA2MSS1:31

    for A be partial non-empty UAStr, P be a_partition of A holds A can_be_characterized_by ( MSSign (A,P))

    proof

      let A be partial non-empty UAStr;

      let P be a_partition of A;

      set S = ( MSSign (A,P));

      P = the carrier of S by Def14;

      then

      reconsider Z = ( id P) as ManySortedSet of the carrier of S;

      deffunc F1( OperSymbol of S) = (( Den (($1 `1 ),A)) | ( product ($1 `2 )));

      consider D be ManySortedSet of the carrier' of S such that

       A1: for o be OperSymbol of S holds (D . o) = F1(o) from PBOOLE:sch 5;

      deffunc F2( OperSymbol of A) = { a where a be OperSymbol of S : (a `1 ) = $1 };

      consider Q be ManySortedSet of ( dom the charact of A) such that

       A2: for o be OperSymbol of A holds (Q . o) = F2(o) from PBOOLE:sch 5;

      

       A3: ( dom Q) = ( dom the charact of A) by PARTFUN1:def 2;

      

       A4: the carrier of S = P by Def14;

      

       A5: the carrier' of S = { [o, p] where o be OperSymbol of A, p be Element of (P * ) : ( product p) meets ( dom ( Den (o,A))) } by Def14;

      Q is non-empty

      proof

        let x be object;

        assume x in ( dom Q);

        then

        reconsider o = x as OperSymbol of A;

        set y = the Element of ( dom ( Den (o,A)));

        reconsider y as Element of (the carrier of A * );

        

         A6: ( rng y) c= the carrier of A;

        the carrier of A = ( union P) by EQREL_1:def 4;

        then

        consider f be Function such that

         A7: ( dom f) = ( dom y) and

         A8: ( rng f) c= P and

         A9: y in ( product f) by A6, Th5;

        ( dom y) = ( Seg ( len y)) by FINSEQ_1:def 3;

        then f is FinSequence by A7, FINSEQ_1:def 2;

        then f is FinSequence of P by A8, FINSEQ_1:def 4;

        then

        reconsider f as Element of (P * ) by FINSEQ_1:def 11;

        ( product f) meets ( dom ( Den (o,A))) by A9, XBOOLE_0: 3;

        then

         A10: [o, f] in the carrier' of S by A5;

        

         A11: ( [o, f] `1 ) = o;

        (Q . o) = { a where a be OperSymbol of S : (a `1 ) = o } by A2;

        then [o, f] in (Q . x) by A10, A11;

        hence thesis;

      end;

      then

      reconsider Q as non-empty Function;

      D is ManySortedFunction of ((Z # ) * the Arity of S), (Z * the ResultSort of S)

      proof

        let x be object;

        assume

         A12: x in the carrier' of S;

        then

        consider o be OperSymbol of A, p be Element of (P * ) such that

         A13: x = [o, p] and

         A14: ( product p) meets ( dom ( Den (o,A))) by A5;

        reconsider xx = x as OperSymbol of S by A12;

        

         A15: ( rng the ResultSort of S) c= the carrier of S;

        

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

        

         A17: ( rng p) c= P;

        

         A18: (the Arity of S . x) = p by A13, A14, Def14;

        

         A19: ((Z # ) . p) = ( product (Z * p)) by A4, FINSEQ_2:def 5;

        (Z * p) = p by A17, RELAT_1: 53;

        then

         A20: (((Z # ) * the Arity of S) . x) = ( product p) by A12, A16, A18, A19, FUNCT_1: 13;

        

         A21: (( Den (o,A)) .: ( product p)) c= (the ResultSort of S . x) by A13, A14, Def14;

        

         A22: (xx `2 ) = p by A13;

        

         A23: (xx `1 ) = o by A13;

        

         A24: ( rng (( Den (o,A)) | ( product p))) = (( Den (o,A)) .: ( product p)) by RELAT_1: 115;

        

         A25: (D . xx) = (( Den (o,A)) | ( product p)) by A1, A22, A23;

        ( Den (o,A)) is_exactly_partitable_wrt P by Def10;

        then

         A26: ( product p) c= ( dom ( Den (o,A))) by A14;

        

         A27: (Z * the ResultSort of S) = the ResultSort of S by A4, A15, RELAT_1: 53;

        ( dom (( Den (o,A)) | ( product p))) = ( product p) by A26, RELAT_1: 62;

        hence thesis by A20, A21, A24, A25, A27, FUNCT_2: 2;

      end;

      then

      reconsider D as ManySortedFunction of ((Z # ) * the Arity of S), (Z * the ResultSort of S);

      

       A28: ( Union Q) = the carrier' of S

      proof

        hereby

          let x be object;

          assume x in ( Union Q);

          then

          consider y be object such that

           A29: y in ( dom Q) and

           A30: x in (Q . y) by CARD_5: 2;

          reconsider y as OperSymbol of A by A29, PARTFUN1:def 2;

          (Q . y) = { a where a be OperSymbol of S : (a `1 ) = y } by A2;

          then ex a be OperSymbol of S st x = a & (a `1 ) = y by A30;

          hence x in the carrier' of S;

        end;

        let x be object;

        assume x in the carrier' of S;

        then

        reconsider b = x as OperSymbol of S;

        (Q . (b `1 )) = { a where a be OperSymbol of S : (a `1 ) = (b `1 ) } by A2;

        then b in (Q . (b `1 ));

        hence thesis by A3, CARD_5: 2;

      end;

      now

        let x,y be set;

        assume that

         A31: x in ( dom Q) and

         A32: y in ( dom Q) and

         A33: x <> y;

        reconsider a = x, b = y as OperSymbol of A by A31, A32, PARTFUN1:def 2;

        thus (Q . x) misses (Q . y)

        proof

          assume (Q . x) meets (Q . y);

          then

          consider z be object such that

           A34: z in (Q . x) and

           A35: z in (Q . y) by XBOOLE_0: 3;

          

           A36: (Q . a) = { c where c be OperSymbol of S : (c `1 ) = a } by A2;

          

           A37: (Q . b) = { c where c be OperSymbol of S : (c `1 ) = b } by A2;

          

           A38: ex c1 be OperSymbol of S st z = c1 & (c1 `1 ) = a by A34, A36;

          ex c2 be OperSymbol of S st z = c2 & (c2 `1 ) = b by A35, A37;

          hence contradiction by A33, A38;

        end;

      end;

      then

      reconsider Q as IndexedPartition of the carrier' of S by A28, Th13;

      take G = MSAlgebra (# Z, D #), Q;

      ( rng ( id P)) is a_partition of A;

      hence the Sorts of G is IndexedPartition of A by Def11;

      thus ( dom Q) = ( dom the charact of A) by PARTFUN1:def 2;

      let o be OperSymbol of A;

      reconsider PP = the set of all ( product p) where p be Element of (P * ) as a_partition of (the carrier of A * ) by Th8;

      reconsider QQ = { (a /\ ( dom ( Den (o,A)))) where a be Element of PP : a meets ( dom ( Den (o,A))) } as a_partition of ( dom ( Den (o,A))) by Th10;

      set F = (the Charact of G | (Q . o));

      

       A39: (Q . o) in ( rng Q) by A3, FUNCT_1:def 3;

      

       A40: ( dom D) = the carrier' of S by PARTFUN1:def 2;

      then

       A41: ( dom F) = (Q . o) by A39, RELAT_1: 62;

      reconsider F as non empty Function by A39, A40;

      reconsider Qo = (Q . o) as non empty set;

      reconsider RR = the set of all (( Den (o,A)) | a) where a be Element of QQ as a_partition of ( Den (o,A)) by Th11;

      

       A42: (Q . o) = { a where a be OperSymbol of S : (a `1 ) = o } by A2;

      ( rng F) c= RR

      proof

        let y be object;

        assume y in ( rng F);

        then

        consider x be object such that

         A43: x in ( dom F) and

         A44: y = (F . x) by FUNCT_1:def 3;

        x in (( dom the Charact of G) /\ (Q . o)) by A43, RELAT_1: 61;

        then x in (Q . o) by XBOOLE_0:def 4;

        then

        consider a be OperSymbol of S such that

         A45: x = a and

         A46: (a `1 ) = o by A42;

        a in the carrier' of S;

        then

        consider s be OperSymbol of A, p be Element of (P * ) such that

         A47: a = [s, p] and

         A48: ( product p) meets ( dom ( Den (s,A))) by A5;

        

         A49: s = o by A46, A47;

        

         A50: (a `2 ) = p by A47;

        

         A51: ( product p) in PP;

        

         A52: ( Den (o,A)) is_exactly_partitable_wrt P by Def10;

        

         A53: (( product p) /\ ( dom ( Den (o,A)))) in QQ by A48, A49, A51;

        ( product p) c= ( dom ( Den (o,A))) by A48, A49, A52;

        then ( product p) in QQ by A53, XBOOLE_1: 28;

        then

         A54: (( Den (o,A)) | ( product p)) in RR;

        y = (D . a) by A43, A44, A45, FUNCT_1: 47;

        hence thesis by A1, A46, A50, A54;

      end;

      then

      reconsider F as Function of Qo, RR by A41, FUNCT_2: 2;

      

       A55: RR c= ( rng F)

      proof

        let x be object;

        assume x in RR;

        then

        consider a be Element of QQ such that

         A56: x = (( Den (o,A)) | a);

        a in QQ;

        then

        consider b be Element of PP such that

         A57: a = (b /\ ( dom ( Den (o,A)))) and

         A58: b meets ( dom ( Den (o,A)));

        b in PP;

        then

        consider p be Element of (P * ) such that

         A59: b = ( product p);

        ( Den (o,A)) is_exactly_partitable_wrt P by Def10;

        then ( product p) c= ( dom ( Den (o,A))) by A58, A59;

        then

         A60: b = a by A57, A59, XBOOLE_1: 28;

        

         A61: [o, p] in the carrier' of S by A5, A58, A59;

        

         A62: ( [o, p] `1 ) = o;

        

         A63: ( [o, p] `2 ) = p;

        

         A64: [o, p] in ( dom D) by A61, PARTFUN1:def 2;

        

         A65: [o, p] in (Q . o) by A42, A61, A62;

        (D . [o, p]) = x by A1, A56, A59, A60, A61, A62, A63;

        hence thesis by A64, A65, FUNCT_1: 50;

      end;

      F is one-to-one

      proof

        let x1,x2 be object;

        assume that

         A66: x1 in ( dom F) and

         A67: x2 in ( dom F) and

         A68: (F . x1) = (F . x2);

        consider a1 be OperSymbol of S such that

         A69: x1 = a1 and

         A70: (a1 `1 ) = o by A41, A42, A66;

        consider a2 be OperSymbol of S such that

         A71: x2 = a2 and

         A72: (a2 `1 ) = o by A41, A42, A67;

        a1 in the carrier' of S;

        then

        consider o1 be OperSymbol of A, p1 be Element of (P * ) such that

         A73: a1 = [o1, p1] and

         A74: ( product p1) meets ( dom ( Den (o1,A))) by A5;

        a2 in the carrier' of S;

        then

        consider o2 be OperSymbol of A, p2 be Element of (P * ) such that

         A75: a2 = [o2, p2] and

         A76: ( product p2) meets ( dom ( Den (o2,A))) by A5;

        

         A77: (F . x1) = (D . a1) by A66, A69, FUNCT_1: 47;

        

         A78: (F . x1) = (D . a2) by A67, A68, A71, FUNCT_1: 47;

        

         A79: (a1 `2 ) = p1 by A73;

        

         A80: (a2 `2 ) = p2 by A75;

        

         A81: (F . x1) = (( Den (o,A)) | ( product p1)) by A1, A70, A77, A79;

        

         A82: (F . x1) = (( Den (o,A)) | ( product p2)) by A1, A72, A78, A80;

        

         A83: ( Den (o,A)) is_exactly_partitable_wrt P by Def10;

        

         A84: o = o1 by A70, A73;

        

         A85: o = o2 by A72, A75;

        

         A86: ( product p1) c= ( dom ( Den (o,A))) by A74, A83, A84;

        

         A87: ( product p2) c= ( dom ( Den (o,A))) by A76, A83, A85;

        ( product p1) = ( dom (( Den (o,A)) | ( product p1))) by A86, RELAT_1: 62;

        hence thesis by A69, A71, A73, A75, A81, A82, A84, A85, A87, Th2, RELAT_1: 62;

      end;

      hence thesis by A55, Th14;

    end;

    theorem :: PUA2MSS1:32

    

     Th31: for A be partial non-empty UAStr holds for S be non void non empty ManySortedSign holds for G be MSAlgebra over S holds for Q be IndexedPartition of the carrier' of S st A can_be_characterized_by (S,G,Q) holds for o be OperSymbol of A, r be FinSequence of ( rng the Sorts of G) st ( product r) c= ( dom ( Den (o,A))) holds ex s be OperSymbol of S st (the Sorts of G * ( the_arity_of s)) = r & s in (Q . o)

    proof

      let A be partial non-empty UAStr;

      let S2 be non void non empty ManySortedSign;

      let G be MSAlgebra over S2, Q be IndexedPartition of the carrier' of S2 such that

       A1: the Sorts of G is IndexedPartition of A and

       A2: ( dom Q) = ( dom the charact of A) and

       A3: for o be OperSymbol of A holds (the Charact of G | (Q . o)) is IndexedPartition of ( Den (o,A));

      reconsider R = the Sorts of G as IndexedPartition of A by A1;

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

      then

      reconsider SG = the Sorts of G as Function of the carrier of S2, ( rng R) by RELSET_1: 4;

      let o be OperSymbol of A, r be FinSequence of ( rng the Sorts of G);

      reconsider p = r as Element of (( rng R) * ) by FINSEQ_1:def 11;

      assume

       A4: ( product r) c= ( dom ( Den (o,A)));

      reconsider P = (the Charact of G | (Q . o)) as IndexedPartition of ( Den (o,A)) by A3;

      set h = the Element of ( product p);

      h in ( product r);

      then

       A5: [h, (( Den (o,A)) . h)] in ( Den (o,A)) by A4, FUNCT_1:def 2;

      then

       A6: (P -index_of [h, (( Den (o,A)) . h)]) in ( dom P) by Def3;

      

       A7: [h, (( Den (o,A)) . h)] in (P . (P -index_of [h, (( Den (o,A)) . h)])) by A5, Def3;

      reconsider Qo = (Q . o) as Element of ( rng Q) by A2, FUNCT_1:def 3;

      

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

      then

       A9: ( dom P) = Qo by RELAT_1: 62;

      reconsider s = (P -index_of [h, (( Den (o,A)) . h)]) as Element of Qo by A6, A8, RELAT_1: 62;

      reconsider q = (SG * ( the_arity_of s)) as FinSequence of ( rng R) by Lm2;

      reconsider q as Element of (( rng R) * ) by FINSEQ_1:def 11;

      reconsider Q = the set of all ( product t) where t be Element of (( rng R) * ) as a_partition of (the carrier of A * ) by Th8;

      take s;

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

      

      then

       A10: ( Args (s,G)) = ((the Sorts of G # ) . (the Arity of S2 . s)) by FUNCT_1: 13

      .= ( product q) by FINSEQ_2:def 5;

      

       A11: ( product q) in Q;

      

       A12: ( product p) in Q;

      (P . s) = (the Charact of G . s) by A9, FUNCT_1: 47;

      then h in ( dom ( Den (s,G))) by A7, XTUPLE_0:def 12;

      hence (the Sorts of G * ( the_arity_of s)) = r by A10, A11, A12, Th2, Lm3;

      thus thesis;

    end;

    theorem :: PUA2MSS1:33

    for A be partial non-empty UAStr, P be a_partition of A st P = ( Class ( LimDomRel A)) holds for S be non void non empty ManySortedSign st A can_be_characterized_by S holds ( MSSign (A,P)) is_rougher_than S

    proof

      let A be partial non-empty UAStr, P be a_partition of A;

      assume

       A1: P = ( Class ( LimDomRel A));

      set S1 = ( MSSign (A,P));

      let S2 be non void non empty ManySortedSign;

      given G be MSAlgebra over S2, Q be IndexedPartition of the carrier' of S2 such that

       A2: A can_be_characterized_by (S2,G,Q);

      

       A3: the Sorts of G is IndexedPartition of A by A2;

      

       A4: ( dom Q) = ( dom the charact of A) by A2;

      reconsider G as non-empty MSAlgebra over S2 by A3, MSUALG_1:def 3;

      reconsider R = the Sorts of G as IndexedPartition of A by A2;

      

       A5: ( dom R) = the carrier of S2 by PARTFUN1:def 2;

      then

      reconsider SG = the Sorts of G as Function of the carrier of S2, ( rng R) by RELSET_1: 4;

      

       A6: the carrier' of S1 = { [o, p] where o be OperSymbol of A, p be Element of (P * ) : ( product p) meets ( dom ( Den (o,A))) } by Def14;

      

       A7: the carrier of S1 = P by Def14;

      defpred Q[ object, object] means ex D1,D2 be set st D1 = $1 & D2 = $2 & D1 c= D2;

      

       A8: ( rng R) is_finer_than P by A1, Th26;

      

       A9: for r be object st r in ( rng R) holds ex p be object st p in P & Q[r, p]

      proof

        let r be object;

        assume

         A10: r in ( rng R);

        reconsider r as set by TARSKI: 1;

        ex p be set st p in P & r c= p by A10, A8;

        hence thesis;

      end;

      consider em be Function such that

       A11: ( dom em) = ( rng R) & ( rng em) c= P and

       A12: for r be object st r in ( rng R) holds Q[r, (em . r)] from FUNCT_1:sch 6( A9);

      reconsider em as Function of ( rng R), P by A11, FUNCT_2: 2;

      

       A13: for a be set st a in ( rng R) holds a c= (em . a)

      proof

        let a be set;

        assume a in ( rng R);

        then Q[a, (em . a)] by A12;

        hence thesis;

      end;

      

       A14: ( dom (em * R)) = ( dom R) by A11, RELAT_1: 27;

      ( rng (em * R)) = ( rng em) by A11, RELAT_1: 28;

      then

      reconsider f = (em * R) as Function of the carrier of S2, the carrier of S1 by A5, A7, A14, FUNCT_2: 2;

      take f;

      defpred S[ object, object] means ex p be FinSequence of P, o be OperSymbol of S2 st $2 = [(Q -index_of $1), p] & $1 = o & ( Args (o,G)) c= ( product p);

      

       A15: for s2 be object st s2 in the carrier' of S2 holds ex s1 be object st s1 in the carrier' of S1 & S[s2, s1]

      proof

        let s2 be object;

        assume s2 in the carrier' of S2;

        then

        reconsider s2 as OperSymbol of S2;

        (SG * ( the_arity_of s2)) is FinSequence of ( rng R) by Lm2;

        then

        consider p be FinSequence of P such that

         A16: ( product (SG * ( the_arity_of s2))) c= ( product p) by A1, Th3, Th26;

        reconsider p as Element of (P * ) by FINSEQ_1:def 11;

        take s1 = [(Q -index_of s2), p];

        reconsider o = (Q -index_of s2) as OperSymbol of A by A4, Def3;

        set aa = the Element of ( Args (s2,G));

        

         A17: aa in ( Args (s2,G));

        

         A18: ( dom ( Den (s2,G))) = ( Args (s2,G)) by FUNCT_2:def 1;

        

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

        

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

        (the Charact of G | (Q . o)) is IndexedPartition of ( Den (o,A)) by A2;

        then ( rng (the Charact of G | (Q . o))) is a_partition of ( Den (o,A)) by Def2;

        then

         A21: (the Charact of G .: (Q . o)) is a_partition of ( Den (o,A)) by RELAT_1: 115;

        s2 in (Q . o) by Def3;

        then (the Charact of G . s2) in (the Charact of G .: (Q . o)) by A20, FUNCT_1:def 6;

        then

         A22: ( dom ( Den (s2,G))) c= ( dom ( Den (o,A))) by A21, RELAT_1: 11;

        

         A23: ( Args (s2,G)) = ((the Sorts of G # ) . (the Arity of S2 . s2)) by A19, FUNCT_1: 13

        .= ( product (SG * ( the_arity_of s2))) by FINSEQ_2:def 5;

        then ( product p) meets ( dom ( Den (o,A))) by A16, A17, A18, A22, XBOOLE_0: 3;

        hence s1 in the carrier' of S1 by A6;

        take p, s2;

        thus thesis by A16, A23;

      end;

      consider g be Function such that

       A24: ( dom g) = the carrier' of S2 & ( rng g) c= the carrier' of S1 & for s be object st s in the carrier' of S2 holds S[s, (g . s)] from FUNCT_1:sch 6( A15);

      reconsider g as Function of the carrier' of S2, the carrier' of S1 by A24, FUNCT_2: 2;

      take g;

      thus

       A25: ( dom f) = the carrier of S2 & ( dom g) = the carrier' of S2 & ( rng f) c= the carrier of S1 & ( rng g) c= the carrier' of S1 by FUNCT_2:def 1;

      now

        let c be OperSymbol of S2;

        set s = (the ResultSort of S2 . c);

        

         A26: (R . s) = ((the Sorts of G * the ResultSort of S2) . c) by FUNCT_2: 15;

        

         A27: ((f * the ResultSort of S2) . c) = (f . s) by FUNCT_2: 15;

        (R . s) in ( rng R) by A5, FUNCT_1:def 3;

        then Q[(R . s), (em . (R . s))] by A12;

        then (R . s) c= (em . (R . s));

        then

         A28: (R . s) c= (f . s) by A5, FUNCT_1: 13;

        consider p be FinSequence of P, o be OperSymbol of S2 such that

         A29: (g . c) = [(Q -index_of c), p] and

         A30: c = o and

         A31: ( Args (o,G)) c= ( product p) by A24;

        reconsider p as Element of (P * ) by FINSEQ_1:def 11;

        reconsider s2 = (Q -index_of c) as OperSymbol of A by A4, Def3;

        set aa = the Element of ( Args (o,G));

        (the Charact of G | (Q . s2)) is IndexedPartition of ( Den (s2,A)) by A2;

        then

         A32: ( rng (the Charact of G | (Q . s2))) is a_partition of ( Den (s2,A)) by Def2;

        

         A33: o in (Q . s2) by A30, Def3;

        

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

        

         A35: (the Charact of G .: (Q . s2)) is a_partition of ( Den (s2,A)) by A32, RELAT_1: 115;

        

         A36: (the Charact of G . o) in (the Charact of G .: (Q . s2)) by A33, A34, FUNCT_1:def 6;

        

         A37: ( dom ( Den (o,G))) = ( Args (o,G)) by FUNCT_2:def 1;

        

         A38: ( dom ( Den (o,G))) c= ( dom ( Den (s2,A))) by A35, A36, RELAT_1: 11;

        aa in ( Args (o,G));

        then ( product p) meets ( dom ( Den (s2,A))) by A31, A37, A38, XBOOLE_0: 3;

        then

         A39: (( Den (s2,A)) .: ( product p)) c= (the ResultSort of S1 . (g . c)) by A29, Def14;

        ( rng ( Den (c,G))) = (( Den (c,G)) .: ( Args (c,G))) by A30, A37, RELAT_1: 113;

        then

         A40: ( rng ( Den (c,G))) c= (( Den (c,G)) .: ( product p)) by A30, A31, RELAT_1: 123;

        (( Den (c,G)) .: ( product p)) c= (( Den (s2,A)) .: ( product p)) by A30, A35, A36, RELAT_1: 124;

        then ( rng ( Den (c,G))) c= (( Den (s2,A)) .: ( product p)) by A40;

        then

         A41: ( rng ( Den (c,G))) c= (the ResultSort of S1 . (g . c)) by A39;

        

         A42: (( Den (c,G)) . aa) in ( rng ( Den (c,G))) by A30, A37, FUNCT_1:def 3;

        then

         A43: (( Den (c,G)) . aa) in ((the Sorts of G * the ResultSort of S2) . c);

        (( Den (c,G)) . aa) in (the ResultSort of S1 . (g . c)) by A41, A42;

        then (( Den (c,G)) . aa) in ((the ResultSort of S1 * g) . c) by FUNCT_2: 15;

        hence ((f * the ResultSort of S2) . c) = ((the ResultSort of S1 * g) . c) by A7, A26, A27, A28, A43, Lm3;

      end;

      hence (f * the ResultSort of S2) = (the ResultSort of S1 * g);

      hereby

        let o be set, p be Function;

        assume o in the carrier' of S2;

        then

        reconsider s = o as OperSymbol of S2;

        assume

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

        reconsider q = (the Arity of S2 . s) as Element of (the carrier of S2 * );

        reconsider r = (SG * q) as FinSequence of ( rng R) by Lm2;

        consider p9 be FinSequence of P, o9 be OperSymbol of S2 such that

         A45: (g . s) = [(Q -index_of s), p9] and

         A46: s = o9 and

         A47: ( Args (o9,G)) c= ( product p9) by A24;

        (g . s) in the carrier' of S1;

        then

        consider o1 be OperSymbol of A, p1 be Element of (P * ) such that

         A48: (g . s) = [o1, p1] and

         A49: ( product p1) meets ( dom ( Den (o1,A))) by A6;

        p9 = p1 by A45, A48, XTUPLE_0: 1;

        then

         A50: (the Arity of S1 . (g . o)) = p9 by A48, A49, Def14;

        ( Args (o9,G)) = ((the Sorts of G # ) . q) by A46, FUNCT_2: 15

        .= ( product r) by FINSEQ_2:def 5;

        then

         A51: ( product r) c= ( product p9) by A47;

        (em * r) = p9 by Th4, A51, A13;

        hence (f * p) = (the Arity of S1 . (g . o)) by A44, A50, RELAT_1: 36;

      end;

      thus ( rng f) c= the carrier of S1;

      thus the carrier of S1 c= ( rng f)

      proof

        let s be object;

        assume s in the carrier of S1;

        then

        reconsider s as Element of P by Def14;

        set a = the Element of s;

        

         A52: (R -index_of a) in ( dom R) by Def3;

        

         A53: a in (R . (R -index_of a)) by Def3;

        

         A54: (R . (R -index_of a)) in ( rng R) by A52, FUNCT_1:def 3;

        

         A55: (em . (R . (R -index_of a))) = (f . (R -index_of a)) by A52, FUNCT_1: 13;

         Q[(R . (R -index_of a)), (em . (R . (R -index_of a)))] by A12, A54;

        then

         A56: (R . (R -index_of a)) c= (f . (R -index_of a)) by A55;

        

         A57: (f . (R -index_of a)) in ( rng f) by A5, A25, A52, FUNCT_1:def 3;

        ( rng f) c= P by A25, Def14;

        hence thesis by A53, A56, A57, Lm3;

      end;

      thus ( rng g) c= the carrier' of S1;

      thus the carrier' of S1 c= ( rng g)

      proof

        let s1 be object;

        assume s1 in the carrier' of S1;

        then

        consider o be OperSymbol of A, p be Element of (P * ) such that

         A58: s1 = [o, p] and

         A59: ( product p) meets ( dom ( Den (o,A))) by A6;

        consider a be object such that

         A60: a in ( product p) and a in ( dom ( Den (o,A))) by A59, XBOOLE_0: 3;

        consider h be Function such that

         A61: a = h and

         A62: ( dom h) = ( dom p) and

         A63: for x be object st x in ( dom p) holds (h . x) in (p . x) by A60, CARD_3:def 5;

        reconsider h as FinSequence by A62, Lm1;

        ( product p) c= ( Funcs (( dom p),( Union p))) by FUNCT_6: 1;

        then

         A64: ex f be Function st h = f & ( dom f) = ( dom p) & ( rng f) c= ( Union p) by A60, A61, FUNCT_2:def 2;

        

         A65: ( Union p) = ( union ( rng p)) by CARD_3:def 4;

        

         A66: ( union ( rng p)) c= ( union P) by ZFMISC_1: 77;

        ( union P) = the carrier of A by EQREL_1:def 4;

        then ( rng h) c= the carrier of A by A64, A65, A66;

        then h is FinSequence of the carrier of A by FINSEQ_1:def 4;

        then

        consider r be FinSequence of ( rng R) such that

         A67: h in ( product r) by Th6;

        

         A68: ( dom h) = ( dom r) by A67, CARD_3: 9;

        

         A69: ( Den (o,A)) is_exactly_partitable_wrt P by Def10;

        now

          let x be object;

          assume

           A70: x in ( dom r);

          then

           A71: (h . x) in (p . x) by A62, A63, A68;

          

           A72: (h . x) in (r . x) by A67, A70, CARD_3: 9;

          

           A73: (r . x) in ( rng r) by A70, FUNCT_1:def 3;

          

           A74: (p . x) in ( rng p) by A62, A68, A70, FUNCT_1:def 3;

          ex c be set st (c in P) & ((r . x) c= c) by A8, A73;

          hence (r . x) c= (p . x) by A71, A72, A74, Lm3;

        end;

        then

         A75: ( product r) c= ( product p) by A62, A68, CARD_3: 27;

        ( product p) c= ( dom ( Den (o,A))) by A59, A69;

        then

        consider s2 be OperSymbol of S2 such that

         A76: (the Sorts of G * ( the_arity_of s2)) = r and

         A77: s2 in (Q . o) by A2, A75, Th31, XBOOLE_1: 1;

        consider p9 be FinSequence of P, o9 be OperSymbol of S2 such that

         A78: (g . s2) = [(Q -index_of s2), p9] and

         A79: s2 = o9 and

         A80: ( Args (o9,G)) c= ( product p9) by A24;

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

        

        then ( Args (s2,G)) = ((the Sorts of G # ) . (the Arity of S2 . s2)) by FUNCT_1: 13

        .= ( product r) by A76, FINSEQ_2:def 5;

        then

         A81: p9 = (em * r) by A13, A79, A80, Th4;

        

         A82: p = (em * r) by A13, A75, Th4;

        (Q -index_of s2) = o by A4, A77, Def3;

        hence thesis by A24, A58, A78, A81, A82, FUNCT_1:def 3;

      end;

    end;