pralg_1.miz



    begin

    reserve U1,U2,U3 for Universal_Algebra,

n,m for Nat,

x,y,z for object,

A,B for non empty set,

h1 for FinSequence of [:A, B:];

    definition

      let A, B, h1;

      :: original: pr1

      redefine

      :: PRALG_1:def1

      func pr1 h1 -> FinSequence of A means

      : Def1: ( len it ) = ( len h1) & for n st n in ( dom it ) holds (it . n) = ((h1 . n) `1 );

      compatibility

      proof

        let f1 be FinSequence of A;

        hereby

          assume

           A1: f1 = ( pr1 h1);

          then

           A2: ( dom f1) = ( dom h1) by MCART_1:def 12;

          hence ( len f1) = ( len h1) by FINSEQ_3: 29;

          let n;

          thus n in ( dom f1) implies (f1 . n) = ((h1 . n) `1 ) by A1, A2, MCART_1:def 12;

        end;

        assume ( len f1) = ( len h1) & for n st n in ( dom f1) holds (f1 . n) = ((h1 . n) `1 );

        then ( dom f1) = ( dom h1) & for n be object st n in ( dom f1) holds (f1 . n) = ((h1 . n) `1 ) by FINSEQ_3: 29;

        hence thesis by MCART_1:def 12;

      end;

      coherence

      proof

        thus ( pr1 h1) is FinSequence of A;

      end;

      :: original: pr2

      redefine

      :: PRALG_1:def2

      func pr2 h1 -> FinSequence of B means

      : Def2: ( len it ) = ( len h1) & for n st n in ( dom it ) holds (it . n) = ((h1 . n) `2 );

      compatibility

      proof

        let f1 be FinSequence of B;

        hereby

          assume

           A3: f1 = ( pr2 h1);

          then

           A4: ( dom f1) = ( dom h1) by MCART_1:def 13;

          hence ( len f1) = ( len h1) by FINSEQ_3: 29;

          let n;

          thus n in ( dom f1) implies (f1 . n) = ((h1 . n) `2 ) by A3, A4, MCART_1:def 13;

        end;

        assume ( len f1) = ( len h1) & for n st n in ( dom f1) holds (f1 . n) = ((h1 . n) `2 );

        then ( dom f1) = ( dom h1) & for n be object st n in ( dom f1) holds (f1 . n) = ((h1 . n) `2 ) by FINSEQ_3: 29;

        hence thesis by MCART_1:def 13;

      end;

      coherence

      proof

        thus ( pr2 h1) is FinSequence of B;

      end;

    end

    definition

      let A, B;

      let f1 be homogeneous quasi_total non empty PartFunc of (A * ), A;

      let f2 be homogeneous quasi_total non empty PartFunc of (B * ), B;

      assume

       A1: ( arity f1) = ( arity f2);

      :: PRALG_1:def3

      func [[:f1,f2:]] -> homogeneous quasi_total non empty PartFunc of ( [:A, B:] * ), [:A, B:] means

      : Def3: ( dom it ) = (( arity f1) -tuples_on [:A, B:]) & for h be FinSequence of [:A, B:] st h in ( dom it ) holds (it . h) = [(f1 . ( pr1 h)), (f2 . ( pr2 h))];

      existence

      proof

        set ar = (( arity f1) -tuples_on [:A, B:]), ab = { s where s be Element of ( [:A, B:] * ) : ( len s) = ( arity f1) };

        defpred P[ object, object] means for h be FinSequence of [:A, B:] st $1 = h holds $2 = [(f1 . ( pr1 h)), (f2 . ( pr2 h))];

        

         A2: ( dom f2) = (( arity f2) -tuples_on B) by MARGREL1: 22;

        

         A3: ( rng f1) c= A & ( rng f2) c= B by RELAT_1:def 19;

        

         A4: ( dom f1) = (( arity f1) -tuples_on A) by MARGREL1: 22;

        

         A5: for x,y be object st x in ar & P[x, y] holds y in [:A, B:]

        proof

          let x,y be object;

          assume that

           A6: x in ar and

           A7: P[x, y];

          consider s be Element of ( [:A, B:] * ) such that

           A8: x = s and

           A9: ( len s) = ( arity f1) by A6;

          reconsider s1 = ( pr1 s) as Element of (A * ) by FINSEQ_1:def 11;

          ( len ( pr1 s)) = ( len s) by Def1;

          then s1 in { s3 where s3 be Element of (A * ) : ( len s3) = ( arity f1) } by A9;

          then

           A10: (f1 . s1) in ( rng f1) by A4, FUNCT_1:def 3;

          reconsider s2 = ( pr2 s) as Element of (B * ) by FINSEQ_1:def 11;

          ( len ( pr2 s)) = ( len s) by Def2;

          then s2 in { s3 where s3 be Element of (B * ) : ( len s3) = ( arity f2) } by A1, A9;

          then

           A11: (f2 . s2) in ( rng f2) by A2, FUNCT_1:def 3;

          y = [(f1 . ( pr1 s)), (f2 . ( pr2 s))] by A7, A8;

          hence thesis by A3, A10, A11, ZFMISC_1: 87;

        end;

        

         A12: for x,y,z be object st x in ar & P[x, y] & P[x, z] holds y = z

        proof

          let x,y,z be object;

          assume that

           A13: x in ar and

           A14: P[x, y] and

           A15: P[x, z];

          consider s be Element of ( [:A, B:] * ) such that

           A16: x = s and ( len s) = ( arity f1) by A13;

          y = [(f1 . ( pr1 s)), (f2 . ( pr2 s))] by A14, A16;

          hence thesis by A15, A16;

        end;

        consider f be PartFunc of ar, [:A, B:] such that

         A17: for x be object holds x in ( dom f) iff x in ar & ex y be object st P[x, y] and

         A18: for x be object st x in ( dom f) holds P[x, (f . x)] from PARTFUN1:sch 2( A5, A12);

        

         A19: ( dom f) = ar

        proof

          thus ( dom f) c= ar by A17;

          let x be object;

          assume

           A20: x in ar;

          then

          consider s be Element of ( [:A, B:] * ) such that

           A21: x = s and ( len s) = ( arity f1);

          now

            take y = [(f1 . ( pr1 s)), (f2 . ( pr2 s))];

            let h be FinSequence of [:A, B:];

            assume h = x;

            hence y = [(f1 . ( pr1 h)), (f2 . ( pr2 h))] by A21;

          end;

          hence thesis by A17, A20;

        end;

        ar in the set of all (i -tuples_on [:A, B:]) where i be Nat;

        then ar c= ( union the set of all (i -tuples_on [:A, B:]) where i be Nat) by ZFMISC_1: 74;

        then ar c= ( [:A, B:] * ) by FINSEQ_2: 108;

        then

        reconsider f as PartFunc of ( [:A, B:] * ), [:A, B:] by RELSET_1: 7;

        

         A22: f is quasi_total

        proof

          let x,y be FinSequence of [:A, B:];

          assume that

           A23: ( len x) = ( len y) and

           A24: x in ( dom f);

          reconsider y9 = y as Element of ( [:A, B:] * ) by FINSEQ_1:def 11;

          ex s1 be Element of ( [:A, B:] * ) st s1 = x & ( len s1) = ( arity f1) by A19, A24;

          then y9 in ab by A23;

          hence thesis by A19;

        end;

        f is homogeneous

        proof

          let x,y be FinSequence;

          assume x in ( dom f) & y in ( dom f);

          then (ex s1 be Element of ( [:A, B:] * ) st s1 = x & ( len s1) = ( arity f1)) & ex s2 be Element of ( [:A, B:] * ) st s2 = y & ( len s2) = ( arity f1) by A19;

          hence thesis;

        end;

        then

        reconsider f as homogeneous quasi_total non empty PartFunc of ( [:A, B:] * ), [:A, B:] by A19, A22;

        take f;

        thus ( dom f) = ar by A19;

        let h be FinSequence of [:A, B:];

        assume h in ( dom f);

        hence thesis by A18;

      end;

      uniqueness

      proof

        let x,y be homogeneous quasi_total non empty PartFunc of ( [:A, B:] * ), [:A, B:];

        assume that

         A25: ( dom x) = (( arity f1) -tuples_on [:A, B:]) and

         A26: for h be FinSequence of [:A, B:] st h in ( dom x) holds (x . h) = [(f1 . ( pr1 h)), (f2 . ( pr2 h))] and

         A27: ( dom y) = (( arity f1) -tuples_on [:A, B:]) and

         A28: for h be FinSequence of [:A, B:] st h in ( dom y) holds (y . h) = [(f1 . ( pr1 h)), (f2 . ( pr2 h))];

        now

          let c be Element of ( [:A, B:] * );

          reconsider c9 = c as FinSequence of [:A, B:];

          assume

           A29: c in ( dom x);

          then (x . c9) = [(f1 . ( pr1 c9)), (f2 . ( pr2 c9))] by A26;

          hence (x . c) = (y . c) by A25, A27, A28, A29;

        end;

        hence thesis by A25, A27, PARTFUN1: 5;

      end;

    end

    reserve h1 for homogeneous quasi_total non empty PartFunc of (the carrier of U1 * ), the carrier of U1,

h2 for homogeneous quasi_total non empty PartFunc of (the carrier of U2 * ), the carrier of U2;

    definition

      let U1, U2;

      assume

       A1: (U1,U2) are_similar ;

      :: PRALG_1:def4

      func Opers (U1,U2) -> PFuncFinSequence of [:the carrier of U1, the carrier of U2:] means

      : Def4: ( len it ) = ( len the charact of U1) & for n st n in ( dom it ) holds for h1, h2 st h1 = (the charact of U1 . n) & h2 = (the charact of U2 . n) holds (it . n) = [[:h1, h2:]];

      existence

      proof

        defpred P[ Nat, set] means for h1, h2 st h1 = (the charact of U1 . $1) & h2 = (the charact of U2 . $1) holds $2 = [[:h1, h2:]];

        set l = ( len the charact of U1), c = [:the carrier of U1, the carrier of U2:];

        

         A2: ( dom the charact of U2) = ( Seg ( len the charact of U2)) by FINSEQ_1:def 3;

        

         A3: ( Seg l) = ( dom the charact of U1) by FINSEQ_1:def 3;

        

         A4: for m be Nat st m in ( Seg l) holds ex x be Element of ( PFuncs ((c * ),c)) st P[m, x]

        proof

          let m be Nat;

          assume

           A5: m in ( Seg l);

          then

          reconsider f1 = (the charact of U1 . m) as homogeneous quasi_total non empty PartFunc of (the carrier of U1 * ), the carrier of U1 by A3, MARGREL1:def 24;

          ( len the charact of U1) = ( len the charact of U2) by A1, UNIALG_2: 1;

          then

          reconsider f2 = (the charact of U2 . m) as homogeneous quasi_total non empty PartFunc of (the carrier of U2 * ), the carrier of U2 by A2, A5, MARGREL1:def 24;

          reconsider F = [[:f1, f2:]] as Element of ( PFuncs ((c * ),c)) by PARTFUN1: 45;

          take F;

          let h1, h2;

          assume h1 = (the charact of U1 . m) & h2 = (the charact of U2 . m);

          hence thesis;

        end;

        consider p be FinSequence of ( PFuncs ((c * ),c)) such that

         A6: ( dom p) = ( Seg l) and

         A7: for m be Nat st m in ( Seg l) holds P[m, (p . m)] from FINSEQ_1:sch 5( A4);

        reconsider p as PFuncFinSequence of c;

        take p;

        thus ( len p) = ( len the charact of U1) by A6, FINSEQ_1:def 3;

        let n;

        assume n in ( dom p);

        hence thesis by A6, A7;

      end;

      uniqueness

      proof

        let x,y be PFuncFinSequence of [:the carrier of U1, the carrier of U2:];

        assume that

         A8: ( len x) = ( len the charact of U1) and

         A9: for n st n in ( dom x) holds for h1, h2 st h1 = (the charact of U1 . n) & h2 = (the charact of U2 . n) holds (x . n) = [[:h1, h2:]] and

         A10: ( len y) = ( len the charact of U1) and

         A11: for n st n in ( dom y) holds for h1, h2 st h1 = (the charact of U1 . n) & h2 = (the charact of U2 . n) holds (y . n) = [[:h1, h2:]];

        

         A12: ( dom x) = ( Seg ( len the charact of U1)) by A8, FINSEQ_1:def 3;

        now

          let m be Nat;

          assume

           A13: m in ( dom x);

          then m in ( dom the charact of U1) by A12, FINSEQ_1:def 3;

          then

          reconsider h1 = (the charact of U1 . m) as homogeneous quasi_total non empty PartFunc of (the carrier of U1 * ), the carrier of U1 by MARGREL1:def 24;

          ( Seg ( len the charact of U2)) = ( Seg ( len the charact of U1)) by A1, UNIALG_2: 1;

          then m in ( dom the charact of U2) by A12, A13, FINSEQ_1:def 3;

          then

          reconsider h2 = (the charact of U2 . m) as homogeneous quasi_total non empty PartFunc of (the carrier of U2 * ), the carrier of U2 by MARGREL1:def 24;

          m in ( dom y) & (x . m) = [[:h1, h2:]] by A9, A10, A12, A13, FINSEQ_1:def 3;

          hence (x . m) = (y . m) by A11;

        end;

        hence thesis by A8, A10, FINSEQ_2: 9;

      end;

    end

    theorem :: PRALG_1:1

    

     Th1: (U1,U2) are_similar implies UAStr (# [:the carrier of U1, the carrier of U2:], ( Opers (U1,U2)) #) is strict Universal_Algebra

    proof

      set C = UAStr (# [:the carrier of U1, the carrier of U2:], ( Opers (U1,U2)) #);

      

       A1: ( dom ( Opers (U1,U2))) = ( Seg ( len ( Opers (U1,U2)))) by FINSEQ_1:def 3;

      assume

       A2: (U1,U2) are_similar ;

      then

       A3: ( dom the charact of U2) = ( Seg ( len the charact of U2)) & ( len the charact of U2) = ( len the charact of U1) by FINSEQ_1:def 3, UNIALG_2: 1;

      

       A4: ( len ( Opers (U1,U2))) = ( len the charact of U1) by A2, Def4;

      

       A5: ( dom the charact of U1) = ( Seg ( len the charact of U1)) by FINSEQ_1:def 3;

      

       A6: the charact of C is quasi_total

      proof

        let n;

        let h be PartFunc of (the carrier of C * ), the carrier of C;

        assume that

         A7: n in ( dom the charact of C) and

         A8: h = (the charact of C . n);

        reconsider h2 = (the charact of U2 . n) as homogeneous quasi_total non empty PartFunc of (the carrier of U2 * ), the carrier of U2 by A1, A4, A3, A7, MARGREL1:def 24;

        reconsider h1 = (the charact of U1 . n) as homogeneous quasi_total non empty PartFunc of (the carrier of U1 * ), the carrier of U1 by A1, A5, A4, A7, MARGREL1:def 24;

        h = [[:h1, h2:]] by A2, A7, A8, Def4;

        hence thesis;

      end;

      

       A9: the charact of C is non-empty

      proof

        let n be object;

        set h = (the charact of C . n);

        assume

         A10: n in ( dom the charact of C);

        then

        reconsider m = n as Element of NAT ;

        reconsider h2 = (the charact of U2 . m) as homogeneous quasi_total non empty PartFunc of (the carrier of U2 * ), the carrier of U2 by A1, A4, A3, A10, MARGREL1:def 24;

        reconsider h1 = (the charact of U1 . m) as homogeneous quasi_total non empty PartFunc of (the carrier of U1 * ), the carrier of U1 by A1, A5, A4, A10, MARGREL1:def 24;

        h = [[:h1, h2:]] by A2, A10, Def4;

        hence thesis;

      end;

      

       A11: the charact of C is homogeneous

      proof

        let n;

        let h be PartFunc of (the carrier of C * ), the carrier of C;

        assume that

         A12: n in ( dom the charact of C) and

         A13: h = (the charact of C . n);

        reconsider h2 = (the charact of U2 . n) as homogeneous quasi_total non empty PartFunc of (the carrier of U2 * ), the carrier of U2 by A1, A4, A3, A12, MARGREL1:def 24;

        reconsider h1 = (the charact of U1 . n) as homogeneous quasi_total non empty PartFunc of (the carrier of U1 * ), the carrier of U1 by A1, A5, A4, A12, MARGREL1:def 24;

        h = [[:h1, h2:]] by A2, A12, A13, Def4;

        hence thesis;

      end;

      the charact of C <> {} by A4;

      hence thesis by A6, A11, A9, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;

    end;

    definition

      let U1, U2;

      assume

       A1: (U1,U2) are_similar ;

      :: PRALG_1:def5

      func [:U1,U2:] -> strict Universal_Algebra equals

      : Def5: UAStr (# [:the carrier of U1, the carrier of U2:], ( Opers (U1,U2)) #);

      coherence by A1, Th1;

    end

    definition

      let A,B be non empty set;

      :: PRALG_1:def6

      func Inv (A,B) -> Function of [:A, B:], [:B, A:] means

      : Def6: for a be Element of [:A, B:] holds (it . a) = [(a `2 ), (a `1 )];

      existence

      proof

        deffunc F( Element of [:A, B:]) = [($1 `2 ), ($1 `1 )];

        thus ex I be Function of [:A, B:], [:B, A:] st for a be Element of [:A, B:] holds (I . a) = F(a) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        let f,g be Function of [:A, B:], [:B, A:];

        assume that

         A1: for a be Element of [:A, B:] holds (f . a) = [(a `2 ), (a `1 )] and

         A2: for a be Element of [:A, B:] holds (g . a) = [(a `2 ), (a `1 )];

        now

          let a be Element of [:A, B:];

          (f . a) = [(a `2 ), (a `1 )] by A1;

          hence (f . a) = (g . a) by A2;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: PRALG_1:2

    for A,B be non empty set holds ( rng ( Inv (A,B))) = [:B, A:]

    proof

      let A,B be non empty set;

      thus ( rng ( Inv (A,B))) c= [:B, A:];

      let x be object;

      

       A1: ( dom ( Inv (A,B))) = [:A, B:] by FUNCT_2:def 1;

      assume x in [:B, A:];

      then

      reconsider y = x as Element of [:B, A:];

      (( Inv (A,B)) . [(y `2 ), (y `1 )]) = [( [(y `2 ), (y `1 )] `2 ), ( [(y `2 ), (y `1 )] `1 )] by Def6

      .= [(y `1 ), ( [(y `2 ), (y `1 )] `1 )]

      .= [(y `1 ), (y `2 )]

      .= y by MCART_1: 21;

      hence thesis by A1, FUNCT_1:def 3;

    end;

    theorem :: PRALG_1:3

    for A,B be non empty set holds ( Inv (A,B)) is one-to-one

    proof

      let A,B be non empty set;

      let x,y be object;

      assume that

       A1: x in ( dom ( Inv (A,B))) & y in ( dom ( Inv (A,B))) and

       A2: (( Inv (A,B)) . x) = (( Inv (A,B)) . y);

      reconsider x1 = x, y1 = y as Element of [:A, B:] by A1, FUNCT_2:def 1;

      (( Inv (A,B)) . x1) = [(x1 `2 ), (x1 `1 )] & (( Inv (A,B)) . y1) = [(y1 `2 ), (y1 `1 )] by Def6;

      then (x1 `1 ) = (y1 `1 ) & (x1 `2 ) = (y1 `2 ) by A2, XTUPLE_0: 1;

      hence thesis by DOMAIN_1: 2;

    end;

    theorem :: PRALG_1:4

    (U1,U2) are_similar implies ( Inv (the carrier of U1,the carrier of U2)) is Function of the carrier of [:U1, U2:], the carrier of [:U2, U1:]

    proof

      assume (U1,U2) are_similar ;

      then [:U1, U2:] = UAStr (# [:the carrier of U1, the carrier of U2:], ( Opers (U1,U2)) #) & [:U2, U1:] = UAStr (# [:the carrier of U2, the carrier of U1:], ( Opers (U2,U1)) #) by Def5;

      hence thesis;

    end;

    theorem :: PRALG_1:5

    

     Th5: (U1,U2) are_similar implies for o1 be operation of U1, o2 be operation of U2, o be operation of [:U1, U2:], n be Nat st o1 = (the charact of U1 . n) & o2 = (the charact of U2 . n) & o = (the charact of [:U1, U2:] . n) & n in ( dom the charact of U1) holds ( arity o) = ( arity o1) & ( arity o) = ( arity o2) & o = [[:o1, o2:]]

    proof

      assume

       A1: (U1,U2) are_similar ;

      

       A2: ( dom ( Opers (U1,U2))) = ( Seg ( len ( Opers (U1,U2)))) by FINSEQ_1:def 3;

      

       A3: ( dom the charact of U1) = ( Seg ( len the charact of U1)) by FINSEQ_1:def 3;

      let o1 be operation of U1, o2 be operation of U2, o be operation of [:U1, U2:], n be Nat;

      assume that

       A4: o1 = (the charact of U1 . n) and

       A5: o2 = (the charact of U2 . n) and

       A6: o = (the charact of [:U1, U2:] . n) and

       A7: n in ( dom the charact of U1);

      

       A8: ( dom ( signature U1)) = ( Seg ( len ( signature U1))) & ( len ( signature U1)) = ( len the charact of U1) by FINSEQ_1:def 3, UNIALG_1:def 4;

      then

       A9: (( signature U1) . n) = ( arity o1) by A4, A7, A3, UNIALG_1:def 4;

      

       A10: ( signature U1) = ( signature U2) by A1;

      then

       A11: (( signature U2) . n) = ( arity o2) by A5, A7, A3, A8, UNIALG_1:def 4;

      

       A12: [:U1, U2:] = UAStr (# [:the carrier of U1, the carrier of U2:], ( Opers (U1,U2)) #) & ( len the charact of U1) = ( len ( Opers (U1,U2))) by A1, Def4, Def5;

      then o = [[:o1, o2:]] by A1, A4, A5, A6, A7, A3, A2, Def4;

      then

       A13: ( dom o) = (( arity o1) -tuples_on [:the carrier of U1, the carrier of U2:]) by A10, A9, A11, Def3;

      (ex x be FinSequence st x in ( dom o)) & for x be FinSequence st x in ( dom o) holds ( len x) = ( arity o1)

      proof

        set a = the Element of (( arity o1) -tuples_on [:the carrier of U1, the carrier of U2:]);

        a in ( dom o) by A13;

        hence ex x be FinSequence st x in ( dom o);

        let x be FinSequence;

        assume x in ( dom o);

        then ex s be Element of ( [:the carrier of U1, the carrier of U2:] * ) st s = x & ( len s) = ( arity o1) by A13;

        hence thesis;

      end;

      hence thesis by A1, A4, A5, A6, A7, A3, A2, A12, A9, A11, Def4, MARGREL1:def 25;

    end;

    theorem :: PRALG_1:6

    (U1,U2) are_similar implies ( [:U1, U2:],U1) are_similar

    proof

      

       A1: ( dom ( signature U1)) = ( Seg ( len ( signature U1))) by FINSEQ_1:def 3;

      

       A2: ( dom ( signature U1)) = ( Seg ( len ( signature U1))) by FINSEQ_1:def 3;

      

       A3: ( dom the charact of [:U1, U2:]) = ( Seg ( len the charact of [:U1, U2:])) by FINSEQ_1:def 3;

      

       A4: ( dom the charact of U2) = ( Seg ( len the charact of U2)) by FINSEQ_1:def 3;

      

       A5: ( dom the charact of U1) = ( Seg ( len the charact of U1)) by FINSEQ_1:def 3;

      assume

       A6: (U1,U2) are_similar ;

      then [:U1, U2:] = UAStr (# [:the carrier of U1, the carrier of U2:], ( Opers (U1,U2)) #) by Def5;

      then ( len the charact of [:U1, U2:]) = ( len the charact of U1) by A6, Def4;

      

      then

       A7: ( len ( signature [:U1, U2:])) = ( len the charact of U1) by UNIALG_1:def 4

      .= ( len ( signature U1)) by UNIALG_1:def 4;

      

       A8: ( dom ( signature [:U1, U2:])) = ( Seg ( len ( signature [:U1, U2:]))) by FINSEQ_1:def 3;

      now

        let n be Nat;

        assume

         A9: n in ( dom ( signature U1));

        then n in ( dom the charact of [:U1, U2:]) by A7, A1, A3, UNIALG_1:def 4;

        then

        reconsider o12 = (the charact of [:U1, U2:] . n) as operation of [:U1, U2:] by FUNCT_1:def 3;

        ( len ( signature U1)) = ( len ( signature U2)) by A6

        .= ( len the charact of U2) by UNIALG_1:def 4;

        then

        reconsider o2 = (the charact of U2 . n) as operation of U2 by A1, A4, A9, FUNCT_1:def 3;

        

         A10: o2 = (the charact of U2 . n);

        

         A11: n in ( Seg ( len the charact of U1)) by A2, A9, UNIALG_1:def 4;

        then n in ( dom the charact of U1) by FINSEQ_1:def 3;

        then

        reconsider o1 = (the charact of U1 . n) as operation of U1 by FUNCT_1:def 3;

        (( signature U1) . n) = ( arity o1) & (( signature [:U1, U2:]) . n) = ( arity o12) by A7, A1, A8, A9, UNIALG_1:def 4;

        hence (( signature U1) . n) = (( signature [:U1, U2:]) . n) by A6, A5, A11, A10, Th5;

      end;

      hence thesis by A7, FINSEQ_2: 9;

    end;

    theorem :: PRALG_1:7

    for U1,U2,U3,U4 be Universal_Algebra st U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & (U2,U4) are_similar holds [:U1, U3:] is SubAlgebra of [:U2, U4:]

    proof

      let U1,U2,U3,U4 be Universal_Algebra;

      assume that

       A1: U1 is SubAlgebra of U2 and

       A2: U3 is SubAlgebra of U4 and

       A3: (U2,U4) are_similar ;

      

       A4: [:U2, U4:] = UAStr (# [:the carrier of U2, the carrier of U4:], ( Opers (U2,U4)) #) by A3, Def5;

      

       A5: (U1,U2) are_similar by A1, UNIALG_2: 13;

      then

       A6: (U1,U4) are_similar by A3;

      

       A7: (U3,U4) are_similar by A2, UNIALG_2: 13;

      then

       A8: [:U1, U3:] = UAStr (# [:the carrier of U1, the carrier of U3:], ( Opers (U1,U3)) #) by A6, Def5, UNIALG_2: 2;

      

       A9: the carrier of U1 is Subset of U2 & the carrier of U3 is Subset of U4 by A1, A2, UNIALG_2:def 7;

      hence the carrier of [:U1, U3:] is Subset of [:U2, U4:] by A8, A4, ZFMISC_1: 96;

      let B be non empty Subset of [:U2, U4:];

      assume

       A10: B = the carrier of [:U1, U3:];

      ( len the charact of U4) = ( len ( signature U2)) by UNIALG_1:def 4, A3;

      then

       A11: ( dom the charact of U4) = ( Seg ( len the charact of U4)) & ( len the charact of U4) = ( len the charact of U2) by FINSEQ_1:def 3, UNIALG_1:def 4;

      

       A12: ( dom the charact of U1) = ( Seg ( len the charact of U1)) by FINSEQ_1:def 3;

      

       A13: ( dom the charact of U2) = ( Seg ( len the charact of U2)) by FINSEQ_1:def 3;

      

       A14: (U1,U3) are_similar by A7, A6;

      then

       A15: ( len the charact of [:U1, U3:]) = ( len the charact of U1) by A8, Def4;

      ( len the charact of U1) = ( len ( signature U3)) by UNIALG_1:def 4, A14;

      then

       A16: ( dom the charact of U3) = ( Seg ( len the charact of U3)) & ( len the charact of U1) = ( len the charact of U3) by FINSEQ_1:def 3, UNIALG_1:def 4;

      

       A17: ( dom ( Opers ( [:U2, U4:],B))) = ( Seg ( len ( Opers ( [:U2, U4:],B)))) by FINSEQ_1:def 3;

      

       A18: ( dom the charact of [:U2, U4:]) = ( dom ( Opers ( [:U2, U4:],B))) by UNIALG_2:def 6;

      then ( len the charact of [:U2, U4:]) = ( len ( Opers ( [:U2, U4:],B))) by FINSEQ_3: 29;

      then

       A19: ( len the charact of U2) = ( len ( Opers ( [:U2, U4:],B))) by A3, A4, Def4;

      ( len the charact of U1) = ( len ( signature U2)) by UNIALG_1:def 4, A5;

      then

       A20: ( len the charact of [:U1, U3:]) = ( len ( Opers ( [:U2, U4:],B))) by A19, A15, UNIALG_1:def 4;

      reconsider B3 = the carrier of U3 as non empty Subset of U4 by A2, UNIALG_2:def 7;

      

       A21: B3 is opers_closed by A2, UNIALG_2:def 7;

      reconsider B1 = the carrier of U1 as non empty Subset of U2 by A1, UNIALG_2:def 7;

      

       A22: B1 is opers_closed by A1, UNIALG_2:def 7;

      

       A23: [:the carrier of U1, the carrier of U3:] c= [:the carrier of U2, the carrier of U4:] by A9, ZFMISC_1: 96;

      

       A24: for o be operation of [:U2, U4:] holds B is_closed_on o

      proof

        let o be operation of [:U2, U4:];

        let s be FinSequence of B;

        reconsider s0 = s as Element of ( [:the carrier of U1, the carrier of U3:] * ) by A8, A10, FINSEQ_1:def 11;

        consider n be Nat such that

         A25: n in ( dom the charact of [:U2, U4:]) and

         A26: (the charact of [:U2, U4:] . n) = o by FINSEQ_2: 10;

        reconsider s3 = ( pr2 s0) as Element of (B3 * ) by FINSEQ_1:def 11;

        reconsider s1 = ( pr1 s0) as Element of (B1 * ) by FINSEQ_1:def 11;

        

         A27: ( len the charact of [:U2, U4:]) = ( len the charact of U2) by A3, A4, Def4;

        

         A28: n in ( Seg ( len the charact of [:U2, U4:])) by A25, FINSEQ_1:def 3;

        then

         A29: n in ( dom the charact of U2) by A27, FINSEQ_1:def 3;

        then

        reconsider o2 = (the charact of U2 . n) as operation of U2 by FUNCT_1:def 3;

        ( len the charact of U4) = ( len the charact of U2) by A3, UNIALG_2: 1;

        then n in ( dom the charact of U4) by A28, A27, FINSEQ_1:def 3;

        then

        reconsider o4 = (the charact of U4 . n) as operation of U4 by FUNCT_1:def 3;

        

         A30: o = [[:o2, o4:]] by A3, A26, A29, Th5;

        o4 = (the charact of U4 . n);

        then

         A31: ( arity o) = ( arity o2) by A3, A26, A29, Th5;

        ( rng s0) c= [:the carrier of U1, the carrier of U3:] by FINSEQ_1:def 4;

        then ( rng s0) c= [:the carrier of U2, the carrier of U4:] by A23;

        then s0 is FinSequence of [:the carrier of U2, the carrier of U4:] by FINSEQ_1:def 4;

        then

        reconsider ss = s0 as Element of ( [:the carrier of U2, the carrier of U4:] * ) by FINSEQ_1:def 11;

        o2 = (the charact of U2 . n);

        then

         A32: ( arity o) = ( arity o4) by A3, A26, A29, Th5;

        assume

         A33: ( len s) = ( arity o);

        then

         A34: ss in { w where w be Element of ( [:the carrier of U2, the carrier of U4:] * ) : ( len w) = ( arity o2) } by A31;

        B3 is_closed_on o4 & ( len s3) = ( len s0) by A21, Def2;

        then

         A35: (o4 . s3) in B3 by A33, A32;

        B1 is_closed_on o2 & ( len s1) = ( len s0) by A22, Def1;

        then

         A36: (o2 . s1) in B1 by A33, A31;

        ( dom [[:o2, o4:]]) = (( arity o2) -tuples_on [:the carrier of U2, the carrier of U4:]) by A31, A32, Def3;

        then (o . s) = [(o2 . ( pr1 ss)), (o4 . ( pr2 ss))] by A31, A32, A30, A34, Def3;

        hence thesis by A8, A10, A36, A35, ZFMISC_1: 87;

      end;

      

       A37: ( dom the charact of U4) = ( dom ( Opers (U4,B3))) by UNIALG_2:def 6;

      

       A38: ( dom the charact of [:U1, U3:]) = ( Seg ( len the charact of [:U1, U3:])) by FINSEQ_1:def 3;

      

       A39: ( dom the charact of U2) = ( dom ( Opers (U2,B1))) by UNIALG_2:def 6;

      for n be Nat st n in ( dom the charact of [:U1, U3:]) holds (the charact of [:U1, U3:] . n) = (( Opers ( [:U2, U4:],B)) . n)

      proof

        let n be Nat;

        assume

         A40: n in ( dom the charact of [:U1, U3:]);

        then

        reconsider o2 = (the charact of U2 . n) as operation of U2 by A19, A20, A13, A38, FUNCT_1:def 3;

        reconsider o4 = (the charact of U4 . n) as operation of U4 by A19, A20, A38, A11, A40, FUNCT_1:def 3;

        reconsider o24 = (the charact of [:U2, U4:] . n) as operation of [:U2, U4:] by A18, A20, A38, A17, A40, FUNCT_1:def 3;

        

         A41: o24 = [[:o2, o4:]] by A3, A19, A20, A13, A38, A40, Th5;

        reconsider o3 = (the charact of U3 . n) as operation of U3 by A15, A38, A16, A40, FUNCT_1:def 3;

        (( Opers (U4,B3)) . n) = (o4 /. B3) by A19, A20, A38, A11, A37, A40, UNIALG_2:def 6;

        then

         A42: o3 = (o4 /. B3) by A2, UNIALG_2:def 7;

        o2 = (the charact of U2 . n);

        then

         A43: ( arity o24) = ( arity o4) by A3, A19, A20, A13, A38, A40, Th5;

        reconsider o1 = (the charact of U1 . n) as operation of U1 by A15, A12, A38, A40, FUNCT_1:def 3;

        (( Opers (U2,B1)) . n) = (o2 /. B1) by A19, A20, A13, A38, A39, A40, UNIALG_2:def 6;

        then

         A44: o1 = (o2 /. B1) by A1, UNIALG_2:def 7;

        

         A45: B3 is_closed_on o4 by A21;

        then

         A46: ( arity (o4 /. B3)) = ( arity o4) by UNIALG_2: 5;

        o4 = (the charact of U4 . n);

        then

         A47: ( arity o24) = ( arity o2) by A3, A19, A20, A13, A38, A40, Th5;

        

        then

         A48: ( dom ( [[:o2, o4:]] | (( arity o24) -tuples_on B))) = (( dom [[:o2, o4:]]) /\ (( arity o2) -tuples_on B)) by RELAT_1: 61

        .= ((( arity o2) -tuples_on the carrier of [:U2, U4:]) /\ (( arity o2) -tuples_on B)) by A4, A43, A47, Def3

        .= (( arity o2) -tuples_on B) by MARGREL1: 21;

        

         A49: B1 is_closed_on o2 by A22;

        then

         A50: ( arity (o2 /. B1)) = ( arity o2) by UNIALG_2: 5;

        then

         A51: ( dom [[:(o2 /. B1), (o4 /. B3):]]) = (( arity o2) -tuples_on B) by A8, A10, A43, A47, A46, Def3;

         A52:

        now

          let x be object;

          

           A53: ( dom ( [[:o2, o4:]] | (( arity o24) -tuples_on B))) c= ( dom [[:o2, o4:]]) by RELAT_1: 60;

          assume

           A54: x in (( arity o2) -tuples_on B);

          then

          consider s be Element of (B * ) such that

           A55: s = x and

           A56: ( len s) = ( arity o2);

          ( rng s) c= B by FINSEQ_1:def 4;

          then ( rng s) c= [:the carrier of U2, the carrier of U4:] by A4, XBOOLE_1: 1;

          then

          reconsider s0 = s as FinSequence of [:the carrier of U2, the carrier of U4:] by FINSEQ_1:def 4;

          

           A57: (( [[:o2, o4:]] | (( arity o24) -tuples_on B)) . x) = ( [[:o2, o4:]] . s0) by A48, A54, A55, FUNCT_1: 47

          .= [(o2 . ( pr1 s0)), (o4 . ( pr2 s0))] by A43, A47, A48, A54, A55, A53, Def3;

          reconsider s1 = s as FinSequence of [:B1 qua non empty set, B3 qua non empty set:] by A8, A10;

          reconsider s11 = ( pr1 s1) as Element of (B1 * ) by FINSEQ_1:def 11;

          ( len ( pr1 s1)) = ( len s1) by Def1;

          then

           A58: s11 in { a where a be Element of (B1 * ) : ( len a) = ( arity o2) } by A56;

          reconsider s12 = ( pr2 s1) as Element of (B3 * ) by FINSEQ_1:def 11;

          ( len ( pr2 s1)) = ( len s1) by Def2;

          then

           A59: s12 in { b where b be Element of (B3 * ) : ( len b) = ( arity o4) } by A43, A47, A56;

          

           A60: ( dom (o4 | (( arity o4) -tuples_on B3))) = (( dom o4) /\ (( arity o4) -tuples_on B3)) by RELAT_1: 61

          .= ((( arity o4) -tuples_on the carrier of U4) /\ (( arity o4) -tuples_on B3)) by MARGREL1: 22

          .= (( arity o4) -tuples_on B3) by MARGREL1: 21;

          

           A61: ( dom (o2 | (( arity o2) -tuples_on B1))) = (( dom o2) /\ (( arity o2) -tuples_on B1)) by RELAT_1: 61

          .= ((( arity o2) -tuples_on the carrier of U2) /\ (( arity o2) -tuples_on B1)) by MARGREL1: 22

          .= (( arity o2) -tuples_on B1) by MARGREL1: 21;

          ( [[:(o2 /. B1), (o4 /. B3):]] . x) = [((o2 /. B1) . ( pr1 s1)), ((o4 /. B3) . ( pr2 s1))] by A43, A47, A50, A46, A51, A54, A55, Def3

          .= [((o2 | (( arity o2) -tuples_on B1)) . s11), ((o4 /. B3) . ( pr2 s1))] by A49, UNIALG_2:def 5

          .= [(o2 . ( pr1 s1)), ((o4 /. B3) . ( pr2 s1))] by A58, A61, FUNCT_1: 47

          .= [(o2 . ( pr1 s1)), ((o4 | (( arity o4) -tuples_on B3)) . ( pr2 s1))] by A45, UNIALG_2:def 5

          .= [(o2 . ( pr1 s1)), (o4 . ( pr2 s1))] by A59, A60, FUNCT_1: 47;

          hence ( [[:(o2 /. B1), (o4 /. B3):]] . x) = (( [[:o2, o4:]] | (( arity o24) -tuples_on B)) . x) by A57;

        end;

        

        thus (( Opers ( [:U2, U4:],B)) . n) = (o24 /. B) by A20, A38, A17, A40, UNIALG_2:def 6

        .= ( [[:o2, o4:]] | (( arity o24) -tuples_on B)) by A24, A41, UNIALG_2:def 5

        .= [[:(o2 /. B1), (o4 /. B3):]] by A51, A48, A52

        .= (the charact of [:U1, U3:] . n) by A14, A8, A40, A44, A42, Def4;

      end;

      hence thesis by A24, A20, FINSEQ_2: 9;

    end;

    begin

    definition

      let k be Nat;

      :: PRALG_1:def7

      func TrivialOp (k) -> PartFunc of ( { {} } * ), { {} } means

      : Def7: ( dom it ) = {(k |-> {} )} & ( rng it ) = { {} };

      existence

      proof

        consider f be Function such that

         A1: ( dom f) = {(k |-> {} )} and

         A2: ( rng f) = { {} } by FUNCT_1: 5;

        ( dom f) c= ( { {} } * )

        proof

          reconsider a = {} as Element of { {} } by TARSKI:def 1;

          let x be object;

          assume x in ( dom f);

          then x = (k |-> a) by A1, TARSKI:def 1;

          hence thesis by FINSEQ_1:def 11;

        end;

        then

        reconsider f as PartFunc of ( { {} } * ), { {} } by A2, RELSET_1: 4;

        take f;

        thus thesis by A1, A2;

      end;

      uniqueness by FUNCT_1: 7;

    end

    registration

      let k be Nat;

      cluster ( TrivialOp k) -> homogeneous quasi_total non empty;

      coherence

      proof

        set f = ( TrivialOp k);

        

         A1: ( dom f) = {(k |-> {} )} by Def7;

        thus f is homogeneous by A1;

        now

          let x,y be FinSequence of { {} };

          assume that

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

           A3: x in ( dom f);

          

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

          

           A5: x = (k |-> {} ) by A1, A3, TARSKI:def 1;

          now

            let n be Nat;

            assume n in ( dom x);

            then n in ( dom y) by A2, A4, FINSEQ_1:def 3;

            then

             A6: (y . n) in { {} } by FINSEQ_2: 11;

            (x . n) = {} by A5;

            hence (x . n) = (y . n) by A6, TARSKI:def 1;

          end;

          hence y in ( dom f) by A2, A3, FINSEQ_2: 9;

        end;

        hence thesis by A1;

      end;

    end

    theorem :: PRALG_1:8

    for k be Nat holds ( arity ( TrivialOp k)) = k

    proof

      let k be Nat;

      now

        ( dom ( TrivialOp k)) = {(k |-> {} )} by Def7;

        then (k |-> {} ) in ( dom ( TrivialOp k)) by TARSKI:def 1;

        hence ex x be FinSequence st x in ( dom ( TrivialOp k));

        let x be FinSequence;

        assume x in ( dom ( TrivialOp k));

        then x in {(k |-> {} )} by Def7;

        then x = (k |-> {} ) by TARSKI:def 1;

        hence ( len x) = k by CARD_1:def 7;

      end;

      hence thesis by MARGREL1:def 25;

    end;

    definition

      let f be FinSequence of NAT ;

      :: PRALG_1:def8

      func TrivialOps (f) -> PFuncFinSequence of { {} } means

      : Def8: ( len it ) = ( len f) & for n st n in ( dom it ) holds for m st m = (f . n) holds (it . n) = ( TrivialOp m);

      existence

      proof

        defpred P[ set, set] means for m st m = (f . $1) holds $2 = ( TrivialOp m);

        

         A1: for k be Nat st k in ( Seg ( len f)) holds ex x be Element of ( PFuncs (( { {} } * ), { {} })) st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len f));

          then k in ( dom f) by FINSEQ_1:def 3;

          then

          reconsider k1 = (f . k) as Element of NAT by FINSEQ_2: 11;

          reconsider A = ( TrivialOp k1) as Element of ( PFuncs (( { {} } * ), { {} })) by PARTFUN1: 45;

          take A;

          let m;

          assume m = (f . k);

          hence thesis;

        end;

        consider p be FinSequence of ( PFuncs (( { {} } * ), { {} })) such that

         A2: ( dom p) = ( Seg ( len f)) & for k be Nat st k in ( Seg ( len f)) holds P[k, (p . k)] from FINSEQ_1:sch 5( A1);

        reconsider p as PFuncFinSequence of { {} };

        take p;

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

        let n;

        assume n in ( dom p);

        hence thesis by A2;

      end;

      uniqueness

      proof

        let x,y be PFuncFinSequence of { {} };

        assume that

         A3: ( len x) = ( len f) and

         A4: for n st n in ( dom x) holds for m st m = (f . n) holds (x . n) = ( TrivialOp m) and

         A5: ( len y) = ( len f) and

         A6: for n st n in ( dom y) holds for m st m = (f . n) holds (y . n) = ( TrivialOp m);

        

         A7: ( dom x) = ( Seg ( len f)) by A3, FINSEQ_1:def 3;

        now

          let n be Nat;

          assume

           A8: n in ( dom x);

          then n in ( dom f) by A7, FINSEQ_1:def 3;

          then

          reconsider m = (f . n) as Element of NAT by FINSEQ_2: 11;

          n in ( dom y) & (x . n) = ( TrivialOp m) by A4, A5, A7, A8, FINSEQ_1:def 3;

          hence (x . n) = (y . n) by A6;

        end;

        hence thesis by A3, A5, FINSEQ_2: 9;

      end;

    end

    theorem :: PRALG_1:9

    

     Th9: for f be FinSequence of NAT holds ( TrivialOps f) is homogeneous quasi_total non-empty

    proof

      let f be FinSequence of NAT ;

      

       A1: for n be Nat, h be PartFunc of ( { {} } * ), { {} } st n in ( dom ( TrivialOps f)) & h = (( TrivialOps f) . n) holds h is quasi_total

      proof

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

        assume that

         A2: n in ( dom ( TrivialOps f)) and

         A3: (( TrivialOps f) . n) = h;

        ( dom ( TrivialOps f)) = ( Seg ( len ( TrivialOps f))) by FINSEQ_1:def 3

        .= ( Seg ( len f)) by Def8

        .= ( dom f) by FINSEQ_1:def 3;

        then

        reconsider m = (f . n) as Element of NAT by A2, FINSEQ_2: 11;

        (( TrivialOps f) . n) = ( TrivialOp m) by A2, Def8;

        hence thesis by A3;

      end;

      

       A4: for n be object st n in ( dom ( TrivialOps f)) holds (( TrivialOps f) . n) is non empty

      proof

        let n be object;

        assume

         A5: n in ( dom ( TrivialOps f));

        then

        reconsider k = n as Element of NAT ;

        ( dom ( TrivialOps f)) = ( Seg ( len ( TrivialOps f))) by FINSEQ_1:def 3

        .= ( Seg ( len f)) by Def8

        .= ( dom f) by FINSEQ_1:def 3;

        then

        reconsider m = (f . k) as Element of NAT by A5, FINSEQ_2: 11;

        (( TrivialOps f) . k) = ( TrivialOp m) by A5, Def8;

        hence thesis;

      end;

      for n be Nat, h be PartFunc of ( { {} } * ), { {} } st n in ( dom ( TrivialOps f)) & h = (( TrivialOps f) . n) holds h is homogeneous

      proof

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

        assume that

         A6: n in ( dom ( TrivialOps f)) and

         A7: (( TrivialOps f) . n) = h;

        ( dom ( TrivialOps f)) = ( Seg ( len ( TrivialOps f))) by FINSEQ_1:def 3

        .= ( Seg ( len f)) by Def8

        .= ( dom f) by FINSEQ_1:def 3;

        then

        reconsider m = (f . n) as Element of NAT by A6, FINSEQ_2: 11;

        (( TrivialOps f) . n) = ( TrivialOp m) by A6, Def8;

        hence thesis by A7;

      end;

      hence thesis by A1, A4, FUNCT_1:def 9;

    end;

    theorem :: PRALG_1:10

    

     Th10: for f be FinSequence of NAT st f <> {} holds UAStr (# { {} }, ( TrivialOps f) #) is strict Universal_Algebra

    proof

      let f be FinSequence of NAT ;

      assume

       A1: f <> {} ;

      set U0 = UAStr (# { {} }, ( TrivialOps f) #);

      

       A2: the charact of U0 is homogeneous quasi_total non-empty by Th9;

      ( len the charact of U0) = ( len f) by Def8;

      then the charact of U0 <> {} by A1;

      hence thesis by A2, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;

    end;

    registration

      let D be non empty set;

      cluster non empty for Element of (D * );

      existence

      proof

        set d = the Element of D;

        reconsider e = <*d*> as Element of (D * ) by FINSEQ_1:def 11;

        take e;

        thus thesis;

      end;

    end

    definition

      let f be non empty FinSequence of NAT ;

      :: PRALG_1:def9

      func Trivial_Algebra (f) -> strict Universal_Algebra equals UAStr (# { {} }, ( TrivialOps f) #);

      coherence by Th10;

    end

    begin

    definition

      let IT be Function;

      :: PRALG_1:def10

      attr IT is Univ_Alg-yielding means

      : Def10: for x st x in ( dom IT) holds (IT . x) is Universal_Algebra;

    end

    definition

      let IT be Relation;

      :: PRALG_1:def11

      attr IT is 1-sorted-yielding means for x st x in ( rng IT) holds x is 1-sorted;

    end

    definition

      let IT be Function;

      :: original: 1-sorted-yielding

      redefine

      :: PRALG_1:def12

      attr IT is 1-sorted-yielding means

      : Def11a: for x st x in ( dom IT) holds (IT . x) is 1-sorted;

      compatibility

      proof

        thus IT is 1-sorted-yielding implies for x st x in ( dom IT) holds (IT . x) is 1-sorted

        proof

          assume

           A1: IT is 1-sorted-yielding;

          let x;

          assume x in ( dom IT);

          hence thesis by A1, FUNCT_1: 3;

        end;

        assume

         A2: for x st x in ( dom IT) holds (IT . x) is 1-sorted;

        for x st x in ( rng IT) holds x is 1-sorted

        proof

          let x;

          assume x in ( rng IT);

          then

          consider xx be object such that

           A3: xx in ( dom IT) & x = (IT . xx) by FUNCT_1:def 3;

          thus thesis by A2, A3;

        end;

        hence thesis;

      end;

    end

    registration

      cluster Univ_Alg-yielding for Function;

      existence

      proof

        reconsider f = {} as Function;

        take f;

        let x;

        thus thesis;

      end;

    end

    registration

      cluster Univ_Alg-yielding -> 1-sorted-yielding for Function;

      coherence ;

    end

    registration

      let I be set;

      cluster 1-sorted-yielding for ManySortedSet of I;

      existence

      proof

        set A = the 1-sorted;

        set f = (I --> A);

        reconsider f as ManySortedSet of I;

        take f;

        thus thesis by FUNCOP_1: 7;

      end;

    end

    definition

      let IT be Function;

      :: PRALG_1:def13

      attr IT is equal-signature means

      : Def12: for x, y st x in ( dom IT) & y in ( dom IT) holds for U1, U2 st U1 = (IT . x) & U2 = (IT . y) holds ( signature U1) = ( signature U2);

    end

    registration

      let J be non empty set;

      cluster equal-signature Univ_Alg-yielding for ManySortedSet of J;

      existence

      proof

        set U1 = the Universal_Algebra;

        set f = (J --> U1);

        reconsider f as ManySortedSet of J;

        take f;

        for x, y st x in ( dom f) & y in ( dom f) holds for U1, U2 st U1 = (f . x) & U2 = (f . y) holds ( signature U1) = ( signature U2)

        proof

          let x, y;

          assume that

           A2: x in ( dom f) and

           A3: y in ( dom f);

          let U2, U3;

          assume

           A4: U2 = (f . x) & U3 = (f . y);

          (f . x) = U1 by A2, FUNCOP_1: 7;

          hence thesis by A3, A4, FUNCOP_1: 7;

        end;

        hence f is equal-signature;

        thus thesis by FUNCOP_1: 7;

      end;

    end

    definition

      let A be 1-sorted-yielding non empty Function, j be Element of ( dom A);

      :: original: .

      redefine

      func A . j -> 1-sorted ;

      coherence by Def11a;

    end

    definition

      let J be non empty set, A be 1-sorted-yielding ManySortedSet of J, j be Element of J;

      :: original: .

      redefine

      func A . j -> 1-sorted ;

      coherence

      proof

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

        hence thesis by Def11a;

      end;

    end

    definition

      let J be non empty set, A be Univ_Alg-yielding ManySortedSet of J, j be Element of J;

      :: original: .

      redefine

      func A . j -> Universal_Algebra ;

      coherence

      proof

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

        hence thesis by Def10;

      end;

    end

    definition

      let A be 1-sorted-yielding Function;

      :: PRALG_1:def14

      func Carrier A -> Function means

      : Def13: ( dom it ) = ( dom A) & for j be set st j in ( dom A) holds ex R be 1-sorted st R = (A . j) & (it . j) = the carrier of R;

      existence

      proof

        set J = ( dom A);

        defpred P[ object, object] means ex R be 1-sorted st R = (A . $1) & $2 = the carrier of R;

        

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

        proof

          let i be object;

          assume

           A2: i in J;

          then

          reconsider J as non empty set;

          reconsider i9 = i as Element of J by A2;

          ex j be object st P[i, j]

          proof

            reconsider R = (A . i9) as 1-sorted by Def11a;

            take j = the carrier of R;

            thus thesis;

          end;

          hence thesis;

        end;

        consider M be Function such that

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

        take M;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let X,Y be Function;

        assume

         A5: ( dom X) = ( dom A) & (for j be set st j in ( dom A) holds ex R be 1-sorted st R = (A . j) & (X . j) = the carrier of R) & ( dom Y) = ( dom A) & for j be set st j in ( dom A) holds ex R be 1-sorted st R = (A . j) & (Y . j) = the carrier of R;

        for i be object st i in ( dom A) holds (X . i) = (Y . i)

        proof

          let i be object;

          assume i in ( dom A);

          then (ex R be 1-sorted st R = (A . i) & (X . i) = the carrier of R) & ex R be 1-sorted st R = (A . i) & (Y . i) = the carrier of R by A5;

          hence thesis;

        end;

        hence thesis by A5;

      end;

    end

    definition

      let J be set, A be 1-sorted-yielding ManySortedSet of J;

      :: original: Carrier

      redefine

      :: PRALG_1:def15

      func Carrier A -> ManySortedSet of J means for j be set st j in J holds ex R be 1-sorted st R = (A . j) & (it . j) = the carrier of R;

      compatibility

      proof

        let f be ManySortedSet of J;

        hereby

          assume

           A1: f = ( Carrier A);

          then

           A3: ( dom f) = ( dom A) by Def13;

          

           A4: J = ( dom f) by PARTFUN1:def 2;

          let j be set;

          assume

           A2: j in J;

          hence ex R be 1-sorted st R = (A . j) & (f . j) = the carrier of R by A1, Def13, A4, A3;

        end;

        assume

         B1: for j be set st j in J holds ex R be 1-sorted st R = (A . j) & (f . j) = the carrier of R;

        

         B0: ( dom ( Carrier A)) = ( dom A) by Def13

        .= J by PARTFUN1:def 2;

        

         B4: J = ( dom f) by PARTFUN1:def 2;

        for j be set st j in J holds (f . j) = (( Carrier A) . j)

        proof

          let j be set;

          assume

           B3: j in J;

          then

          consider R be 1-sorted such that

           B2: R = (A . j) & (f . j) = the carrier of R by B1;

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

          then ex R1 be 1-sorted st R1 = (A . j) & (( Carrier A) . j) = the carrier of R1 by Def13, B3;

          hence thesis by B2;

        end;

        hence thesis by B0, B4;

      end;

      coherence

      proof

        

         A1: ( dom A) = J by PARTFUN1:def 2;

        ( dom ( Carrier A)) = ( dom A) by Def13;

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

      end;

    end

    registration

      let J be non empty set, A be Univ_Alg-yielding ManySortedSet of J;

      cluster ( Carrier A) -> non-empty;

      coherence

      proof

        let i be object;

        

         A0: ( dom A) = J by PARTFUN1:def 2;

        assume

         A1: i in J;

        then

        consider R be 1-sorted such that

         A2: R = (A . i) and

         A3: (( Carrier A) . i) = the carrier of R by Def13, A0;

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

        then R is Universal_Algebra by A1, A2, Def10;

        hence thesis by A3;

      end;

    end

    definition

      let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J;

      :: PRALG_1:def16

      func ComSign A -> FinSequence of NAT means

      : Def14: for j be Element of J holds it = ( signature (A . j));

      existence

      proof

        set j = the Element of J;

        reconsider U0 = (A . j) as Universal_Algebra;

        take ( signature U0);

        let j1 be Element of J;

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

        hence thesis by Def12;

      end;

      uniqueness

      proof

        set j = the Element of J;

        let X,Y be FinSequence of NAT ;

        assume that

         A1: for j be Element of J holds X = ( signature (A . j)) and

         A2: for j be Element of J holds Y = ( signature (A . j));

        reconsider U0 = (A . j) as Universal_Algebra;

        X = ( signature U0) by A1;

        hence thesis by A2;

      end;

    end

    registration

      let J be non empty set, B be non-empty ManySortedSet of J;

      cluster ( product B) -> non empty;

      coherence ;

    end

    definition

      let J be non empty set, B be non-empty ManySortedSet of J;

      :: PRALG_1:def17

      mode ManySortedOperation of B -> ManySortedFunction of J means

      : Def15: for j be Element of J holds (it . j) is homogeneous quasi_total non empty PartFunc of ((B . j) * ), (B . j);

      existence

      proof

        defpred P[ object, object] means $2 in (B . $1);

        

         A1: for x be object st x in J holds ex y be object st P[x, y] by XBOOLE_0:def 1;

        consider f be Function such that

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

        deffunc G( object) = (( <*> (B . $1)) .--> (f . $1));

        consider F be Function such that

         A3: ( dom F) = J & for x be object st x in J holds (F . x) = G(x) from FUNCT_1:sch 3;

        reconsider F as ManySortedSet of J by A3, PARTFUN1:def 2, RELAT_1:def 18;

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

        proof

          let x be object;

          assume x in ( dom F);

          then (F . x) = (( <*> (B . x)) .--> (f . x)) by A3;

          hence thesis;

        end;

        then

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

        take F;

        let j be Element of J;

        reconsider b = (f . j) as Element of (B . j) by A2;

        (F . j) = (( <*> (B . j)) .--> b) by A3;

        hence thesis by MARGREL1: 18;

      end;

    end

    definition

      let J be non empty set, B be non-empty ManySortedSet of J, O be ManySortedOperation of B, j be Element of J;

      :: original: .

      redefine

      func O . j -> homogeneous quasi_total non empty PartFunc of ((B . j) * ), (B . j) ;

      coherence by Def15;

    end

    definition

      let IT be Function;

      :: PRALG_1:def18

      attr IT is equal-arity means for x,y be set st x in ( dom IT) & y in ( dom IT) holds for f,g be Function st (IT . x) = f & (IT . y) = g holds for n,m be Nat holds for X,Y be non empty set st ( dom f) = (n -tuples_on X) & ( dom g) = (m -tuples_on Y) holds for o1 be homogeneous quasi_total non empty PartFunc of (X * ), X, o2 be homogeneous quasi_total non empty PartFunc of (Y * ), Y st f = o1 & g = o2 holds ( arity o1) = ( arity o2);

    end

    registration

      let J be non empty set, B be non-empty ManySortedSet of J;

      cluster equal-arity for ManySortedOperation of B;

      existence

      proof

        defpred P[ object, object] means $2 in (B . $1);

        

         A1: for x be object st x in J holds ex y be object st P[x, y] by XBOOLE_0:def 1;

        consider f be Function such that

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

        deffunc G( object) = (( <*> (B . $1)) .--> (f . $1));

        consider F be Function such that

         A3: ( dom F) = J & for x be object st x in J holds (F . x) = G(x) from FUNCT_1:sch 3;

        reconsider F as ManySortedSet of J by A3, PARTFUN1:def 2, RELAT_1:def 18;

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

        proof

          let x be object;

          assume x in ( dom F);

          then (F . x) = (( <*> (B . x)) .--> (f . x)) by A3;

          hence thesis;

        end;

        then

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

        now

          let j be Element of J;

          reconsider b = (f . j) as Element of (B . j) by A2;

          (F . j) = (( <*> (B . j)) .--> b) by A3;

          hence (F . j) is homogeneous quasi_total non empty PartFunc of ((B . j) * ), (B . j) by MARGREL1: 18;

        end;

        then

        reconsider F as ManySortedOperation of B by Def15;

        take F;

        for x,y be set st x in ( dom F) & y in ( dom F) holds for f,g be Function st (F . x) = f & (F . y) = g holds for n,m be Nat holds for X,Y be non empty set st ( dom f) = (n -tuples_on X) & ( dom g) = (m -tuples_on Y) holds for o1 be homogeneous quasi_total non empty PartFunc of (X * ), X, o2 be homogeneous quasi_total non empty PartFunc of (Y * ), Y st f = o1 & g = o2 holds ( arity o1) = ( arity o2)

        proof

          let x,y be set;

          assume that

           A4: x in ( dom F) and

           A5: y in ( dom F);

          reconsider x1 = x, y1 = y as Element of J by A3, A4, A5;

          let g,h be Function;

          assume that

           A6: (F . x) = g and

           A7: (F . y) = h;

          reconsider fx = (f . x1) as Element of (B . x1) by A2;

          let n,m be Nat;

          let X,Y be non empty set;

          assume that ( dom g) = (n -tuples_on X) and ( dom h) = (m -tuples_on Y);

          let o1 be homogeneous quasi_total non empty PartFunc of (X * ), X, o2 be homogeneous quasi_total non empty PartFunc of (Y * ), Y;

          assume that

           A8: g = o1 and

           A9: h = o2;

          reconsider o1x = (( <*> (B . x1)) .--> fx) as homogeneous quasi_total non empty PartFunc of ((B . x1) * ), (B . x1) by MARGREL1: 18;

          consider p1 be object such that

           A11: p1 in ( dom o1) by XBOOLE_0:def 1;

          ( dom o1) c= (X * ) by RELAT_1:def 18;

          then

          reconsider p1 as Element of (X * ) by A11;

          o1 = (( <*> (B . x)) .--> (f . x)) by A3, A4, A6, A8;

          then p1 = ( <*> (B . x1)) by A11, TARSKI:def 1;

          then ( len p1) = 0 ;

          then

           A12: ( arity o1) = 0 by A11, MARGREL1:def 25;

          reconsider fy = (f . y1) as Element of (B . y1) by A2;

          reconsider o2y = (( <*> (B . y1)) .--> fy) as homogeneous quasi_total non empty PartFunc of ((B . y1) * ), (B . y1) by MARGREL1: 18;

          consider p2 be object such that

           A14: p2 in ( dom o2) by XBOOLE_0:def 1;

          ( dom o2) c= (Y * ) by RELAT_1:def 18;

          then

          reconsider p2 as Element of (Y * ) by A14;

          o2 = (( <*> (B . y)) .--> (f . y)) by A3, A5, A7, A9;

          then p2 = ( <*> (B . y1)) by A14, TARSKI:def 1;

          then ( len p2) = 0 ;

          hence thesis by A12, A14, MARGREL1:def 25;

        end;

        hence thesis;

      end;

    end

    theorem :: PRALG_1:11

    

     Th11: for J be non empty set, B be non-empty ManySortedSet of J, O be ManySortedOperation of B holds O is equal-arity iff for i,j be Element of J holds ( arity (O . i)) = ( arity (O . j))

    proof

      let J be non empty set, B be non-empty ManySortedSet of J, O be ManySortedOperation of B;

      thus O is equal-arity implies for i,j be Element of J holds ( arity (O . i)) = ( arity (O . j))

      proof

        assume

         A1: O is equal-arity;

        let i,j be Element of J;

        

         A2: ( dom (O . j)) = (( arity (O . j)) -tuples_on (B . j)) by MARGREL1: 22;

        ( dom O) = J & ( dom (O . i)) = (( arity (O . i)) -tuples_on (B . i)) by MARGREL1: 22, PARTFUN1:def 2;

        hence thesis by A1, A2;

      end;

      assume

       A3: for i,j be Element of J holds ( arity (O . i)) = ( arity (O . j));

      let x,y be set;

      assume x in ( dom O) & y in ( dom O);

      then

      reconsider x1 = x, y1 = y as Element of J by PARTFUN1:def 2;

      let f,g be Function;

      assume that

       A4: (O . x) = f and

       A5: (O . y) = g;

      ( arity (O . x1)) = ( arity (O . y1)) by A3;

      then

       A6: ( dom g) = (( arity (O . x1)) -tuples_on (B . y1)) by A5, MARGREL1: 22;

      let n,m be Nat;

      let X,Y be non empty set;

      assume that

       A7: ( dom f) = (n -tuples_on X) and

       A8: ( dom g) = (m -tuples_on Y);

      ( dom f) = (( arity (O . x1)) -tuples_on (B . x1)) by A4, MARGREL1: 22;

      then

       A9: n = ( arity (O . x1)) by A7, FINSEQ_2: 110;

      set p = the Element of (n -tuples_on X);

      set q = the Element of (m -tuples_on Y);

      let o1 be homogeneous quasi_total non empty PartFunc of (X * ), X, o2 be homogeneous quasi_total non empty PartFunc of (Y * ), Y;

      assume that

       A10: f = o1 and

       A11: g = o2;

      

       A12: ( arity o2) = ( len q) by A8, A11, MARGREL1:def 25

      .= m by CARD_1:def 7;

      ( arity o1) = ( len p) by A7, A10, MARGREL1:def 25

      .= n by CARD_1:def 7;

      hence thesis by A8, A6, A9, A12, FINSEQ_2: 110;

    end;

    definition

      let F be Function-yielding Function, f be Function;

      :: PRALG_1:def19

      func F .. f -> Function means

      : Def17: ( dom it ) = (( dom F) /\ ( dom f)) & for x be set st x in ( dom it ) holds (it . x) = ((F . x) . (f . x));

      existence

      proof

        set I = (( dom F) /\ ( dom f));

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

        

         A1: for i be object st i in I holds ex y be object st P[i, y];

        consider Ff be Function such that

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

        take Ff;

        ( dom Ff) = (( dom F) /\ ( dom f)) by A2;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let m,n be Function;

        assume that

         A3: ( dom m) = (( dom F) /\ ( dom f)) and

         A4: for x be set st x in ( dom m) holds (m . x) = ((F . x) . (f . x)) and

         A5: ( dom n) = (( dom F) /\ ( dom f)) and

         A6: for x be set st x in ( dom n) holds (n . x) = ((F . x) . (f . x));

        for x be object st x in ( dom m) holds (m . x) = (n . x)

        proof

          let x be object;

          consider g be set such that

           A7: g = (F . x);

          reconsider g as Function by A7;

          assume

           A8: x in ( dom m);

          then

           A9: (m . x) = (g . (f . x)) by A4, A7;

          x in ( dom n) by A3, A5, A8;

          hence thesis by A6, A7, A9;

        end;

        hence thesis by A3, A5;

      end;

    end

    registration

      let I be set, f be ManySortedFunction of I, x be ManySortedSet of I;

      cluster (f .. x) -> I -defined;

      coherence

      proof

        ( dom (f .. x)) = (( dom f) /\ ( dom x)) by Def17

        .= (I /\ ( dom x)) by PARTFUN1:def 2

        .= (I /\ I) by PARTFUN1:def 2;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let I be set, f be ManySortedFunction of I, x be ManySortedSet of I;

      cluster (f .. x) -> total;

      coherence

      proof

        ( dom (f .. x)) = (( dom f) /\ ( dom x)) by Def17

        .= (I /\ ( dom x)) by PARTFUN1:def 2

        .= (I /\ I) by PARTFUN1:def 2;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    definition

      let I be set, f be ManySortedFunction of I, x be ManySortedSet of I;

      :: original: ..

      redefine

      :: PRALG_1:def20

      func f .. x means

      : Def18: ( dom it ) = I & for i be set st i in I holds for g be Function st g = (f . i) holds (it . i) = (g . (x . i));

      compatibility

      proof

        let M be Function;

        hereby

          assume

           A1: M = (f .. x);

          hence

           A2: ( dom M) = I by PARTFUN1:def 2;

          thus for i be set st i in I holds for g be Function st g = (f . i) holds (M . i) = (g . (x . i)) by A1, A2, Def17;

        end;

        assume that

         A3: ( dom M) = I and

         A4: for i be set st i in I holds for g be Function st g = (f . i) holds (M . i) = (g . (x . i));

        

         A5: ( dom f) = I by PARTFUN1:def 2;

        then

         A6: for i be set st i in ( dom f) holds (M . i) = ((f . i) . (x . i)) by A4;

        ( dom M) = (I /\ I) by A3

        .= (I /\ ( dom x)) by PARTFUN1:def 2

        .= (( dom f) /\ ( dom x)) by PARTFUN1:def 2;

        hence thesis by A3, A5, A6, Def17;

      end;

    end

    registration

      let J be non empty set, B be non-empty ManySortedSet of J, p be FinSequence of ( product B);

      cluster ( uncurry p) -> [:( dom p), J:] -defined;

      coherence

      proof

        now

          set j = the Element of J;

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

          then (B . j) in ( rng B) by FUNCT_1:def 3;

          then

          reconsider S = ( union ( rng B)) as non empty set by XBOOLE_1: 3, ZFMISC_1: 74;

          ( rng p) c= ( Funcs (J,S))

          proof

            let x be object;

            

             A1: ( rng p) c= ( product B) by FINSEQ_1:def 4;

            assume x in ( rng p);

            then

            consider f be Function such that

             A2: x = f and

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

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

            

             A5: ( rng f) c= S

            proof

              let z be object;

              assume z in ( rng f);

              then

              consider y be object such that

               A6: y in ( dom f) and

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

              (B . y) in ( rng B) by A3, A6, FUNCT_1:def 3;

              then (B . y) c= ( union ( rng B)) by ZFMISC_1: 74;

              hence thesis by A3, A4, A6, A7;

            end;

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

            hence thesis by A2, A3, A5, FUNCT_2:def 2;

          end;

          then ( dom ( uncurry p)) = [:( dom p), J:] by FUNCT_5: 26;

          hence thesis by RELAT_1:def 18;

        end;

        hence thesis;

      end;

    end

    registration

      let J be non empty set, B be non-empty ManySortedSet of J, p be FinSequence of ( product B);

      cluster ( uncurry p) -> total;

      coherence

      proof

        now

          set j = the Element of J;

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

          then (B . j) in ( rng B) by FUNCT_1:def 3;

          then

          reconsider S = ( union ( rng B)) as non empty set by XBOOLE_1: 3, ZFMISC_1: 74;

          ( rng p) c= ( Funcs (J,S))

          proof

            let x be object;

            

             A1: ( rng p) c= ( product B) by FINSEQ_1:def 4;

            assume x in ( rng p);

            then

            consider f be Function such that

             A2: x = f and

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

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

            

             A5: ( rng f) c= S

            proof

              let z be object;

              assume z in ( rng f);

              then

              consider y be object such that

               A6: y in ( dom f) and

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

              (B . y) in ( rng B) by A3, A6, FUNCT_1:def 3;

              then (B . y) c= ( union ( rng B)) by ZFMISC_1: 74;

              hence thesis by A3, A4, A6, A7;

            end;

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

            hence thesis by A2, A3, A5, FUNCT_2:def 2;

          end;

          hence thesis by PARTFUN1:def 2, FUNCT_5: 26;

        end;

        hence thesis;

      end;

    end

    registration

      let I,J be set, X be ManySortedSet of [:I, J:];

      cluster ( ~ X) -> [:J, I:] -defined;

      coherence

      proof

        ( dom X) = [:I, J:] by PARTFUN1:def 2;

        then ( dom ( ~ X)) = [:J, I:] by FUNCT_4: 46;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let I,J be set, X be ManySortedSet of [:I, J:];

      cluster ( ~ X) -> total;

      coherence

      proof

        ( dom X) = [:I, J:] by PARTFUN1:def 2;

        hence thesis by PARTFUN1:def 2, FUNCT_4: 46;

      end;

    end

    registration

      let X be set, Y be non empty set, f be ManySortedSet of [:X, Y:];

      cluster ( curry f) -> X -defined;

      coherence

      proof

        set a = ( curry f);

        ( dom f) = [:X, Y:] & ( dom a) = ( proj1 ( dom f)) by FUNCT_5:def 1, PARTFUN1:def 2;

        then ( dom a) = X by FUNCT_5: 9;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let X be set, Y be non empty set, f be ManySortedSet of [:X, Y:];

      cluster ( curry f) -> total;

      coherence

      proof

        set a = ( curry f);

        ( dom f) = [:X, Y:] & ( dom a) = ( proj1 ( dom f)) by FUNCT_5:def 1, PARTFUN1:def 2;

        then ( dom a) = X by FUNCT_5: 9;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    definition

      let J be non empty set, B be non-empty ManySortedSet of J, O be equal-arity ManySortedOperation of B;

      :: PRALG_1:def21

      func ComAr (O) -> Nat means

      : Def19: for j be Element of J holds it = ( arity (O . j));

      existence

      proof

        set i = the Element of J;

        take ( arity (O . i));

        let j be Element of J;

        thus thesis by Th11;

      end;

      uniqueness

      proof

        set j = the Element of J;

        let n,m be Nat;

        assume that

         A1: for j be Element of J holds n = ( arity (O . j)) and

         A2: for j be Element of J holds m = ( arity (O . j));

        n = ( arity (O . j)) by A1;

        hence thesis by A2;

      end;

    end

    definition

      let J be non empty set, B be non-empty ManySortedSet of J, O be equal-arity ManySortedOperation of B;

      :: PRALG_1:def22

      func [[:O:]] -> homogeneous quasi_total non empty PartFunc of (( product B) * ), ( product B) means ( dom it ) = (( ComAr O) -tuples_on ( product B)) & for p be Element of (( product B) * ) st p in ( dom it ) holds (( dom p) = {} implies (it . p) = (O .. ( EmptyMS J))) & (( dom p) <> {} implies for Z be non empty set, w be ManySortedSet of [:J, Z:] st Z = ( dom p) & w = ( ~ ( uncurry p)) holds (it . p) = (O .. ( curry w)));

      existence

      proof

        set pr = ( product B), ca = ( ComAr O), ct = (ca -tuples_on pr);

        defpred P[ object, object] means for p be Element of (pr * ) st p = $1 holds (( dom p) = {} implies $2 = (O .. ( EmptyMS J))) & (( dom p) <> {} implies for Z be non empty set, w be ManySortedSet of [:J, Z:] st Z = ( dom p) & w = ( ~ ( uncurry p)) holds $2 = (O .. ( curry w)));

        set aa = { q where q be Element of (pr * ) : ( len q) = ca };

        

         A1: for x be object st x in ct holds ex y be object st y in pr & P[x, y]

        proof

          let x be object;

          assume x in ct;

          then

          consider w be Element of (pr * ) such that

           A2: x = w and

           A3: ( len w) = ca;

          now

            per cases ;

              case

               A4: ( dom w) = {} ;

              

               A5: for z be object st z in ( dom B) holds ((O .. ( EmptyMS J)) . z) in (B . z)

              proof

                let z be object;

                assume z in ( dom B);

                then

                reconsider j = z as Element of J by PARTFUN1:def 2;

                

                 A6: ( rng (O . j)) c= (B . j) by RELAT_1:def 19;

                w = {} by A4;

                then ( arity (O . j)) = 0 by A3, Def19;

                

                then ( dom (O . j)) = ( 0 -tuples_on (B . j)) by MARGREL1: 22

                .= {( <*> (B . j))} by FINSEQ_2: 94;

                then ( {} (B . j)) in ( dom (O . j)) by TARSKI:def 1;

                then

                 A7: ((O . j) . ( {} (B . j))) in ( rng (O . j)) by FUNCT_1:def 3;

                ((O .. ( EmptyMS J)) . z) = ((O . j) . (( EmptyMS J) . j)) by Def18

                .= ((O . j) . ( {} (B . j)));

                hence thesis by A7, A6;

              end;

              take y = (O .. ( EmptyMS J));

              ( dom (O .. ( EmptyMS J))) = J by PARTFUN1:def 2

              .= ( dom B) by PARTFUN1:def 2;

              hence y in pr by A5, CARD_3:def 5;

              let p be Element of (pr * );

              assume p = x;

              hence (( dom p) = {} implies y = (O .. ( EmptyMS J))) & (( dom p) <> {} implies for Z be non empty set, w be ManySortedSet of [:J, Z:] st Z = ( dom p) & w = ( ~ ( uncurry p)) holds y = (O .. ( curry w))) by A2, A4;

            end;

              case ( dom w) <> {} ;

              then

              reconsider Z = ( dom w) as non empty set;

              reconsider p = ( ~ ( uncurry w)) as ManySortedSet of [:J, Z:];

              take y = (O .. ( curry p));

              

               A8: for z be object st z in ( dom B) holds ((O .. ( curry p)) . z) in (B . z)

              proof

                let z be object;

                assume z in ( dom B);

                then

                reconsider j = z as Element of J by PARTFUN1:def 2;

                

                 A9: ( dom p) = [:J, Z:] by PARTFUN1:def 2;

                then ( proj1 ( dom p)) = J by FUNCT_5: 9;

                then

                consider g be Function such that

                 A10: (( curry p) . j) = g and

                 A11: ( dom g) = ( proj2 (( dom p) /\ [: {j}, ( proj2 ( dom p)):])) and

                 A12: for y st y in ( dom g) holds (g . y) = (p . (j,y)) by FUNCT_5:def 1;

                ( proj2 ( dom p)) = Z by A9, FUNCT_5: 9;

                

                then

                 A13: ( dom g) = ( proj2 [:(J /\ {j}), (Z /\ Z):]) by A9, A11, ZFMISC_1: 100

                .= ( proj2 [: {j}, Z:]) by ZFMISC_1: 46

                .= ( dom w) by FUNCT_5: 9

                .= ( Seg ( len w)) by FINSEQ_1:def 3;

                then

                reconsider g as FinSequence by FINSEQ_1:def 2;

                ( rng g) c= (B . j)

                proof

                  let y be object;

                  assume y in ( rng g);

                  then

                  consider x be object such that

                   A14: x in ( dom g) and

                   A15: (g . x) = y by FUNCT_1:def 3;

                  ( dom ( uncurry w)) = [:( dom w), J:] & ( dom g) = ( dom w) by A13, FINSEQ_1:def 3, PARTFUN1:def 2;

                  then

                   A16: [x, j] in ( dom ( uncurry w)) by A14, ZFMISC_1: 87;

                  then

                  consider a be object, f be Function, b be object such that

                   A17: [x, j] = [a, b] and

                   A18: a in ( dom w) and

                   A19: f = (w . a) and

                   A20: b in ( dom f) by FUNCT_5:def 2;

                  y = (( ~ ( uncurry w)) . (j,x)) by A12, A14, A15;

                  then

                   A21: y = (( uncurry w) . (x,j)) by A16, FUNCT_4:def 2;

                  ( [a, b] `1 ) = a & ( [a, b] `2 ) = j by A17;

                  then

                   A22: y = (f . j) by A16, A21, A17, A19, FUNCT_5:def 2;

                  

                   A23: j = b by A17, XTUPLE_0: 1;

                  

                   A24: ( rng w) c= pr & (w . a) in ( rng w) by A18, FINSEQ_1:def 4, FUNCT_1:def 3;

                  then ( dom f) = ( dom B) by A19, CARD_3: 9;

                  hence thesis by A19, A20, A23, A24, A22, CARD_3: 9;

                end;

                then

                reconsider g as FinSequence of (B . j) by FINSEQ_1:def 4;

                reconsider g as Element of ((B . j) * ) by FINSEQ_1:def 11;

                ( arity (O . j)) = ca by Def19;

                

                then

                 A25: ( dom (O . j)) = (ca -tuples_on (B . j)) by MARGREL1: 22

                .= { s where s be Element of ((B . j) * ) : ( len s) = ca };

                ( len g) = ( len w) by A13, FINSEQ_1:def 3;

                then g in ( dom (O . j)) by A3, A25;

                then

                 A26: ((O . j) . g) in ( rng (O . j)) by FUNCT_1:def 3;

                ((O .. ( curry p)) . z) = ((O . j) . (( curry p) . j)) & ( rng (O . j)) c= (B . j) by Def18, RELAT_1:def 19;

                hence thesis by A10, A26;

              end;

              ( dom (O .. ( curry p))) = J by PARTFUN1:def 2

              .= ( dom B) by PARTFUN1:def 2;

              hence y in pr by A8, CARD_3:def 5;

              let l be Element of (pr * );

              assume l = x;

              hence (( dom l) = {} implies y = (O .. ( EmptyMS J))) & (( dom l) <> {} implies for Z be non empty set, w be ManySortedSet of [:J, Z:] st Z = ( dom l) & w = ( ~ ( uncurry l)) holds y = (O .. ( curry w))) by A2;

            end;

          end;

          hence thesis;

        end;

        consider f be Function such that

         A27: ( dom f) = ct & ( rng f) c= pr & for x be object st x in ct holds P[x, (f . x)] from FUNCT_1:sch 6( A1);

        ct in the set of all (n -tuples_on pr) where n be Nat;

        then

         A28: ct c= ( union the set of all (m -tuples_on pr) where m be Nat) by ZFMISC_1: 74;

        then ( dom f) c= (pr * ) by A27, FINSEQ_2: 108;

        then

        reconsider f as PartFunc of (pr * ), pr by A27, RELSET_1: 4;

        

         A29: f is homogeneous

        proof

          let x,y be FinSequence;

          assume

           A30: x in ( dom f) & y in ( dom f);

          then

          reconsider x1 = x, y1 = y as Element of (pr * ) by A27, A28, FINSEQ_2: 108;

          (ex w be Element of (pr * ) st x1 = w & ( len w) = ca) & ex w be Element of (pr * ) st y1 = w & ( len w) = ca by A27, A30;

          hence thesis;

        end;

        f is quasi_total

        proof

          let x,y be FinSequence of pr;

          assume that

           A31: ( len x) = ( len y) and

           A32: x in ( dom f);

          reconsider x1 = x, y1 = y as Element of (pr * ) by FINSEQ_1:def 11;

          ex w be Element of (pr * ) st x1 = w & ( len w) = ca by A27, A32;

          then y1 in aa by A31;

          hence thesis by A27;

        end;

        then

        reconsider f as homogeneous quasi_total non empty PartFunc of (pr * ), pr by A27, A29;

        take f;

        thus ( dom f) = ct by A27;

        let p be Element of (pr * );

        assume p in ( dom f);

        hence thesis by A27;

      end;

      uniqueness

      proof

        set pr = ( product B), ca = ( ComAr O);

        let f,g be homogeneous quasi_total non empty PartFunc of (pr * ), pr;

        assume that

         A33: ( dom f) = (ca -tuples_on pr) and

         A34: for p be Element of (pr * ) st p in ( dom f) holds (( dom p) = {} implies (f . p) = (O .. ( EmptyMS J))) & (( dom p) <> {} implies for Z be non empty set, w be ManySortedSet of [:J, Z:] st Z = ( dom p) & w = ( ~ ( uncurry p)) holds (f . p) = (O .. ( curry w))) and

         A35: ( dom g) = (ca -tuples_on pr) and

         A36: for p be Element of (pr * ) st p in ( dom g) holds (( dom p) = {} implies (g . p) = (O .. ( EmptyMS J))) & (( dom p) <> {} implies for Z be non empty set, w be ManySortedSet of [:J, Z:] st Z = ( dom p) & w = ( ~ ( uncurry p)) holds (g . p) = (O .. ( curry w)));

        for x be object st x in (ca -tuples_on pr) holds (f . x) = (g . x)

        proof

          let x be object;

          assume

           A37: x in (ca -tuples_on pr);

          then

          consider s be Element of (pr * ) such that

           A38: x = s and ( len s) = ca;

          per cases ;

            suppose

             A39: ( dom s) = {} ;

            then (f . s) = (O .. ( EmptyMS J)) by A33, A34, A37, A38;

            hence thesis by A35, A36, A37, A38, A39;

          end;

            suppose ( dom s) <> {} ;

            then

            reconsider Z = ( dom s) as non empty set;

            reconsider w = ( ~ ( uncurry s)) as ManySortedSet of [:J, Z:];

            (f . s) = (O .. ( curry w)) by A33, A34, A37, A38;

            hence thesis by A35, A36, A37, A38;

          end;

        end;

        hence thesis by A33, A35;

      end;

    end

    definition

      let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J, n be Nat;

      assume

       A1: n in ( dom ( ComSign A));

      :: PRALG_1:def23

      func ProdOp (A,n) -> equal-arity ManySortedOperation of ( Carrier A) means for j be Element of J holds for o be operation of (A . j) st (the charact of (A . j) . n) = o holds (it . j) = o;

      existence

      proof

        defpred P[ object, object] means for j be Element of J st $1 = j holds for o be operation of (A . j) st (the charact of (A . j) . n) = o holds $2 = o;

        

         A2: for x be object st x in J holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in J;

          then

          reconsider x1 = x as Element of J;

          n in ( dom ( signature (A . x1))) by A1, Def14;

          then n in ( Seg ( len ( signature (A . x1)))) by FINSEQ_1:def 3;

          then n in ( Seg ( len the charact of (A . x1))) by UNIALG_1:def 4;

          then n in ( dom the charact of (A . x1)) by FINSEQ_1:def 3;

          then

          reconsider o = (the charact of (A . x1) . n) as operation of (A . x1) by FUNCT_1:def 3;

          take o;

          let j be Element of J;

          assume

           A3: x = j;

          let o1 be operation of (A . j);

          assume (the charact of (A . j) . n) = o1;

          hence thesis by A3;

        end;

        consider f be Function such that

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

        reconsider f as ManySortedSet of J by A4, PARTFUN1:def 2, RELAT_1:def 18;

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

        proof

          let x be object;

          assume x in ( dom f);

          then

          reconsider x1 = x as Element of J by A4;

          n in ( dom ( signature (A . x1))) by A1, Def14;

          then n in ( Seg ( len ( signature (A . x1)))) by FINSEQ_1:def 3;

          then n in ( Seg ( len the charact of (A . x1))) by UNIALG_1:def 4;

          then n in ( dom the charact of (A . x1)) by FINSEQ_1:def 3;

          then

          reconsider o = (the charact of (A . x1) . n) as operation of (A . x1) by FUNCT_1:def 3;

          (f . x) = o by A4;

          hence thesis;

        end;

        then

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

        for j be Element of J holds (f . j) is homogeneous quasi_total non empty PartFunc of ((( Carrier A) . j) * ), (( Carrier A) . j)

        proof

          let j be Element of J;

          

           AA: J = ( dom A) by PARTFUN1:def 2;

          n in ( dom ( signature (A . j))) by A1, Def14;

          then n in ( Seg ( len ( signature (A . j)))) by FINSEQ_1:def 3;

          then n in ( Seg ( len the charact of (A . j))) by UNIALG_1:def 4;

          then n in ( dom the charact of (A . j)) by FINSEQ_1:def 3;

          then

          reconsider o = (the charact of (A . j) . n) as operation of (A . j) by FUNCT_1:def 3;

          (ex R be 1-sorted st R = (A . j) & (( Carrier A) . j) = the carrier of R) & (f . j) = o by A4, Def13, AA;

          hence thesis;

        end;

        then

        reconsider f as ManySortedOperation of ( Carrier A) by Def15;

        for i,j be Element of J holds ( arity (f . i)) = ( arity (f . j))

        proof

          let i,j be Element of J;

          

           A5: n in ( dom ( signature (A . j))) by A1, Def14;

          then

           A6: n in ( Seg ( len ( signature (A . j)))) by FINSEQ_1:def 3;

          then n in ( Seg ( len the charact of (A . j))) by UNIALG_1:def 4;

          then n in ( dom the charact of (A . j)) by FINSEQ_1:def 3;

          then

          reconsider o = (the charact of (A . j) . n) as operation of (A . j) by FUNCT_1:def 3;

          

           A7: (( signature (A . j)) . n) = ( arity o) by A5, UNIALG_1:def 4;

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

          then

           A8: ( signature (A . i)) = ( signature (A . j)) by Def12;

          then n in ( Seg ( len the charact of (A . i))) by A6, UNIALG_1:def 4;

          then n in ( dom the charact of (A . i)) by FINSEQ_1:def 3;

          then

          reconsider o1 = (the charact of (A . i) . n) as operation of (A . i) by FUNCT_1:def 3;

          ( arity (f . j)) = ( arity o) & (f . i) = o1 by A4;

          hence thesis by A8, A5, A7, UNIALG_1:def 4;

        end;

        then

        reconsider f as equal-arity ManySortedOperation of ( Carrier A) by Th11;

        take f;

        let j be Element of J;

        let o be operation of (A . j);

        assume (the charact of (A . j) . n) = o;

        hence thesis by A4;

      end;

      uniqueness

      proof

        let O1,O2 be equal-arity ManySortedOperation of ( Carrier A);

        assume that

         A9: for j be Element of J holds for o be operation of (A . j) st (the charact of (A . j) . n) = o holds (O1 . j) = o and

         A10: for j be Element of J holds for o be operation of (A . j) st (the charact of (A . j) . n) = o holds (O2 . j) = o;

        for x be object st x in J holds (O1 . x) = (O2 . x)

        proof

          let x be object;

          assume x in J;

          then

          reconsider x1 = x as Element of J;

          n in ( dom ( signature (A . x1))) by A1, Def14;

          then n in ( Seg ( len ( signature (A . x1)))) by FINSEQ_1:def 3;

          then n in ( Seg ( len the charact of (A . x1))) by UNIALG_1:def 4;

          then n in ( dom the charact of (A . x1)) by FINSEQ_1:def 3;

          then

          reconsider o = (the charact of (A . x1) . n) as operation of (A . x1) by FUNCT_1:def 3;

          (O1 . x1) = o by A9;

          hence thesis by A10;

        end;

        hence thesis;

      end;

    end

    definition

      let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J;

      :: PRALG_1:def24

      func ProdOpSeq (A) -> PFuncFinSequence of ( product ( Carrier A)) means

      : Def22: ( len it ) = ( len ( ComSign A)) & for n st n in ( dom it ) holds (it . n) = [[:( ProdOp (A,n)):]];

      existence

      proof

        set f = ( ComSign A);

        defpred P[ Nat, set] means $2 = [[:( ProdOp (A,$1)):]];

        

         A1: for k be Nat st k in ( Seg ( len f)) holds ex x be Element of ( PFuncs ((( product ( Carrier A)) * ),( product ( Carrier A)))) st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len f));

          reconsider a = [[:( ProdOp (A,k)):]] as Element of ( PFuncs ((( product ( Carrier A)) * ),( product ( Carrier A)))) by PARTFUN1: 45;

          take a;

          thus thesis;

        end;

        consider p be FinSequence of ( PFuncs ((( product ( Carrier A)) * ),( product ( Carrier A)))) such that

         A2: ( dom p) = ( Seg ( len f)) & for k be Nat st k in ( Seg ( len f)) holds P[k, (p . k)] from FINSEQ_1:sch 5( A1);

        reconsider p as PFuncFinSequence of ( product ( Carrier A));

        take p;

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

        let n;

        assume n in ( dom p);

        hence thesis by A2;

      end;

      uniqueness

      proof

        let x,y be PFuncFinSequence of ( product ( Carrier A));

        assume that

         A3: ( len x) = ( len ( ComSign A)) and

         A4: for n st n in ( dom x) holds (x . n) = [[:( ProdOp (A,n)):]] and

         A5: ( len y) = ( len ( ComSign A)) and

         A6: for n st n in ( dom y) holds (y . n) = [[:( ProdOp (A,n)):]];

        

         A7: ( dom x) = ( Seg ( len ( ComSign A))) by A3, FINSEQ_1:def 3;

        now

          let n be Nat;

          assume n in ( dom x);

          then n in ( dom y) & (x . n) = [[:( ProdOp (A,n)):]] by A4, A5, A7, FINSEQ_1:def 3;

          hence (x . n) = (y . n) by A6;

        end;

        hence thesis by A3, A5, FINSEQ_2: 9;

      end;

    end

    definition

      let J be non empty set, A be equal-signature Univ_Alg-yielding ManySortedSet of J;

      :: PRALG_1:def25

      func ProdUnivAlg A -> strict Universal_Algebra equals UAStr (# ( product ( Carrier A)), ( ProdOpSeq A) #);

      coherence

      proof

        set j = the Element of J;

        set ua = UAStr (# ( product ( Carrier A)), ( ProdOpSeq A) #), pr = ( product ( Carrier A));

        for n be Nat, h be PartFunc of (pr * ), pr st n in ( dom the charact of ua) & h = (the charact of ua . n) holds h is quasi_total

        proof

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

          assume that

           A1: n in ( dom the charact of ua) and

           A2: (the charact of ua . n) = h;

          (the charact of ua . n) = [[:( ProdOp (A,n)):]] by A1, Def22;

          hence thesis by A2;

        end;

        then

         A3: the charact of ua is quasi_total;

        for n be Nat, h be PartFunc of (pr * ), pr st n in ( dom the charact of ua) & h = (the charact of ua . n) holds h is homogeneous

        proof

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

          assume that

           A4: n in ( dom the charact of ua) and

           A5: (the charact of ua . n) = h;

          (the charact of ua . n) = [[:( ProdOp (A,n)):]] by A4, Def22;

          hence thesis by A5;

        end;

        then

         A6: the charact of ua is homogeneous;

        for n be object st n in ( dom the charact of ua) holds (the charact of ua . n) is non empty

        proof

          let n be object;

          assume

           A7: n in ( dom the charact of ua);

          then

          reconsider n9 = n as Element of NAT ;

          (the charact of ua . n) = [[:( ProdOp (A,n9)):]] by A7, Def22;

          hence thesis;

        end;

        then

         A8: the charact of ua is non-empty by FUNCT_1:def 9;

        ( len the charact of ua) = ( len ( ComSign A)) by Def22

        .= ( len ( signature (A . j))) by Def14

        .= ( len the charact of (A . j)) by UNIALG_1:def 4;

        then the charact of ua <> {} ;

        hence thesis by A3, A6, A8, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;

      end;

    end