msualg_1.miz



    begin

    reserve i for object;

    begin

    definition

      struct ( 2-sorted) ManySortedSign (# the carrier, carrier' -> set,

the Arity -> Function of the carrier', ( the carrier * ),

the ResultSort -> Function of the carrier', the carrier #)

       attr strict strict;

    end

    registration

      cluster void strict non empty for ManySortedSign;

      existence

      proof

        reconsider g = ( {} --> {} ) as Function of {} , { {} };

        reconsider f = ( {} --> {} ) as Function of {} , ( { {} } * );

        take ManySortedSign (# { {} }, {} , f, g #);

        thus thesis;

      end;

      cluster non void strict non empty for ManySortedSign;

      existence

      proof

         {} in ( { {} } * ) by FINSEQ_1: 49;

        then

        reconsider f = ( { {} } --> {} ) as Function of { {} }, ( { {} } * ) by FUNCOP_1: 46;

        reconsider g = ( { {} } --> {} ) as Function of { {} }, { {} };

        take ManySortedSign (# { {} }, { {} }, f, g #);

        thus thesis;

      end;

    end

    reserve S for non empty ManySortedSign;

    definition

      let S;

      mode SortSymbol of S is Element of S;

      mode OperSymbol of S is Element of the carrier' of S;

    end

    definition

      let S be non void non empty ManySortedSign;

      let o be OperSymbol of S;

      :: MSUALG_1:def1

      func the_arity_of o -> Element of (the carrier of S * ) equals (the Arity of S . o);

      coherence ;

      :: MSUALG_1:def2

      func the_result_sort_of o -> Element of S equals (the ResultSort of S . o);

      coherence ;

    end

    begin

    definition

      let S be 1-sorted;

      struct many-sorted over S (# the Sorts -> ManySortedSet of the carrier of S #)

       attr strict strict;

    end

    definition

      let S;

      struct ( many-sorted over S) MSAlgebra over S (# the Sorts -> ManySortedSet of the carrier of S,

the Charact -> ManySortedFunction of (( the Sorts # ) * the Arity of S), ( the Sorts * the ResultSort of S) #)

       attr strict strict;

    end

    definition

      let S be 1-sorted;

      let A be many-sorted over S;

      :: MSUALG_1:def3

      attr A is non-empty means

      : Def3: the Sorts of A is non-empty;

    end

    registration

      let S;

      cluster strict non-empty for MSAlgebra over S;

      existence

      proof

        reconsider s = (the carrier of S --> { 0 }) as ManySortedSet of the carrier of S;

        set o = the ManySortedFunction of ((s # ) * the Arity of S), (s * the ResultSort of S);

        take MSAlgebra (# s, o #);

        thus MSAlgebra (# s, o #) is strict;

        let i be object;

        assume i in the carrier of S;

        hence thesis;

      end;

    end

    registration

      let S be 1-sorted;

      cluster strict non-empty for many-sorted over S;

      existence

      proof

        reconsider s = (the carrier of S --> { 0 }) as ManySortedSet of the carrier of S;

        take many-sorted (# s #);

        thus many-sorted (# s #) is strict;

        let i be object;

        assume i in the carrier of S;

        hence thesis;

      end;

    end

    registration

      let S be 1-sorted;

      let A be non-empty many-sorted over S;

      cluster the Sorts of A -> non-empty;

      coherence by Def3;

    end

    registration

      let S;

      let A be non-empty MSAlgebra over S;

      cluster -> non empty for Component of the Sorts of A;

      coherence

      proof

        let C be Component of the Sorts of A;

        ex i be object st i in the carrier of S & C = (the Sorts of A . i) by PBOOLE: 138;

        hence thesis;

      end;

      cluster -> non empty for Component of (the Sorts of A # );

      coherence

      proof

        let C be Component of (the Sorts of A # );

        ex i be object st i in (the carrier of S * ) & C = ((the Sorts of A # ) . i) by PBOOLE: 138;

        hence thesis;

      end;

    end

    definition

      let S be non void non empty ManySortedSign;

      let o be OperSymbol of S;

      let A be MSAlgebra over S;

      :: MSUALG_1:def4

      func Args (o,A) -> Component of (the Sorts of A # ) equals (((the Sorts of A # ) * the Arity of S) . o);

      coherence

      proof

        o in the carrier' of S;

        then o in ( dom ((the Sorts of A # ) * the Arity of S)) by PARTFUN1:def 2;

        then (((the Sorts of A # ) * the Arity of S) . o) in ( rng ((the Sorts of A # ) * the Arity of S)) by FUNCT_1:def 3;

        hence thesis by FUNCT_1: 14;

      end;

      correctness ;

      :: MSUALG_1:def5

      func Result (o,A) -> Component of the Sorts of A equals ((the Sorts of A * the ResultSort of S) . o);

      coherence

      proof

        o in the carrier' of S;

        then o in ( dom (the Sorts of A * the ResultSort of S)) by PARTFUN1:def 2;

        then ((the Sorts of A * the ResultSort of S) . o) in ( rng (the Sorts of A * the ResultSort of S)) by FUNCT_1:def 3;

        hence thesis by FUNCT_1: 14;

      end;

      correctness ;

    end

    definition

      let S be non void non empty ManySortedSign;

      let o be OperSymbol of S;

      let A be MSAlgebra over S;

      :: MSUALG_1:def6

      func Den (o,A) -> Function of ( Args (o,A)), ( Result (o,A)) equals (the Charact of A . o);

      coherence by PBOOLE:def 15;

    end

    theorem :: MSUALG_1:1

    for S be non void non empty ManySortedSign, o be OperSymbol of S, A be non-empty MSAlgebra over S holds ( Den (o,A)) is non empty;

    begin

    reserve D for non empty set,

n for Nat;

    

     Lm1: for h be homogeneous quasi_total non empty PartFunc of (D * ), D holds ( dom h) = (( arity h) -tuples_on D)

    proof

      let h be homogeneous quasi_total non empty PartFunc of (D * ), D;

      set x0 = the Element of ( dom h);

      

       A1: x0 in ( dom h);

      

       A2: ( dom h) c= (D * ) by RELAT_1:def 18;

      then

      reconsider x0 as FinSequence of D by A1, FINSEQ_1:def 11;

      thus ( dom h) c= (( arity h) -tuples_on D)

      proof

        let x be object;

        assume

         A3: x in ( dom h);

        then

        reconsider f = x as FinSequence of D by A2, FINSEQ_1:def 11;

        

         A4: f is Element of (( len f) -tuples_on D) by FINSEQ_2: 92;

        ( len f) = ( arity h) by A3, MARGREL1:def 25;

        hence thesis by A4;

      end;

      let x be object;

      assume x in (( arity h) -tuples_on D);

      then

      reconsider f = x as Element of (( arity h) -tuples_on D);

      ( len x0) = ( arity h) by MARGREL1:def 25

      .= ( len f) by CARD_1:def 7;

      hence thesis by MARGREL1:def 22;

    end;

    theorem :: MSUALG_1:2

    

     Th2: for C be set, A,B be non empty set, F be PartFunc of C, A, G be Function of A, B holds (G * F) is Function of ( dom F), B

    proof

      let C be set;

      let A,B be non empty set;

      let F be PartFunc of C, A;

      let G be Function of A, B;

      ( dom G) = A by FUNCT_2:def 1;

      then ( rng F) c= ( dom G) by RELAT_1:def 19;

      then

       A1: ( dom (G * F)) = ( dom F) by RELAT_1: 27;

      ( rng (G * F)) c= B by RELAT_1:def 19;

      hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

    end;

    theorem :: MSUALG_1:3

    

     Th3: for h be homogeneous quasi_total non empty PartFunc of (D * ), D holds ( dom h) = ( Funcs (( Seg ( arity h)),D))

    proof

      let h be homogeneous quasi_total non empty PartFunc of (D * ), D;

      

      thus ( dom h) = (( arity h) -tuples_on D) by Lm1

      .= ( Funcs (( Seg ( arity h)),D)) by FINSEQ_2: 93;

    end;

    theorem :: MSUALG_1:4

    

     Th4: for A be Universal_Algebra holds ( signature A) is non empty

    proof

      let A be Universal_Algebra;

      ( len the charact of A) <> 0 ;

      then ( len ( signature A)) <> 0 by UNIALG_1:def 4;

      hence thesis;

    end;

    begin

    definition

      let IT be ManySortedSign;

      :: MSUALG_1:def7

      attr IT is segmental means

      : Def7: ex n st the carrier' of IT = ( Seg n);

    end

    theorem :: MSUALG_1:5

    

     Th5: for S be non empty ManySortedSign st S is trivial holds for A be MSAlgebra over S, c1,c2 be Component of the Sorts of A holds c1 = c2

    proof

      let S be non empty ManySortedSign such that

       A1: S is trivial;

      let A be MSAlgebra over S, c1,c2 be Component of the Sorts of A;

      (ex i1 be object st i1 in the carrier of S & c1 = (the Sorts of A . i1)) & ex i2 be object st i2 in the carrier of S & c2 = (the Sorts of A . i2) by PBOOLE: 138;

      hence thesis by A1;

    end;

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

    

     Lm2: for A be Universal_Algebra holds for f be Function of ( dom ( signature A)), ( { 0 } * ) holds ManySortedSign (# { 0 }, ( dom ( signature A)), f, (( dom ( signature A)) --> z) #) is segmental1 -element non void strict

    proof

      let A be Universal_Algebra;

      let f be Function of ( dom ( signature A)), ( { 0 } * );

      set S = ManySortedSign (# { 0 }, ( dom ( signature A)), f, (( dom ( signature A)) --> z) #);

      

       A1: S is segmental

      proof

        take ( len ( signature A));

        thus thesis by FINSEQ_1:def 3;

      end;

      ( signature A) <> {} by Th4;

      hence thesis by A1;

    end;

    registration

      cluster segmental non void strict1 -element for ManySortedSign;

      existence

      proof

        set A = the Universal_Algebra;

        reconsider f = (( *--> 0 ) * ( signature A)) as Function of ( dom ( signature A)), ( { 0 } * ) by Th2;

         ManySortedSign (# { 0 }, ( dom ( signature A)), f, (( dom ( signature A)) --> z) #) is segmental non void strict1 -element by Lm2;

        hence thesis;

      end;

    end

    definition

      let A be Universal_Algebra;

      :: MSUALG_1:def8

      func MSSign A -> non void strict segmental trivial ManySortedSign means

      : Def8: the carrier of it = { 0 } & the carrier' of it = ( dom ( signature A)) & the Arity of it = (( *--> 0 ) * ( signature A)) & the ResultSort of it = (( dom ( signature A)) --> 0 );

      correctness

      proof

        reconsider f = (( *--> 0 ) * ( signature A)) as Function of ( dom ( signature A)), ( { 0 } * ) by Th2;

         ManySortedSign (# { 0 }, ( dom ( signature A)), f, (( dom ( signature A)) --> z) #) is segmental trivial non void strict by Lm2;

        hence thesis;

      end;

    end

    registration

      let A be Universal_Algebra;

      cluster ( MSSign A) -> 1 -element;

      coherence by Def8;

    end

    definition

      let A be Universal_Algebra;

      :: MSUALG_1:def9

      func MSSorts A -> non-empty ManySortedSet of the carrier of ( MSSign A) equals ( 0 .--> the carrier of A);

      coherence

      proof

        set M = ( { 0 } --> the carrier of A);

        the carrier of ( MSSign A) = { 0 } by Def8;

        then

        reconsider M as ManySortedSet of the carrier of ( MSSign A);

        M is non-empty;

        hence thesis;

      end;

      correctness ;

    end

    definition

      let A be Universal_Algebra;

      :: MSUALG_1:def10

      func MSCharact A -> ManySortedFunction of ((( MSSorts A) # ) * the Arity of ( MSSign A)), (( MSSorts A) * the ResultSort of ( MSSign A)) equals the charact of A;

      coherence

      proof

        

         A1: the ResultSort of ( MSSign A) = (( dom ( signature A)) --> 0 ) by Def8;

        reconsider OS = the carrier' of ( MSSign A) as non empty set;

        reconsider DO = ((( MSSorts A) # ) * the Arity of ( MSSign A)), RO = (( MSSorts A) * the ResultSort of ( MSSign A)) as ManySortedSet of OS;

        

         A2: the carrier' of ( MSSign A) = ( dom ( signature A)) by Def8;

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

        then

         A3: ( dom the charact of A) = OS by A2, FINSEQ_3: 29;

        then

        reconsider O = the charact of A as ManySortedSet of OS by PARTFUN1:def 2, RELAT_1:def 18;

        

         A4: the Arity of ( MSSign A) = (( *--> 0 ) * ( signature A)) by Def8;

        reconsider O as ManySortedFunction of OS;

        

         A5: the carrier of ( MSSign A) = { 0 } by Def8;

        O is ManySortedFunction of DO, RO

        proof

          set D = the carrier of A;

          let i;

          reconsider M = ( 0 .--> D) as ManySortedSet of { 0 };

          

           A6: 0 in { 0 } by TARSKI:def 1;

          assume

           A7: i in OS;

          then

          reconsider n = i as Nat by A2;

          reconsider h = (O . n) as homogeneous quasi_total non empty PartFunc of (D * ), D by A3, A7, MARGREL1:def 24, UNIALG_1: 1;

          n in ( dom (( dom ( signature A)) --> 0 )) by A2, A7;

          

          then (RO . i) = (( MSSorts A) . ((( dom ( signature A)) --> 0 ) . n)) by A1, FUNCT_1: 13

          .= (( { 0 } --> the carrier of A) . 0 ) by A2, A7, FUNCOP_1: 7

          .= the carrier of A by A6, FUNCOP_1: 7;

          then

           A8: ( rng h) c= (RO . i) by RELAT_1:def 19;

          reconsider o = i as Element of OS by A7;

          (DO . i) = ((((( MSSorts A) # ) * ( *--> 0 )) * ( signature A)) . n) by A4, RELAT_1: 36

          .= (((M # ) * ( *--> 0 )) . (( signature A) . n)) by A5, A2, A7, FUNCT_1: 13

          .= (((M # ) * ( *--> 0 )) . ( arity h)) by A2, A7, UNIALG_1:def 4

          .= ( Funcs (( Seg ( arity h)),D)) by FINSEQ_2: 145

          .= ( dom (O . o)) by Th3;

          hence thesis by A8, FUNCT_2:def 1, RELSET_1: 4;

        end;

        hence thesis;

      end;

      correctness ;

    end

    definition

      let A be Universal_Algebra;

      :: MSUALG_1:def11

      func MSAlg A -> strict MSAlgebra over ( MSSign A) equals MSAlgebra (# ( MSSorts A), ( MSCharact A) #);

      correctness ;

    end

    registration

      let A be Universal_Algebra;

      cluster ( MSAlg A) -> non-empty;

      coherence ;

    end

    definition

      let MS be 1 -element ManySortedSign;

      let A be MSAlgebra over MS;

      :: MSUALG_1:def12

      func the_sort_of A -> set means

      : Def12: it is Component of the Sorts of A;

      existence

      proof

        set c = the Component of the Sorts of A;

        take c;

        thus thesis;

      end;

      uniqueness by Th5;

    end

    registration

      let MS be 1 -element ManySortedSign;

      let A be non-empty MSAlgebra over MS;

      cluster ( the_sort_of A) -> non empty;

      coherence

      proof

        ( the_sort_of A) is Component of the Sorts of A by Def12;

        hence thesis;

      end;

    end

    theorem :: MSUALG_1:6

    

     Th6: for MS be segmental non void1 -element ManySortedSign, i be OperSymbol of MS, A be non-empty MSAlgebra over MS holds ( Args (i,A)) = (( len ( the_arity_of i)) -tuples_on ( the_sort_of A))

    proof

      let MS be segmental non void1 -element ManySortedSign, i be OperSymbol of MS, A be non-empty MSAlgebra over MS;

      set m = ( len ( the_arity_of i));

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

      

      then

       A1: ( Args (i,A)) = ((the Sorts of A # ) . (the Arity of MS . i)) by FUNCT_1: 13

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

      

       A2: ( rng ( the_arity_of i)) c= the carrier of MS by FINSEQ_1:def 4;

      then ( rng ( the_arity_of i)) c= ( dom the Sorts of A) by PARTFUN1:def 2;

      then

       A3: ( dom (the Sorts of A * ( the_arity_of i))) = ( dom ( the_arity_of i)) by RELAT_1: 27;

      

       A4: ex n be Nat st ( dom ( the_arity_of i)) = ( Seg n) by FINSEQ_1:def 2;

      thus ( Args (i,A)) c= (m -tuples_on ( the_sort_of A))

      proof

        let x be object;

        assume x in ( Args (i,A));

        then

        consider g be Function such that

         A5: x = g and

         A6: ( dom g) = ( dom (the Sorts of A * ( the_arity_of i))) and

         A7: for j be object st j in ( dom (the Sorts of A * ( the_arity_of i))) holds (g . j) in ((the Sorts of A * ( the_arity_of i)) . j) by A1, CARD_3:def 5;

        reconsider p = g as FinSequence by A4, A3, A6, FINSEQ_1:def 2;

        ( rng p) c= ( the_sort_of A)

        proof

          let j be object;

          assume j in ( rng p);

          then

          consider u be object such that

           A8: u in ( dom g) and

           A9: (p . u) = j by FUNCT_1:def 3;

          (( the_arity_of i) . u) in ( rng ( the_arity_of i)) by A3, A6, A8, FUNCT_1:def 3;

          then

           A10: (the Sorts of A . (( the_arity_of i) . u)) is Component of the Sorts of A by A2, PBOOLE: 139;

          (g . u) in ((the Sorts of A * ( the_arity_of i)) . u) by A6, A7, A8;

          then (g . u) in (the Sorts of A . (( the_arity_of i) . u)) by A3, A6, A8, FUNCT_1: 13;

          hence thesis by A9, A10, Def12;

        end;

        then

         A11: p is FinSequence of ( the_sort_of A) by FINSEQ_1:def 4;

        ( len p) = m by A3, A6, FINSEQ_3: 29;

        then x is Element of (m -tuples_on ( the_sort_of A)) by A5, A11, FINSEQ_2: 92;

        hence thesis;

      end;

      let x be object;

      assume x in (m -tuples_on ( the_sort_of A));

      then x in ( Funcs (( Seg m),( the_sort_of A))) by FINSEQ_2: 93;

      then

      consider g be Function such that

       A12: x = g and

       A13: ( dom g) = ( Seg m) and

       A14: ( rng g) c= ( the_sort_of A) by FUNCT_2:def 2;

      

       A15: ( dom g) = ( dom (the Sorts of A * ( the_arity_of i))) by A3, A13, FINSEQ_1:def 3;

      now

        let x be object;

        assume

         A16: x in ( dom (the Sorts of A * ( the_arity_of i)));

        then (( the_arity_of i) . x) in ( rng ( the_arity_of i)) by A3, FUNCT_1:def 3;

        then

         A17: (the Sorts of A . (( the_arity_of i) . x)) is Component of the Sorts of A by A2, PBOOLE: 139;

        (g . x) in ( rng g) by A15, A16, FUNCT_1:def 3;

        then (g . x) in ( the_sort_of A) by A14;

        then (g . x) in (the Sorts of A . (( the_arity_of i) . x)) by A17, Def12;

        hence (g . x) in ((the Sorts of A * ( the_arity_of i)) . x) by A3, A16, FUNCT_1: 13;

      end;

      hence thesis by A1, A12, A15, CARD_3: 9;

    end;

    theorem :: MSUALG_1:7

    

     Th7: for MS be segmental non void1 -element ManySortedSign, i be OperSymbol of MS, A be non-empty MSAlgebra over MS holds ( Args (i,A)) c= (( the_sort_of A) * )

    proof

      let MS be segmental non void1 -element ManySortedSign, i be OperSymbol of MS, A be non-empty MSAlgebra over MS;

      ( Args (i,A)) = (( len ( the_arity_of i)) -tuples_on ( the_sort_of A)) by Th6;

      hence thesis by FINSEQ_2: 142;

    end;

    theorem :: MSUALG_1:8

    

     Th8: for MS be segmental non void1 -element ManySortedSign, A be non-empty MSAlgebra over MS holds the Charact of A is FinSequence of ( PFuncs ((( the_sort_of A) * ),( the_sort_of A)))

    proof

      let MS be segmental non void1 -element ManySortedSign, A be non-empty MSAlgebra over MS;

      

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

      ex n be Element of NAT st the carrier' of MS = ( Seg n)

      proof

        consider n such that

         A2: the carrier' of MS = ( Seg n) by Def7;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      then

      reconsider f = the Charact of A as FinSequence by A1, FINSEQ_1:def 2;

      f is FinSequence of ( PFuncs ((( the_sort_of A) * ),( the_sort_of A)))

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider i be object such that

         A3: i in the carrier' of MS and

         A4: (f . i) = x by A1, FUNCT_1:def 3;

        reconsider i as OperSymbol of MS by A3;

        

         A5: (the Sorts of A . (the ResultSort of MS . i)) is Component of the Sorts of A by PBOOLE: 139;

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

        

        then ((the Sorts of A * the ResultSort of MS) . i) = (the Sorts of A . (the ResultSort of MS . i)) by FUNCT_1: 13

        .= ( the_sort_of A) by A5, Def12;

        then

         A6: x is Function of ( Args (i,A)), ( the_sort_of A) by A4, PBOOLE:def 15;

        ( Args (i,A)) c= (( the_sort_of A) * ) by Th7;

        then x is PartFunc of (( the_sort_of A) * ), ( the_sort_of A) by A6, RELSET_1: 7;

        hence thesis by PARTFUN1: 45;

      end;

      hence thesis;

    end;

    definition

      let MS be segmental non void1 -element ManySortedSign;

      let A be non-empty MSAlgebra over MS;

      :: MSUALG_1:def13

      func the_charact_of A -> PFuncFinSequence of ( the_sort_of A) equals the Charact of A;

      coherence by Th8;

    end

    reserve MS for segmental non void1 -element ManySortedSign,

A for non-empty MSAlgebra over MS,

h for PartFunc of (( the_sort_of A) * ), ( the_sort_of A),

x,y for FinSequence of ( the_sort_of A);

    definition

      let MS, A;

      :: MSUALG_1:def14

      func 1-Alg A -> non-empty strict Universal_Algebra equals UAStr (# ( the_sort_of A), ( the_charact_of A) #);

      coherence

      proof

        

         A1: ( the_charact_of A) is quasi_total

        proof

          let n, h such that

           A2: n in ( dom ( the_charact_of A)) and

           A3: h = (( the_charact_of A) . n);

          reconsider o = n as OperSymbol of MS by A2, PARTFUN1:def 2;

          let x, y such that

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

           A5: x in ( dom h);

          

           A6: (((the Sorts of A # ) * the Arity of MS) . o) = ( Args (o,A));

          h is Function of (((the Sorts of A # ) * the Arity of MS) . o), ((the Sorts of A * the ResultSort of MS) . o) by A3, PBOOLE:def 15;

          

          then

           A7: ( dom h) = (((the Sorts of A # ) * the Arity of MS) . o) by FUNCT_2:def 1

          .= (( len ( the_arity_of o)) -tuples_on ( the_sort_of A)) by A6, Th6;

          then ( len y) = ( len ( the_arity_of o)) by A4, A5, CARD_1:def 7;

          then y is Element of ( dom h) by A7, FINSEQ_2: 92;

          hence thesis by A5;

        end;

        

         A8: ( the_charact_of A) is homogeneous

        proof

          let n, h such that

           A9: n in ( dom ( the_charact_of A)) and

           A10: h = (( the_charact_of A) . n);

          reconsider o = n as OperSymbol of MS by A9, PARTFUN1:def 2;

          thus ( dom h) is with_common_domain

          proof

            let x,y be FinSequence such that

             A11: x in ( dom h) and

             A12: y in ( dom h);

            

             A13: (((the Sorts of A # ) * the Arity of MS) . o) = ( Args (o,A));

            h is Function of (((the Sorts of A # ) * the Arity of MS) . o), ((the Sorts of A * the ResultSort of MS) . o) by A10, PBOOLE:def 15;

            

            then

             A14: ( dom h) = (((the Sorts of A # ) * the Arity of MS) . o) by FUNCT_2:def 1

            .= (( len ( the_arity_of o)) -tuples_on ( the_sort_of A)) by A13, Th6;

            

            hence ( len x) = ( len ( the_arity_of o)) by A11, CARD_1:def 7

            .= ( len y) by A12, A14, CARD_1:def 7;

          end;

        end;

        ( the_charact_of A) is non-empty

        proof

          let n be object;

          assume n in ( dom ( the_charact_of A));

          then

          reconsider o = n as OperSymbol of MS by PARTFUN1:def 2;

          set h = (( the_charact_of A) . n);

          h = ( Den (o,A));

          hence thesis;

        end;

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

      end;

      correctness ;

    end

    theorem :: MSUALG_1:9

    for A be strict Universal_Algebra holds A = ( 1-Alg ( MSAlg A))

    proof

      let A be strict Universal_Algebra;

      the carrier of A in {the carrier of A} by TARSKI:def 1;

      then the carrier of A in ( rng the Sorts of ( MSAlg A)) by FUNCOP_1: 8;

      hence thesis by Def12;

    end;

    theorem :: MSUALG_1:10

    for A be Universal_Algebra holds for f be Function of ( dom ( signature A)), ( { 0 } * ) holds for z be Element of { 0 } st f = (( *--> 0 ) * ( signature A)) holds ( MSSign A) = ManySortedSign (# { 0 }, ( dom ( signature A)), f, (( dom ( signature A)) --> z) #)

    proof

      let A be Universal_Algebra;

      let f be Function of ( dom ( signature A)), ( { 0 } * );

      let z be Element of { 0 };

      

       A1: the carrier' of ( MSSign A) = ( dom ( signature A)) & the Arity of ( MSSign A) = (( *--> 0 ) * ( signature A)) by Def8;

      z = 0 & the carrier of ( MSSign A) = { 0 } by Def8, TARSKI:def 1;

      hence thesis by A1, Def8;

    end;