mssublat.miz



    begin

    reserve a for set,

i for Nat;

    theorem :: MSSUBLAT:1

    

     Th1: (( *--> a) . 0 ) = {}

    proof

      

      thus (( *--> a) . 0 ) = ( 0 |-> a) by FINSEQ_2:def 6

      .= {} ;

    end;

    theorem :: MSSUBLAT:2

    (( *--> a) . 1) = <*a*>

    proof

      

      thus (( *--> a) . 1) = (1 |-> a) by FINSEQ_2:def 6

      .= <*a*> by FINSEQ_2: 59;

    end;

    theorem :: MSSUBLAT:3

    (( *--> a) . 2) = <*a, a*>

    proof

      

      thus (( *--> a) . 2) = (2 |-> a) by FINSEQ_2:def 6

      .= <*a, a*> by FINSEQ_2: 61;

    end;

    theorem :: MSSUBLAT:4

    (( *--> a) . 3) = <*a, a, a*>

    proof

      

      thus (( *--> a) . 3) = (3 |-> a) by FINSEQ_2:def 6

      .= <*a, a, a*> by FINSEQ_2: 62;

    end;

    theorem :: MSSUBLAT:5

    

     Th5: for f be FinSequence of { 0 } holds f = (i |-> 0 ) iff ( len f) = i

    proof

      let f be FinSequence of { 0 };

      thus f = (i |-> 0 ) implies ( len f) = i by CARD_1:def 7;

      assume ( len f) = i;

      then

       A1: ( dom f) = ( Seg i) by FINSEQ_1:def 3;

      per cases ;

        suppose

         A2: ( Seg i) = {} ;

        

        hence f = {} by A1

        .= ( 0 |-> 0 )

        .= (i |-> 0 ) by A2;

      end;

        suppose

         A3: ( Seg i) <> {} ;

        ( rng f) c= { 0 } by FINSEQ_1:def 4;

        then ( rng f) = { 0 } or ( rng f) = {} by ZFMISC_1: 33;

        hence thesis by A1, A3, FUNCOP_1: 9, RELAT_1: 42;

      end;

    end;

    theorem :: MSSUBLAT:6

    

     Th6: for f be FinSequence st f = (( *--> 0 ) . i) holds ( len f) = i

    proof

      let p be FinSequence;

      assume

       A1: p = (( *--> 0 ) . i);

      p = (i |-> 0 ) by A1, FINSEQ_2:def 6;

      hence thesis by CARD_1:def 7;

    end;

    begin

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

    theorem :: MSSUBLAT:7

    

     Th7: for U1,U2 be Universal_Algebra st U1 is SubAlgebra of U2 holds ( MSSign U1) = ( MSSign U2)

    proof

      let U1,U2 be Universal_Algebra;

      set ff2 = (( dom ( signature U1)) --> z), gg2 = (( dom ( signature U2)) --> z);

      reconsider ff1 = (( *--> 0 ) * ( signature U1)) as Function of ( dom ( signature U1)), ( { 0 } * ) by MSUALG_1: 2;

      reconsider gg1 = (( *--> 0 ) * ( signature U2)) as Function of ( dom ( signature U2)), ( { 0 } * ) by MSUALG_1: 2;

      assume U1 is SubAlgebra of U2;

      then

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

      

       A2: ( MSSign U1) = ManySortedSign (# { 0 }, ( dom ( signature U1)), ff1, ff2 #) & ( MSSign U2) = ManySortedSign (# { 0 }, ( dom ( signature U2)), gg1, gg2 #) by MSUALG_1: 10;

      thus thesis by A1, A2;

    end;

    theorem :: MSSUBLAT:8

    

     Th8: for U1,U2 be Universal_Algebra st U1 is SubAlgebra of U2 holds for B be MSSubset of ( MSAlg U2) st B = the Sorts of ( MSAlg U1) holds for o be OperSymbol of ( MSSign U2) holds for a be OperSymbol of ( MSSign U1) st a = o holds ( Den (a,( MSAlg U1))) = (( Den (o,( MSAlg U2))) | ( Args (a,( MSAlg U1))))

    proof

      let U1,U2 be Universal_Algebra such that

       A1: U1 is SubAlgebra of U2;

      

       A2: ( MSSign U1) = ( MSSign U2) by A1, Th7;

      

       A3: ( MSSign U1) = ( MSSign U2) by A1, Th7;

      let B be MSSubset of ( MSAlg U2) such that

       A4: B = the Sorts of ( MSAlg U1);

      let o be OperSymbol of ( MSSign U2);

      reconsider a = o as Element of the carrier' of ( MSSign U1) by A1, Th7;

      set X = ( Args (a,( MSAlg U1)));

      set Y = ( dom ( Den (a,( MSAlg U1))));

      the Sorts of ( MSAlg U2) is MSSubset of ( MSAlg U2) & B c= the Sorts of ( MSAlg U2) by PBOOLE:def 18;

      then

       A5: (((B # ) * the Arity of ( MSSign U1)) . a) c= (((the Sorts of ( MSAlg U2) # ) * the Arity of ( MSSign U2)) . o) by A3, MSUALG_2: 2;

      ( dom ( Den (o,( MSAlg U2)))) = ( Args (o,( MSAlg U2))) & ( Args (o,( MSAlg U2))) = (((the Sorts of ( MSAlg U2) # ) * the Arity of ( MSSign U2)) . o) by FUNCT_2:def 1, MSUALG_1:def 4;

      then ( Args (a,( MSAlg U1))) c= ( dom ( Den (o,( MSAlg U2)))) by A4, A2, A5, MSUALG_1:def 4;

      then ( dom (( Den (o,( MSAlg U2))) | ( Args (a,( MSAlg U1))))) = ( Args (a,( MSAlg U1))) by RELAT_1: 62;

      then ( dom (( Den (o,( MSAlg U2))) | ( Args (a,( MSAlg U1))))) = ( dom ( Den (a,( MSAlg U1)))) by FUNCT_2:def 1;

      then

       A6: Y = (( dom ( Den (o,( MSAlg U2)))) /\ X) by RELAT_1: 61;

      for x be object st x in Y holds (( Den (o,( MSAlg U2))) . x) = (( Den (a,( MSAlg U1))) . x)

      proof

        ( MSAlg U1) = MSAlgebra (# ( MSSorts U1), ( MSCharact U1) #) by MSUALG_1:def 11;

        then the Sorts of ( MSAlg U1) = ( 0 .--> the carrier of U1) by MSUALG_1:def 9;

        then ( rng the Sorts of ( MSAlg U1)) = {the carrier of U1} by FUNCOP_1: 8;

        then

         A7: the carrier of U1 is Component of the Sorts of ( MSAlg U1) by TARSKI:def 1;

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

        let x be object;

        

         A8: ( MSAlg U2) = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

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

        then

         A9: ( signature U1) = ( signature U2);

        assume x in Y;

        then x in X by A6, XBOOLE_0:def 4;

        then x in (( len ( the_arity_of a)) -tuples_on ( the_sort_of ( MSAlg U1))) by MSUALG_1: 6;

        then

         A10: x in (( len ( the_arity_of a)) -tuples_on the carrier of U1) by A7, MSUALG_1:def 12;

        reconsider gg1 = (( *--> 0 ) * ( signature U2)) as Function of ( dom ( signature U2)), ( { 0 } * ) by MSUALG_1: 2;

        set ff1 = (( *--> 0 ) * ( signature U1)), ff2 = (( dom ( signature U1)) --> z), gg2 = (( dom ( signature U2)) --> z);

        reconsider ff1 as Function of ( dom ( signature U1)), ( { 0 } * ) by MSUALG_1: 2;

        consider n be Nat such that

         A11: ( dom ( signature U2)) = ( Seg n) by FINSEQ_1:def 2;

        

         A12: ( MSSign U2) = ManySortedSign (# { 0 }, ( dom ( signature U2)), gg1, gg2 #) by MSUALG_1: 10;

        then

         A13: a in ( Seg n) by A11;

        

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

        .= ( Seg ( len ( signature U2))) by UNIALG_1:def 4

        .= ( dom ( signature U2)) by FINSEQ_1:def 3;

        then

        reconsider op = (the charact of U2 . a) as operation of U2 by A12, FUNCT_1:def 3;

        reconsider a as Element of NAT by A13;

        

         A15: ( rng ( signature U1)) c= NAT by FINSEQ_1:def 4;

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

        then

         A16: ( signature U1) = ( signature U2);

        then

         A17: (( signature U1) . a) in ( rng ( signature U1)) by A12, FUNCT_1:def 3;

        then

        reconsider sig = (( signature U1) . a) as Element of NAT by A15;

        ( dom ( *--> 0 )) = NAT by FUNCT_2:def 1;

        then ( MSSign U1) = ManySortedSign (# { 0 }, ( dom ( signature U1)), ff1, ff2 #) & a in ( dom (( *--> 0 ) * ( signature U1))) by A12, A16, A17, A15, FUNCT_1: 11, MSUALG_1: 10;

        then (the Arity of ( MSSign U1) . a) = (( *--> 0 ) . (( signature U1) . a)) by FUNCT_1: 12;

        then

         A18: (the Arity of ( MSSign U1) . a) = (sig |-> 0 ) by FINSEQ_2:def 6;

        reconsider ar = (the Arity of ( MSSign U1) . a) as FinSequence;

        x in (( len ar) -tuples_on the carrier of U1) by A10, MSUALG_1:def 1;

        then x in (sig -tuples_on the carrier of U1) by A18, CARD_1:def 7;

        then

         A19: x in (( arity op) -tuples_on the carrier of U1) by A12, A9, UNIALG_1:def 4;

        now

          let n be object;

          assume n in ( dom ( Opers (U2,cc)));

          then ( rng ( Opers (U2,cc))) c= ( PFuncs ((cc * ),cc)) & (( Opers (U2,cc)) . n) in ( rng ( Opers (U2,cc))) by FINSEQ_1:def 4, FUNCT_1:def 3;

          hence (( Opers (U2,cc)) . n) is Function by PARTFUN1: 46;

        end;

        then

        reconsider f = ( Opers (U2,cc)) as Function-yielding Function by FUNCOP_1:def 6;

        cc is opers_closed by A1, UNIALG_2:def 7;

        then

         A20: cc is_closed_on op;

        a in ( dom the charact of U2) by A12, A14;

        then

         A21: o in ( dom ( Opers (U2,cc))) by UNIALG_2:def 6;

        reconsider a as OperSymbol of ( MSSign U1);

        ( MSAlg U1) = MSAlgebra (# ( MSSorts U1), ( MSCharact U1) #) by MSUALG_1:def 11;

        

        then (( Den (a,( MSAlg U1))) . x) = ((( MSCharact U1) . o) . x) by MSUALG_1:def 6

        .= ((the charact of U1 . o) . x) by MSUALG_1:def 10

        .= ((f . o) . x) by A1, UNIALG_2:def 7

        .= ((op /. cc) . x) by A21, UNIALG_2:def 6

        .= ((op | (( arity op) -tuples_on cc)) . x) by A20, UNIALG_2:def 5

        .= ((the charact of U2 . o) . x) by A19, FUNCT_1: 49

        .= ((the Charact of ( MSAlg U2) . o) . x) by A8, MSUALG_1:def 10

        .= (( Den (o,( MSAlg U2))) . x) by MSUALG_1:def 6;

        hence thesis;

      end;

      hence thesis by A6, FUNCT_1: 46;

    end;

    theorem :: MSSUBLAT:9

    

     Th9: for U1,U2 be Universal_Algebra st U1 is SubAlgebra of U2 holds the Sorts of ( MSAlg U1) is MSSubset of ( MSAlg U2)

    proof

      let U1,U2 be Universal_Algebra;

      set gg1 = (( *--> 0 ) * ( signature U2)), gg2 = (( dom ( signature U2)) --> z);

      reconsider gg1 as Function of ( dom ( signature U2)), ( { 0 } * ) by MSUALG_1: 2;

      

       A1: ( MSSign U2) = ManySortedSign (# { 0 }, ( dom ( signature U2)), gg1, gg2 #) by MSUALG_1: 10;

      ( MSAlg U2) = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

      then

       A2: the Sorts of ( MSAlg U2) = ( 0 .--> the carrier of U2) by MSUALG_1:def 9;

      assume

       A3: U1 is SubAlgebra of U2;

      then ( MSSign U1) = ( MSSign U2) by Th7;

      then

      reconsider A = ( MSAlg U1) as non-empty MSAlgebra over ( MSSign U2);

      ( MSAlg U1) = MSAlgebra (# ( MSSorts U1), ( MSCharact U1) #) by MSUALG_1:def 11;

      then

       A4: the Sorts of A = ( 0 .--> the carrier of U1) by MSUALG_1:def 9;

      

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

      

       A6: the carrier of U1 is Subset of U2 by A3, UNIALG_2:def 7;

      the Sorts of A c= the Sorts of ( MSAlg U2)

      proof

        let i be object;

        assume i in the carrier of ( MSSign U2);

        then

         A7: i = 0 by A1, TARSKI:def 1;

        (the Sorts of A . 0 ) = the carrier of U1 & (the Sorts of ( MSAlg U2) . 0 ) = the carrier of U2 by A4, A2, A5, FUNCOP_1: 7;

        hence thesis by A6, A7;

      end;

      hence thesis by PBOOLE:def 18;

    end;

    theorem :: MSSUBLAT:10

    

     Th10: for U1,U2 be Universal_Algebra st U1 is SubAlgebra of U2 holds for B be MSSubset of ( MSAlg U2) st B = the Sorts of ( MSAlg U1) holds B is opers_closed

    proof

      let U1,U2 be Universal_Algebra such that

       A1: U1 is SubAlgebra of U2;

      let B be MSSubset of ( MSAlg U2) such that

       A2: B = the Sorts of ( MSAlg U1);

      let o be OperSymbol of ( MSSign U2);

      reconsider a = o as Element of the carrier' of ( MSSign U1) by A1, Th7;

      set S = ((B * the ResultSort of ( MSSign U2)) . a);

      S = ((the Sorts of ( MSAlg U1) * the ResultSort of ( MSSign U1)) . a) by A1, A2, Th7;

      then

       A3: S = ( Result (a,( MSAlg U1))) by MSUALG_1:def 5;

      set Z = ( rng (( Den (o,( MSAlg U2))) | (((B # ) * the Arity of ( MSSign U2)) . a)));

      ( MSSign U1) = ( MSSign U2) by A1, Th7;

      then ( rng ( Den (a,( MSAlg U1)))) c= ( Result (a,( MSAlg U1))) & Z = ( rng (( Den (o,( MSAlg U2))) | ( Args (a,( MSAlg U1))))) by A2, MSUALG_1:def 4, RELAT_1:def 19;

      then Z c= ( Result (a,( MSAlg U1))) by A1, A2, Th8;

      hence thesis by A3;

    end;

    theorem :: MSSUBLAT:11

    

     Th11: for U1,U2 be Universal_Algebra st U1 is SubAlgebra of U2 holds for B be MSSubset of ( MSAlg U2) st B = the Sorts of ( MSAlg U1) holds the Charact of ( MSAlg U1) = ( Opers (( MSAlg U2),B))

    proof

      let U1,U2 be Universal_Algebra such that

       A1: U1 is SubAlgebra of U2;

      let B be MSSubset of ( MSAlg U2);

      set f1 = the Charact of ( MSAlg U1), f2 = ( Opers (( MSAlg U2),B));

      the carrier' of ( MSSign U1) = the carrier' of ( MSSign U2)

      proof

        set ff1 = (( *--> 0 ) * ( signature U1)), ff2 = (( dom ( signature U1)) --> z), gg1 = (( *--> 0 ) * ( signature U2)), gg2 = (( dom ( signature U2)) --> z);

        reconsider ff1 as Function of ( dom ( signature U1)), ( { 0 } * ) by MSUALG_1: 2;

        reconsider gg1 as Function of ( dom ( signature U2)), ( { 0 } * ) by MSUALG_1: 2;

        

         A2: ( MSSign U2) = ManySortedSign (# { 0 }, ( dom ( signature U2)), gg1, gg2 #) by MSUALG_1: 10;

        (U1,U2) are_similar & ( MSSign U1) = ManySortedSign (# { 0 }, ( dom ( signature U1)), ff1, ff2 #) by A1, MSUALG_1: 10, UNIALG_2: 13;

        hence thesis by A2;

      end;

      then

      reconsider f1 as ManySortedSet of the carrier' of ( MSSign U2);

      assume

       A3: B = the Sorts of ( MSAlg U1);

      for x be object st x in the carrier' of ( MSSign U2) holds (f1 . x) = (f2 . x)

      proof

        let x be object;

        assume

         A4: x in the carrier' of ( MSSign U2);

        then

        reconsider y = x as OperSymbol of ( MSSign U2);

        reconsider x as OperSymbol of ( MSSign U1) by A1, A4, Th7;

        B is opers_closed by A1, A3, Th10;

        then (f2 . y) = (y /. B) & B is_closed_on y by MSUALG_2:def 8;

        then

         A5: (f2 . y) = (( Den (y,( MSAlg U2))) | (((B # ) * the Arity of ( MSSign U2)) . y)) by MSUALG_2:def 7;

        (((B # ) * the Arity of ( MSSign U1)) . x) = (((the Sorts of ( MSAlg U1) # ) * the Arity of ( MSSign U1)) . x) by A1, A3, Th7;

        then (f2 . y) = (( Den (y,( MSAlg U2))) | (((the Sorts of ( MSAlg U1) # ) * the Arity of ( MSSign U1)) . x)) by A1, A5, Th7;

        then (f1 . x) = ( Den (x,( MSAlg U1))) & (f2 . y) = (( Den (y,( MSAlg U2))) | ( Args (x,( MSAlg U1)))) by MSUALG_1:def 4, MSUALG_1:def 6;

        hence thesis by A1, A3, Th8;

      end;

      hence thesis by PBOOLE: 3;

    end;

    theorem :: MSSUBLAT:12

    

     Th12: for U1,U2 be Universal_Algebra st U1 is SubAlgebra of U2 holds ( MSAlg U1) is MSSubAlgebra of ( MSAlg U2)

    proof

      let U1,U2 be Universal_Algebra;

      assume

       A1: U1 is SubAlgebra of U2;

      then ( MSSign U1) = ( MSSign U2) by Th7;

      then

      reconsider A = ( MSAlg U1) as non-empty MSAlgebra over ( MSSign U2);

      A is MSSubAlgebra of ( MSAlg U2)

      proof

        thus the Sorts of A is MSSubset of ( MSAlg U2) by A1, Th9;

        let B be MSSubset of ( MSAlg U2);

        assume

         A2: B = the Sorts of A;

        hence B is opers_closed by A1, Th10;

        thus thesis by A1, A2, Th11;

      end;

      hence thesis;

    end;

    theorem :: MSSUBLAT:13

    

     Th13: for U1,U2 be Universal_Algebra st ( MSAlg U1) is MSSubAlgebra of ( MSAlg U2) holds the carrier of U1 is Subset of U2

    proof

      let U1,U2 be Universal_Algebra;

      set MU1 = ( MSAlg U1), MU2 = ( MSAlg U2);

      assume

       A1: MU1 is MSSubAlgebra of MU2;

      then

      reconsider MU1 as MSAlgebra over ( MSSign U2);

      reconsider C = the Sorts of MU1 as MSSubset of MU2 by A1, MSUALG_2:def 9;

      set gg1 = (( *--> 0 ) * ( signature U2)), gg2 = (( dom ( signature U2)) --> z);

      reconsider gg1 as Function of ( dom ( signature U2)), ( { 0 } * ) by MSUALG_1: 2;

      reconsider C1 = C as ManySortedSet of the carrier of ( MSSign U2);

      

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

      MU2 = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

      then

       A3: C1 c= ( MSSorts U2) by PBOOLE:def 18;

      ( MSSign U2) = ManySortedSign (# { 0 }, ( dom ( signature U2)), gg1, gg2 #) & ( MSSorts U2) = ( 0 .--> the carrier of U2) by MSUALG_1: 10, MSUALG_1:def 9;

      then MU1 = MSAlgebra (# ( MSSorts U1), ( MSCharact U1) #) & (C1 . 0 ) c= (( { 0 } --> the carrier of U2) . 0 ) by A3, MSUALG_1:def 11;

      then (( MSSorts U1) . 0 ) c= the carrier of U2 by A2, FUNCOP_1: 7;

      then (( 0 .--> the carrier of U1) . 0 ) c= the carrier of U2 by MSUALG_1:def 9;

      hence thesis by A2, FUNCOP_1: 7;

    end;

    theorem :: MSSUBLAT:14

    

     Th14: for U1,U2 be Universal_Algebra st ( MSAlg U1) is MSSubAlgebra of ( MSAlg U2) holds for B be non empty Subset of U2 st B = the carrier of U1 holds B is opers_closed

    proof

      let U1,U2 be Universal_Algebra;

      set MU1 = ( MSAlg U1), MU2 = ( MSAlg U2);

      

       A1: MU2 = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

      assume

       A2: MU1 is MSSubAlgebra of MU2;

      then

      reconsider MU1 as MSAlgebra over ( MSSign U2);

      let B be non empty Subset of U2;

      assume

       A3: B = the carrier of U1;

      let o be operation of U2;

      reconsider C = the Sorts of MU1 as MSSubset of MU2 by A2, MSUALG_2:def 9;

      

       A4: MU1 = MSAlgebra (# ( MSSorts U1), ( MSCharact U1) #) by MSUALG_1:def 11;

      set gg1 = (( *--> 0 ) * ( signature U2)), gg2 = (( dom ( signature U2)) --> z);

      reconsider gg1 as Function of ( dom ( signature U2)), ( { 0 } * ) by MSUALG_1: 2;

      

       A5: ( MSSign U2) = ManySortedSign (# { 0 }, ( dom ( signature U2)), gg1, gg2 #) by MSUALG_1: 10;

      

       A6: C is opers_closed by A2, MSUALG_2:def 9;

      thus B is_closed_on o

      proof

        

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

        let s be FinSequence of B;

        consider n be object such that

         A8: n in ( dom the charact of U2) and

         A9: o = (the charact of U2 . n) by FUNCT_1:def 3;

        

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

        then

         A11: n in ( dom ( signature U2)) by A8, UNIALG_1:def 4;

        reconsider n as OperSymbol of ( MSSign U2) by A5, A8, A10, UNIALG_1:def 4;

        assume

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

        ex y be set st y in ( dom (( Den (n,MU2)) | (((C # ) * the Arity of ( MSSign U2)) . n))) & ((( Den (n,MU2)) | (((C # ) * the Arity of ( MSSign U2)) . n)) . y) = (o . s)

        proof

          take s;

          thus s in ( dom (( Den (n,MU2)) | (((C # ) * the Arity of ( MSSign U2)) . n)))

          proof

            (( arity o) |-> 0 ) is FinSequence of the carrier of ( MSSign U2) by A5, FINSEQ_2: 63;

            then

            reconsider ao0 = (( arity o) |-> 0 ) as Element of (the carrier of ( MSSign U2) * ) by FINSEQ_1:def 11;

             A13:

            now

              assume ( Seg ( arity o)) = {} ;

              then (( arity o) |-> 0 ) = ( <*> the carrier of ( MSSign U2));

              hence (( arity o) |-> 0 ) is FinSequence of the carrier of ( MSSign U2);

            end;

            ( Seg ( arity o)) <> {} implies ( dom (( arity o) |-> 0 )) = ( Seg ( arity o)) & ( rng (( arity o) |-> 0 )) c= the carrier of ( MSSign U2) by A5, FUNCOP_1: 13;

            then (( arity o) |-> 0 ) is FinSequence of the carrier of ( MSSign U2) by A13, FINSEQ_1:def 4;

            then

            reconsider aro = (( arity o) |-> 0 ) as Element of (the carrier of ( MSSign U2) * ) by FINSEQ_1:def 11;

            

             A14: ( dom the Arity of ( MSSign U2)) = the carrier' of ( MSSign U2) by FUNCT_2:def 1;

            the Sorts of MU2 = ( 0 .--> the carrier of U2) by A1, MSUALG_1:def 9;

            

            then

             A15: (the Sorts of MU2 * aro) = (( arity o) |-> the carrier of U2) by FINSEQ_2: 144

            .= (( Seg ( arity o)) --> the carrier of U2);

            ( dom s) = ( Seg ( arity o)) by A12, FINSEQ_1:def 3;

            then

             A16: ( dom s) = ( dom (the Sorts of MU2 * aro)) by A15;

            

             A17: for x be object st x in ( dom (the Sorts of MU2 * aro)) holds (s . x) in ((the Sorts of MU2 * aro) . x)

            proof

              let x be object;

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

              then

               A18: ( rng s) c= the carrier of U2 by XBOOLE_1: 1;

              assume

               A19: x in ( dom (the Sorts of MU2 * aro));

              (s . x) in ( rng s) by A16, A19, FUNCT_1:def 3;

              then

               A20: 0 in { 0 } & (s . x) in the carrier of U2 by A18, TARSKI:def 1;

              ((the Sorts of MU2 * aro) . x) = (the Sorts of MU2 . (aro . x)) by A19, FUNCT_1: 12

              .= (( MSSorts U2) . 0 ) by A1

              .= (( 0 .--> the carrier of U2) . 0 ) by MSUALG_1:def 9;

              hence thesis by A20, FUNCOP_1: 7;

            end;

            ( dom ( Den (n,MU2))) = ( Args (n,MU2)) by FUNCT_2:def 1;

            

            then ( dom ( Den (n,MU2))) = (((the Sorts of MU2 # ) * the Arity of ( MSSign U2)) . n) by MSUALG_1:def 4

            .= ((the Sorts of MU2 # ) . ((( *--> 0 ) * ( signature U2)) . n)) by A5, A14, FUNCT_1: 13

            .= ((the Sorts of MU2 # ) . (( *--> 0 ) . (( signature U2) . n))) by A11, FUNCT_1: 13

            .= ((the Sorts of MU2 # ) . (( *--> 0 ) . ( arity o))) by A9, A11, UNIALG_1:def 4

            .= ((the Sorts of MU2 # ) . (( arity o) |-> 0 )) by FINSEQ_2:def 6;

            then ( dom ( Den (n,MU2))) = ( product (the Sorts of MU2 * aro)) by FINSEQ_2:def 5;

            then

             A21: s in ( dom ( Den (n,MU2))) by A16, A17, CARD_3:def 5;

            

             A22: s is Element of (( len s) -tuples_on B) by FINSEQ_2: 92;

            

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

            

             A24: n in ( dom ( signature U2)) by A8, A10, UNIALG_1:def 4;

            

             A25: C = ( 0 .--> the carrier of U1) by A4, MSUALG_1:def 9;

            then ( dom C) = { 0 };

            then

             A26: 0 in ( dom C) by TARSKI:def 1;

            ( dom ( *--> 0 )) = NAT & (( signature U2) . n) = ( arity o) by A9, A11, FUNCT_2:def 1, UNIALG_1:def 4;

            then

             A27: n in ( dom (( *--> 0 ) * ( signature U2))) by A24, FUNCT_1: 11;

            

            then (((C # ) * the Arity of ( MSSign U2)) . n) = ((C # ) . ((( *--> 0 ) * ( signature U2)) . n)) by A5, FUNCT_1: 13

            .= ((C # ) . (( *--> 0 ) . (( signature U2) . n))) by A27, FUNCT_1: 12

            .= ((C # ) . (( *--> 0 ) . ( arity o))) by A9, A24, UNIALG_1:def 4

            .= ((C # ) . (( arity o) |-> 0 )) by FINSEQ_2:def 6;

            

            then (((C # ) * the Arity of ( MSSign U2)) . n) = ( product (C * ao0)) by FINSEQ_2:def 5

            .= ( product (( Seg ( arity o)) --> (C . 0 ))) by A26, FUNCOP_1: 17

            .= ( product (( Seg ( arity o)) --> B)) by A3, A25, A23, FUNCOP_1: 7

            .= ( Funcs (( Seg ( arity o)),B)) by CARD_3: 11

            .= (( arity o) -tuples_on B) by FINSEQ_2: 93;

            then s in (( dom ( Den (n,MU2))) /\ (((C # ) * the Arity of ( MSSign U2)) . n)) by A12, A21, A22, XBOOLE_0:def 4;

            hence thesis by RELAT_1: 61;

          end;

          

          hence ((( Den (n,MU2)) | (((C # ) * the Arity of ( MSSign U2)) . n)) . s) = (( Den (n,MU2)) . s) by FUNCT_1: 47

          .= ((( MSCharact U2) . n) . s) by A1, MSUALG_1:def 6

          .= (o . s) by A9, MSUALG_1:def 10;

        end;

        then

         A28: (o . s) in ( rng (( Den (n,MU2)) | (((C # ) * the Arity of ( MSSign U2)) . n))) by FUNCT_1:def 3;

        C is_closed_on n by A6;

        then

         A29: ( rng (( Den (n,MU2)) | (((C # ) * the Arity of ( MSSign U2)) . n))) c= ((C * the ResultSort of ( MSSign U2)) . n);

        n in ( dom (( dom ( signature U2)) --> 0 )) by A11;

        

        then ((C * the ResultSort of ( MSSign U2)) . n) = (C . ((( dom ( signature U2)) --> 0 ) . n)) by A5, FUNCT_1: 13

        .= (the Sorts of MU1 . 0 )

        .= (( 0 .--> the carrier of U1) . 0 ) by A4, MSUALG_1:def 9

        .= B by A3, A7, FUNCOP_1: 7;

        hence thesis by A29, A28;

      end;

    end;

    theorem :: MSSUBLAT:15

    

     Th15: for U1,U2 be Universal_Algebra st ( MSAlg U1) is MSSubAlgebra of ( MSAlg U2) holds for B be non empty Subset of U2 st B = the carrier of U1 holds the charact of U1 = ( Opers (U2,B))

    proof

      let U1,U2 be Universal_Algebra;

      set MU1 = ( MSAlg U1), MU2 = ( MSAlg U2);

      

       A1: MU2 = MSAlgebra (# ( MSSorts U2), ( MSCharact U2) #) by MSUALG_1:def 11;

      assume

       A2: MU1 is MSSubAlgebra of MU2;

      then

      reconsider MU1 as MSAlgebra over ( MSSign U2);

      reconsider C = the Sorts of MU1 as MSSubset of MU2 by A2, MSUALG_2:def 9;

      

       A3: the Charact of MU1 = ( Opers (MU2,C)) by A2, MSUALG_2:def 9;

      set gg1 = (( *--> 0 ) * ( signature U2)), gg2 = (( dom ( signature U2)) --> z);

      reconsider gg1 as Function of ( dom ( signature U2)), ( { 0 } * ) by MSUALG_1: 2;

      

       A4: ( MSSign U2) = ManySortedSign (# { 0 }, ( dom ( signature U2)), gg1, gg2 #) by MSUALG_1: 10;

      let B be non empty Subset of U2;

      assume

       A5: B = the carrier of U1;

      then

      reconsider ch1 = the charact of U1 as PFuncFinSequence of B;

      

       A6: MU1 = MSAlgebra (# ( MSSorts U1), ( MSCharact U1) #) by MSUALG_1:def 11;

      

      then

       A7: ( dom ch1) = ( dom the Charact of MU1) by MSUALG_1:def 10

      .= the carrier' of ( MSSign U2) by PARTFUN1:def 2

      .= ( Seg ( len ( signature U2))) by A4, FINSEQ_1:def 3

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

      .= ( dom the charact of U2) by FINSEQ_1:def 3;

      

       A8: C is opers_closed by A2, MSUALG_2:def 9;

      for n be set, o be operation of U2 st n in ( dom ch1) & o = (the charact of U2 . n) holds (ch1 . n) = (o /. B)

      proof

        

         A9: C = ( 0 .--> the carrier of U1) by A6, MSUALG_1:def 9;

        then ( dom C) = { 0 };

        then

         A10: 0 in ( dom C) by TARSKI:def 1;

        let n be set;

        let o be operation of U2;

        assume that

         A11: n in ( dom ch1) and

         A12: o = (the charact of U2 . n);

        n in ( dom the Charact of MU2) by A1, A7, A11, MSUALG_1:def 10;

        then

        reconsider N = n as OperSymbol of ( MSSign U2) by PARTFUN1:def 2;

        

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

        then

         A14: N in ( dom ( signature U2)) by A7, A11, UNIALG_1:def 4;

        (( arity o) |-> 0 ) is FinSequence of the carrier of ( MSSign U2) by A4, FINSEQ_2: 63;

        then

        reconsider ao0 = (( arity o) |-> 0 ) as Element of (the carrier of ( MSSign U2) * ) by FINSEQ_1:def 11;

        

         A15: C is_closed_on N by A8;

        B is opers_closed by A2, A5, Th14;

        then

         A16: B is_closed_on o;

        

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

        N in ( dom ( signature U2)) by A7, A11, A13, UNIALG_1:def 4;

        then ( dom ( *--> 0 )) = NAT & (( signature U2) . N) = ( arity o) by A12, FUNCT_2:def 1, UNIALG_1:def 4;

        then

         A18: N in ( dom (( *--> 0 ) * ( signature U2))) by A14, FUNCT_1: 11;

        

        then (((C # ) * the Arity of ( MSSign U2)) . N) = ((C # ) . ((( *--> 0 ) * ( signature U2)) . N)) by A4, FUNCT_1: 13

        .= ((C # ) . (( *--> 0 ) . (( signature U2) . N))) by A18, FUNCT_1: 12

        .= ((C # ) . (( *--> 0 ) . ( arity o))) by A12, A14, UNIALG_1:def 4

        .= ((C # ) . (( arity o) |-> 0 )) by FINSEQ_2:def 6;

        

        then

         A19: (((C # ) * the Arity of ( MSSign U2)) . N) = ( product (C * ao0)) by FINSEQ_2:def 5

        .= ( product (( Seg ( arity o)) --> (C . 0 ))) by A10, FUNCOP_1: 17

        .= ( product (( Seg ( arity o)) --> B)) by A5, A9, A17, FUNCOP_1: 7

        .= ( Funcs (( Seg ( arity o)),B)) by CARD_3: 11

        .= (( arity o) -tuples_on B) by FINSEQ_2: 93;

        (ch1 . N) = (the Charact of MU1 . N) by A6, MSUALG_1:def 10

        .= (N /. C) by A3, MSUALG_2:def 8

        .= (( Den (N,MU2)) | (((C # ) * the Arity of ( MSSign U2)) . N)) by A15, MSUALG_2:def 7

        .= ((( MSCharact U2) . N) | (((C # ) * the Arity of ( MSSign U2)) . N)) by A1, MSUALG_1:def 6

        .= (o | (( arity o) -tuples_on B)) by A12, A19, MSUALG_1:def 10;

        hence thesis by A16, UNIALG_2:def 5;

      end;

      hence thesis by A7, UNIALG_2:def 6;

    end;

    theorem :: MSSUBLAT:16

    

     Th16: for U1,U2 be Universal_Algebra st ( MSAlg U1) is MSSubAlgebra of ( MSAlg U2) holds U1 is SubAlgebra of U2

    proof

      let U1,U2 be Universal_Algebra;

      assume

       A1: ( MSAlg U1) is MSSubAlgebra of ( MSAlg U2);

      hence the carrier of U1 is Subset of U2 by Th13;

      let B be non empty Subset of U2;

      assume B = the carrier of U1;

      hence thesis by A1, Th14, Th15;

    end;

    reserve MS for segmental non void1 -element ManySortedSign,

A for non-empty MSAlgebra over MS;

    theorem :: MSSUBLAT:17

    

     Th17: for B be non-empty MSSubAlgebra of A holds the carrier of ( 1-Alg B) is Subset of ( 1-Alg A)

    proof

      let B be non-empty MSSubAlgebra of A;

      the Sorts of B is MSSubset of A by MSUALG_2:def 9;

      then

       A1: the Sorts of B c= the Sorts of A by PBOOLE:def 18;

      ( 1-Alg B) = UAStr (# ( the_sort_of B), ( the_charact_of B) #) by MSUALG_1:def 14;

      then

      reconsider c = the carrier of ( 1-Alg B) as Component of the Sorts of B by MSUALG_1:def 12;

      ( 1-Alg A) = UAStr (# ( the_sort_of A), ( the_charact_of A) #) by MSUALG_1:def 14;

      then

      reconsider d = the carrier of ( 1-Alg A) as Component of the Sorts of A by MSUALG_1:def 12;

      

       A2: ( dom the Sorts of A) = the carrier of MS by PARTFUN1:def 2;

      then

      consider dr be object such that

       A3: dr in the carrier of MS and

       A4: d = (the Sorts of A . dr) by FUNCT_1:def 3;

      ( dom the Sorts of A) = ( dom the Sorts of B) by A2, PARTFUN1:def 2;

      then

      consider cr be object such that

       A5: cr in the carrier of MS and

       A6: c = (the Sorts of B . cr) by A2, FUNCT_1:def 3;

      cr = dr by A5, A3, STRUCT_0:def 10;

      hence thesis by A1, A5, A6, A4;

    end;

    theorem :: MSSUBLAT:18

    

     Th18: for B be non-empty MSSubAlgebra of A holds for S be non empty Subset of ( 1-Alg A) st S = the carrier of ( 1-Alg B) holds S is opers_closed

    proof

      let B be non-empty MSSubAlgebra of A;

      reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def 9;

      

       A1: C is opers_closed by MSUALG_2:def 9;

      

       A2: ( 1-Alg B) = UAStr (# ( the_sort_of B), ( the_charact_of B) #) by MSUALG_1:def 14;

      let S be non empty Subset of ( 1-Alg A) such that

       A3: S = the carrier of ( 1-Alg B);

      set 1A = ( 1-Alg A);

      

       A4: ( 1-Alg A) = UAStr (# ( the_sort_of A), ( the_charact_of A) #) by MSUALG_1:def 14;

      let o be operation of 1A;

      

       A5: ( dom the Sorts of A) = the carrier of MS by PARTFUN1:def 2;

      then

       A6: ( dom the Sorts of A) = ( dom the Sorts of B) by PARTFUN1:def 2;

      thus S is_closed_on o

      proof

        reconsider com = S as Component of the Sorts of B by A2, A3, MSUALG_1:def 12;

        consider n be object such that

         A7: n in ( dom the charact of 1A) and

         A8: o = (the charact of 1A . n) by FUNCT_1:def 3;

        n in ( dom the Charact of A) by A4, A7, MSUALG_1:def 13;

        then

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

        reconsider crn = (C . (the ResultSort of MS . n)) as Component of the Sorts of B by A5, A6, FUNCT_1:def 3;

        let s be FinSequence of S;

        

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

        assume

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

        ex y be set st y in ( dom (( Den (n,A)) | (((C # ) * the Arity of MS) . n))) & ((( Den (n,A)) | (((C # ) * the Arity of MS) . n)) . y) = (o . s)

        proof

          take s;

          

           A11: (the Charact of A . n) = (the charact of 1A . n) by A4, MSUALG_1:def 13;

          thus s in ( dom (( Den (n,A)) | (((C # ) * the Arity of MS) . n)))

          proof

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

            then ( rng s) c= the carrier of 1A by XBOOLE_1: 1;

            then

            reconsider s1 = s as FinSequence of the carrier of 1A by FINSEQ_1:def 4;

            reconsider An = (the Arity of MS . n) as Element of (the carrier of MS * );

            set f = (the Sorts of A * An);

            consider d be object such that

             A12: d in ( dom o) by XBOOLE_0:def 1;

            o in ( PFuncs ((the carrier of 1A * ),the carrier of 1A)) by PARTFUN1: 45;

            then ex o1 be Function st o1 = o & ( dom o1) c= (the carrier of 1A * ) & ( rng o1) c= the carrier of 1A by PARTFUN1:def 3;

            then

            reconsider d as FinSequence of the carrier of 1A by A12, FINSEQ_1:def 11;

            

             A13: ( dom ( Den (n,A))) = ( Args (n,A)) by FUNCT_2:def 1

            .= (( len ( the_arity_of n)) -tuples_on the carrier of 1A) by A4, MSUALG_1: 6;

            ( dom ( Den (n,A))) = ( Args (n,A)) by FUNCT_2:def 1;

            

            then ( dom ( Den (n,A))) = (((the Sorts of A # ) * the Arity of MS) . n) by MSUALG_1:def 4

            .= ((the Sorts of A # ) . (the Arity of MS . n)) by A9, FUNCT_1: 13;

            then

             A14: ( dom ( Den (n,A))) = ( product (the Sorts of A * An)) by FINSEQ_2:def 5;

            

             A15: o = (the Charact of A . n) by A4, A8, MSUALG_1:def 13

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

            ( len d) = ( len s1) by A10, A12, MARGREL1:def 25;

            then ( len s) = ( len ( the_arity_of n)) by A12, A15, A13, CARD_1:def 7;

            

            then

             A16: ( dom s) = ( Seg ( len ( the_arity_of n))) by FINSEQ_1:def 3

            .= ( dom ( the_arity_of n)) by FINSEQ_1:def 3

            .= ( dom An) by MSUALG_1:def 1;

            

             A17: ( dom s) c= ( dom (C * An))

            proof

              let x be object;

              assume

               A18: x in ( dom s);

              then ( rng An) c= the carrier of MS & (An . x) in ( rng An) by A16, FINSEQ_1:def 4, FUNCT_1:def 3;

              then (An . x) in the carrier of MS;

              then (An . x) in ( dom C) by PARTFUN1:def 2;

              hence thesis by A16, A18, FUNCT_1: 11;

            end;

            ( dom (C * An)) c= ( dom s) by A16, RELAT_1: 25;

            then

             A19: ( dom s) = ( dom (C * An)) by A17;

            

             A20: for x be object st x in ( dom s) holds (s . x) in ((C * An) . x)

            proof

              let x be object;

              

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

              assume

               A22: x in ( dom s);

              then

               A23: (s . x) in ( rng s) by FUNCT_1:def 3;

              ( dom s) c= ( dom An) by A19, RELAT_1: 25;

              then ( rng An) c= the carrier of MS & (An . x) in ( rng An) by A22, FINSEQ_1:def 4, FUNCT_1:def 3;

              then (An . x) in the carrier of MS;

              then

               A24: (An . x) in ( dom C) by PARTFUN1:def 2;

              ((C * An) . x) = (C . (An . x)) by A17, A22, FUNCT_1: 12;

              then

              reconsider canx = ((C * An) . x) as Component of C by A24, FUNCT_1:def 3;

              ((C * An) . x) = canx

              .= S by A2, A3, MSUALG_1:def 12;

              hence thesis by A23, A21;

            end;

            

             A25: ( dom f) c= ( dom s) by A16, FUNCT_1: 11;

            

             A26: for x be object st x in ( dom f) holds (s . x) in (f . x)

            proof

              let x be object;

              

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

              assume

               A28: x in ( dom f);

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

              then

              reconsider fx = (f . x) as Component of the Sorts of A by FUNCT_1: 14;

              (s . x) in ( rng s) by A25, A28, FUNCT_1:def 3;

              then fx = ( the_sort_of A) & (s . x) in S by A27, MSUALG_1:def 12;

              hence thesis by A4;

            end;

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

            

            then (((C # ) * the Arity of MS) . n) = ((C # ) . An) by FUNCT_1: 13

            .= ( product (C * An)) by FINSEQ_2:def 5;

            then

             A29: s in (((C # ) * the Arity of MS) . n) by A19, A20, CARD_3: 9;

            ( dom s) c= ( dom f)

            proof

              let x be object;

              assume

               A30: x in ( dom s);

              then ( rng An) c= the carrier of MS & (An . x) in ( rng An) by A16, FINSEQ_1:def 4, FUNCT_1:def 3;

              then (An . x) in the carrier of MS;

              then (An . x) in ( dom the Sorts of A) by PARTFUN1:def 2;

              hence thesis by A16, A30, FUNCT_1: 11;

            end;

            then ( dom s) = ( dom f) by A25;

            then s in ( dom ( Den (n,A))) by A14, A26, CARD_3: 9;

            then s in (( dom ( Den (n,A))) /\ (((C # ) * the Arity of MS) . n)) by A29, XBOOLE_0:def 4;

            hence thesis by RELAT_1: 61;

          end;

          

          hence ((( Den (n,A)) | (((C # ) * the Arity of MS) . n)) . s) = (( Den (n,A)) . s) by FUNCT_1: 47

          .= (o . s) by A8, A11, MSUALG_1:def 6;

        end;

        then

         A31: (o . s) in ( rng (( Den (n,A)) | (((C # ) * the Arity of MS) . n))) by FUNCT_1:def 3;

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

        

        then

         A32: ((C * the ResultSort of MS) . n) = crn by FUNCT_1: 13

        .= com by MSUALG_1: 5;

        C is_closed_on n by A1;

        then ( rng (( Den (n,A)) | (((C # ) * the Arity of MS) . n))) c= ((C * the ResultSort of MS) . n);

        hence thesis by A31, A32;

      end;

    end;

    theorem :: MSSUBLAT:19

    

     Th19: for B be non-empty MSSubAlgebra of A holds for S be non empty Subset of ( 1-Alg A) st S = the carrier of ( 1-Alg B) holds the charact of ( 1-Alg B) = ( Opers (( 1-Alg A),S))

    proof

      let B be non-empty MSSubAlgebra of A;

      reconsider C = the Sorts of B as MSSubset of A by MSUALG_2:def 9;

      

       A1: the Charact of B = ( Opers (A,C)) by MSUALG_2:def 9;

      set 1B = ( 1-Alg B), 1A = ( 1-Alg A);

      

       A2: ( 1-Alg A) = UAStr (# ( the_sort_of A), ( the_charact_of A) #) by MSUALG_1:def 14;

      set f1 = the charact of 1B;

      let S be non empty Subset of ( 1-Alg A) such that

       A3: S = the carrier of ( 1-Alg B);

      reconsider f1 as PFuncFinSequence of S by A3;

      

       A4: ( 1-Alg B) = UAStr (# ( the_sort_of B), ( the_charact_of B) #) by MSUALG_1:def 14;

      then

       A5: f1 = the Charact of B by MSUALG_1:def 13;

      

       A6: C is opers_closed by MSUALG_2:def 9;

      

       A7: for n be set, o be operation of 1A st n in ( dom f1) & o = (the charact of 1A . n) holds (f1 . n) = (o /. S)

      proof

        let n be set, o be operation of 1A;

        assume that

         A8: n in ( dom f1) and

         A9: o = (the charact of 1A . n);

        reconsider y = n as OperSymbol of MS by A5, A8, PARTFUN1:def 2;

        o = (the Charact of A . y) by A2, A9, MSUALG_1:def 13

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

        

        then

         A10: ( dom o) = ( Args (y,A)) by FUNCT_2:def 1

        .= (( len ( the_arity_of y)) -tuples_on ( the_sort_of A)) by MSUALG_1: 6;

        now

          set a = the Element of (( len ( the_arity_of y)) -tuples_on ( the_sort_of A));

          a in ( dom o) by A10;

          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_sort_of A) * ) st x = s & ( len s) = ( len ( the_arity_of y)) by A10;

          hence ( len ( the_arity_of y)) = ( len x);

        end;

        then

         A11: ( arity o) = ( len ( the_arity_of y)) by MARGREL1:def 25;

        S is opers_closed by A3, Th18;

        then

         A12: S is_closed_on o;

        

         A13: C is_closed_on y by A6;

        

         A14: (((C # ) * the Arity of MS) . y) = ( Args (y,B)) by MSUALG_1:def 4

        .= (( arity o) -tuples_on S) by A4, A3, A11, MSUALG_1: 6;

        (f1 . n) = (the Charact of B . y) by A4, MSUALG_1:def 13

        .= (y /. C) by A1, MSUALG_2:def 8

        .= (( Den (y,A)) | (((C # ) * the Arity of MS) . y)) by A13, MSUALG_2:def 7

        .= ((the Charact of A . y) | (((C # ) * the Arity of MS) . y)) by MSUALG_1:def 6

        .= (o | (( arity o) -tuples_on S)) by A2, A9, A14, MSUALG_1:def 13;

        hence thesis by A12, UNIALG_2:def 5;

      end;

      ( dom f1) = the carrier' of MS by A5, PARTFUN1:def 2

      .= ( dom the Charact of A) by PARTFUN1:def 2

      .= ( dom the charact of 1A) by A2, MSUALG_1:def 13;

      hence thesis by A7, UNIALG_2:def 6;

    end;

    theorem :: MSSUBLAT:20

    

     Th20: for B be non-empty MSSubAlgebra of A holds ( 1-Alg B) is SubAlgebra of ( 1-Alg A)

    proof

      let B be non-empty MSSubAlgebra of A;

      the carrier of ( 1-Alg B) is Subset of ( 1-Alg A) & for S be non empty Subset of ( 1-Alg A) st S = the carrier of ( 1-Alg B) holds the charact of ( 1-Alg B) = ( Opers (( 1-Alg A),S)) & S is opers_closed by Th17, Th18, Th19;

      hence thesis by UNIALG_2:def 7;

    end;

    theorem :: MSSUBLAT:21

    

     Th21: for S be non empty non void ManySortedSign, A,B be MSAlgebra over S holds A is MSSubAlgebra of B iff A is MSSubAlgebra of the MSAlgebra of B

    proof

      let S be non empty non void ManySortedSign, A,B be MSAlgebra over S;

      thus A is MSSubAlgebra of B implies A is MSSubAlgebra of the MSAlgebra of B

      proof

        assume

         A1: A is MSSubAlgebra of B;

        hence the Sorts of A is MSSubset of the MSAlgebra of B by MSUALG_2:def 9;

        thus for BB be MSSubset of the MSAlgebra of B st BB = the Sorts of A holds BB is opers_closed & the Charact of A = ( Opers ( the MSAlgebra of B,BB))

        proof

          let BB be MSSubset of the MSAlgebra of B such that

           A2: BB = the Sorts of A;

          reconsider bb = BB as MSSubset of B;

          

           A3: bb is opers_closed by A1, A2, MSUALG_2:def 9;

          

           A4: BB is opers_closed

          proof

            let o be OperSymbol of S;

            

             A5: ( Den (o,B)) = (the Charact of the MSAlgebra of B . o) by MSUALG_1:def 6

            .= ( Den (o, the MSAlgebra of B)) by MSUALG_1:def 6;

            bb is_closed_on o by A3;

            then ( rng (( Den (o, the MSAlgebra of B)) | (((BB # ) * the Arity of S) . o))) c= ((BB * the ResultSort of S) . o) by A5;

            hence thesis;

          end;

          for o be object st o in the carrier' of S holds (the Charact of A . o) = (( Opers ( the MSAlgebra of B,BB)) . o)

          proof

            let o be object;

            assume o in the carrier' of S;

            then

            reconsider o as OperSymbol of S;

            

             A6: ( Den (o,B)) = (the Charact of the MSAlgebra of B . o) by MSUALG_1:def 6

            .= ( Den (o, the MSAlgebra of B)) by MSUALG_1:def 6;

            

             A7: bb is_closed_on o by A3;

            

             A8: BB is_closed_on o by A4;

            (( Opers (B,bb)) . o) = (o /. bb) by MSUALG_2:def 8

            .= (( Den (o, the MSAlgebra of B)) | (((BB # ) * the Arity of S) . o)) by A6, A7, MSUALG_2:def 7

            .= (o /. BB) by A8, MSUALG_2:def 7

            .= (( Opers ( the MSAlgebra of B,BB)) . o) by MSUALG_2:def 8;

            hence thesis by A1, A2, MSUALG_2:def 9;

          end;

          hence thesis by A4;

        end;

      end;

      assume

       A9: A is MSSubAlgebra of the MSAlgebra of B;

      hence the Sorts of A is MSSubset of B by MSUALG_2:def 9;

      let C be MSSubset of B such that

       A10: C = the Sorts of A;

      reconsider CC = C as MSSubset of the MSAlgebra of B;

      

       A11: CC is opers_closed by A9, A10, MSUALG_2:def 9;

      

       A12: C is opers_closed

      proof

        let o be OperSymbol of S;

        

         A13: ( Den (o,B)) = (the Charact of the MSAlgebra of B . o) by MSUALG_1:def 6

        .= ( Den (o, the MSAlgebra of B)) by MSUALG_1:def 6;

        CC is_closed_on o by A11;

        then ( rng (( Den (o,B)) | (((C # ) * the Arity of S) . o))) c= ((C * the ResultSort of S) . o) by A13;

        hence thesis;

      end;

      for o be object st o in the carrier' of S holds (the Charact of A . o) = (( Opers (B,C)) . o)

      proof

        let o be object;

        assume o in the carrier' of S;

        then

        reconsider o as OperSymbol of S;

        

         A14: ( Den (o,B)) = (the Charact of the MSAlgebra of B . o) by MSUALG_1:def 6

        .= ( Den (o, the MSAlgebra of B)) by MSUALG_1:def 6;

        

         A15: CC is_closed_on o by A11;

        

         A16: C is_closed_on o by A12;

        (( Opers ( the MSAlgebra of B,CC)) . o) = (o /. CC) by MSUALG_2:def 8

        .= (( Den (o,B)) | (((C # ) * the Arity of S) . o)) by A14, A15, MSUALG_2:def 7

        .= (o /. C) by A16, MSUALG_2:def 7

        .= (( Opers (B,C)) . o) by MSUALG_2:def 8;

        hence thesis by A9, A10, MSUALG_2:def 9;

      end;

      hence thesis by A12;

    end;

    theorem :: MSSUBLAT:22

    for A,B be Universal_Algebra holds ( signature A) = ( signature B) iff ( MSSign A) = ( MSSign B)

    proof

      

       A1: for A,B be Universal_Algebra st ( MSSign A) = ( MSSign B) holds ( signature A) = ( signature B)

      proof

        let A,B be Universal_Algebra;

        reconsider ff1 = (( *--> 0 ) * ( signature A)) as Function of ( dom ( signature A)), ( { 0 } * ) by MSUALG_1: 2;

        reconsider gg1 = (( *--> 0 ) * ( signature B)) as Function of ( dom ( signature B)), ( { 0 } * ) by MSUALG_1: 2;

        

         A2: ( MSSign A) = ManySortedSign (# { 0 }, ( dom ( signature A)), ff1, (( dom ( signature A)) --> z) #) & ( MSSign B) = ManySortedSign (# { 0 }, ( dom ( signature B)), gg1, (( dom ( signature B)) --> z) #) by MSUALG_1: 10;

        assume

         A3: ( MSSign A) = ( MSSign B);

        now

          let i be Nat;

          assume

           A4: i in ( dom ( signature A));

          then

          reconsider k = (( signature A) . i) as Element of NAT by PARTFUN1: 4;

          

           A5: i in ( dom (( *--> 0 ) * ( signature A))) by A4, FINSEQ_3: 120;

          

          then

           A6: (( *--> 0 ) . (( signature B) . i)) = ((( *--> 0 ) * ( signature A)) . i) by A3, A2, FINSEQ_3: 120

          .= (( *--> 0 ) . (( signature A) . i)) by A5, FINSEQ_3: 120;

          reconsider m = (( signature B) . i) as Element of NAT by A3, A2, A4, PARTFUN1: 4;

          reconsider q = (( *--> 0 ) . m) as FinSequence;

          reconsider p = (( *--> 0 ) . k) as FinSequence;

          

          thus (( signature A) . i) = ( len p) by Th6

          .= ( len q) by A6

          .= (( signature B) . i) by Th6;

        end;

        hence thesis by A3, A2, FINSEQ_1: 13;

      end;

      for A,B be Universal_Algebra st ( signature A) = ( signature B) holds ( MSSign A) = ( MSSign B) by UNIALG_2:def 1, MSUHOM_1: 10;

      hence thesis by A1;

    end;

    theorem :: MSSUBLAT:23

    

     Th23: for A be non-empty MSAlgebra over MS st the carrier of MS = { 0 } holds ( MSSign ( 1-Alg A)) = the ManySortedSign of MS

    proof

      let A be non-empty MSAlgebra over MS;

      reconsider ff1 = (( *--> 0 ) * ( signature ( 1-Alg A))) as Function of ( dom ( signature ( 1-Alg A))), ( { 0 } * ) by MSUALG_1: 2;

      

       A1: ( MSSign ( 1-Alg A)) = ManySortedSign (# { 0 }, ( dom ( signature ( 1-Alg A))), ff1, (( dom ( signature ( 1-Alg A))) --> z) #) by MSUALG_1: 10;

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

      then

       A2: ( rng the ResultSort of MS) <> {} by RELAT_1: 42;

      consider k be Nat such that

       A3: the carrier' of MS = ( Seg k) by MSUALG_1:def 7;

      

       A4: ( 1-Alg A) = UAStr (# ( the_sort_of A), ( the_charact_of A) #) by MSUALG_1:def 14;

      

       A5: ( len ( signature ( 1-Alg A))) = ( len the charact of ( 1-Alg A)) by UNIALG_1:def 4;

      

      then

       A6: ( dom ( signature ( 1-Alg A))) = ( dom the charact of ( 1-Alg A)) by FINSEQ_3: 29

      .= ( dom the Charact of A) by A4, MSUALG_1:def 13

      .= the carrier' of MS by PARTFUN1:def 2;

      then

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

      assume

       A8: the carrier of MS = { 0 };

      

       A9: for x be object st x in the carrier' of MS holds ((( *--> 0 ) * ( signature ( 1-Alg A))) . x) = (the Arity of MS . x)

      proof

        let x be object;

        assume x in the carrier' of MS;

        then

        reconsider x as OperSymbol of MS;

        x in ( Seg k) by A3;

        then

        reconsider n = x as Nat;

        n in ( dom ( signature ( 1-Alg A))) by A6;

        then

         A10: n in ( dom the charact of ( 1-Alg A)) by A5, FINSEQ_3: 29;

        then

        reconsider h = (the charact of ( 1-Alg A) . n) as PartFunc of (the carrier of ( 1-Alg A) * ), the carrier of ( 1-Alg A) by UNIALG_1: 1;

        reconsider h as homogeneous quasi_total non empty PartFunc of (the carrier of ( 1-Alg A) * ), the carrier of ( 1-Alg A) by A10, MARGREL1:def 24;

        set aa = the Element of ( dom h);

        set ah = ( arity h);

        ( dom h) c= (the carrier of ( 1-Alg A) * ) by RELAT_1:def 18;

        then aa in (the carrier of ( 1-Alg A) * );

        then

        reconsider bb = aa as FinSequence of the carrier of ( 1-Alg A) by FINSEQ_1:def 11;

        

         A11: bb in ( dom h);

        h = (the Charact of A . x) by A4, MSUALG_1:def 13

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

        then bb in ( Args (x,A)) by A11, FUNCT_2:def 1;

        then bb in (( len ( the_arity_of x)) -tuples_on ( the_sort_of A)) by MSUALG_1: 6;

        

        then

         A12: ( len ( the_arity_of x)) = ( len bb) by CARD_1:def 7

        .= ah by MARGREL1:def 25;

        ((( *--> 0 ) * ( signature ( 1-Alg A))) . x) = (( *--> 0 ) . (( signature ( 1-Alg A)) . x)) by A6, FUNCT_1: 13

        .= (( *--> 0 ) . ah) by A6, UNIALG_1:def 4

        .= (ah |-> 0 ) by FINSEQ_2:def 6

        .= ( the_arity_of x) by A8, A12, Th5

        .= (the Arity of MS . x) by MSUALG_1:def 1;

        hence thesis;

      end;

      ( rng the ResultSort of MS) c= { 0 } by A8, RELAT_1:def 19;

      then the carrier' of MS = ( dom the ResultSort of MS) & ( rng the ResultSort of MS) = { 0 } by A2, FUNCT_2:def 1, ZFMISC_1: 33;

      then the carrier' of MS = ( dom the Arity of MS) & the ResultSort of ( MSSign ( 1-Alg A)) = the ResultSort of MS by A1, A6, FUNCOP_1: 9, FUNCT_2:def 1;

      hence thesis by A8, A1, A7, A9, FUNCT_1: 2;

    end;

    theorem :: MSSUBLAT:24

    

     Th24: for A,B be non-empty MSAlgebra over MS st ( 1-Alg A) = ( 1-Alg B) holds the MSAlgebra of A = the MSAlgebra of B

    proof

      let A,B be non-empty MSAlgebra over MS such that

       A1: ( 1-Alg A) = ( 1-Alg B);

      

       A2: ( 1-Alg B) = UAStr (# ( the_sort_of B), ( the_charact_of B) #) by MSUALG_1:def 14;

      

       A3: ( 1-Alg A) = UAStr (# ( the_sort_of A), ( the_charact_of A) #) by MSUALG_1:def 14;

       A4:

      now

        let i be object such that

         A5: i in the carrier of MS;

        

         A6: ex c be Component of the Sorts of B st (the Sorts of B . i) = c

        proof

          reconsider c = (the Sorts of B . i) as Component of the Sorts of B by A5, PBOOLE: 139;

          take c;

          thus thesis;

        end;

        ex c be Component of the Sorts of A st (the Sorts of A . i) = c

        proof

          reconsider c = (the Sorts of A . i) as Component of the Sorts of A by A5, PBOOLE: 139;

          take c;

          thus thesis;

        end;

        

        then (the Sorts of A . i) = ( the_sort_of B) by A1, A3, A2, MSUALG_1:def 12

        .= (the Sorts of B . i) by A6, MSUALG_1:def 12;

        hence (the Sorts of A . i) = (the Sorts of B . i);

      end;

      the Charact of A = the charact of ( 1-Alg A) by A3, MSUALG_1:def 13

      .= the Charact of B by A1, A2, MSUALG_1:def 13;

      hence thesis by A4, PBOOLE: 3;

    end;

    theorem :: MSSUBLAT:25

    for A be non-empty MSAlgebra over MS st the carrier of MS = { 0 } holds the Sorts of A = the Sorts of ( MSAlg ( 1-Alg A))

    proof

      let A be non-empty MSAlgebra over MS;

      assume

       A1: the carrier of MS = { 0 };

       A2:

      now

        let i be object;

        assume

         A3: i in the carrier of MS;

        

         A4: ex c be Component of the Sorts of A st (the Sorts of A . i) = c

        proof

          reconsider c = (the Sorts of A . i) as Component of the Sorts of A by A3, PBOOLE: 139;

          take c;

          thus thesis;

        end;

        (( { 0 } --> ( the_sort_of A)) . i) = ( the_sort_of A) by A1, A3, FUNCOP_1: 7;

        hence (the Sorts of A . i) = (( { 0 } --> ( the_sort_of A)) . i) by A4, MSUALG_1:def 12;

      end;

      ( 1-Alg A) = UAStr (# ( the_sort_of A), ( the_charact_of A) #) by MSUALG_1:def 14;

      then

       A5: ( MSAlg ( 1-Alg A)) = MSAlgebra (# ( MSSorts ( 1-Alg A)), ( MSCharact ( 1-Alg A)) #) & ( MSSorts ( 1-Alg A)) = ( 0 .--> ( the_sort_of A)) by MSUALG_1:def 9, MSUALG_1:def 11;

      ( { 0 } --> ( the_sort_of A)) is ManySortedSet of the carrier of MS by A1;

      hence thesis by A5, A2, PBOOLE: 3;

    end;

    theorem :: MSSUBLAT:26

    

     Th26: for A be non-empty MSAlgebra over MS st the carrier of MS = { 0 } holds ( MSAlg ( 1-Alg A)) = the MSAlgebra of A

    proof

      let A be non-empty MSAlgebra over MS;

      reconsider c = ( the_sort_of ( MSAlg ( 1-Alg A))) as Component of the Sorts of ( MSAlg ( 1-Alg A)) by MSUALG_1:def 12;

      assume the carrier of MS = { 0 };

      then ( MSSign ( 1-Alg A)) = the ManySortedSign of MS by Th23;

      then

      reconsider M1A = ( MSAlg ( 1-Alg A)) as strict MSAlgebra over MS;

      reconsider M1A as non-empty strict MSAlgebra over MS by MSUALG_1:def 3;

      

       A1: ( 1-Alg M1A) = UAStr (# ( the_sort_of M1A), ( the_charact_of M1A) #) by MSUALG_1:def 14;

      reconsider c as Component of the Sorts of M1A;

      

       A2: ( 1-Alg ( MSAlg ( 1-Alg A))) = UAStr (# ( the_sort_of ( MSAlg ( 1-Alg A))), ( the_charact_of ( MSAlg ( 1-Alg A))) #) by MSUALG_1:def 14;

      

      then

       A3: the charact of ( 1-Alg A) = ( the_charact_of ( MSAlg ( 1-Alg A))) by MSUALG_1: 9

      .= the Charact of M1A by MSUALG_1:def 13

      .= the charact of ( 1-Alg M1A) by A1, MSUALG_1:def 13;

      c = ( the_sort_of M1A) by MSUALG_1:def 12;

      then the carrier of ( 1-Alg A) = the carrier of ( 1-Alg M1A) by A2, A1, MSUALG_1: 9;

      hence thesis by A3, Th24;

    end;

    theorem :: MSSUBLAT:27

    for A be Universal_Algebra, B be strict non-empty MSSubAlgebra of ( MSAlg A) st the carrier of ( MSSign A) = { 0 } holds ( 1-Alg B) is SubAlgebra of A

    proof

      let A be Universal_Algebra, B be strict non-empty MSSubAlgebra of ( MSAlg A);

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

      then ( MSAlg ( 1-Alg B)) = the MSAlgebra of B by Th26;

      hence thesis by Th16;

    end;

    begin

    theorem :: MSSUBLAT:28

    

     Th28: for A be Universal_Algebra, a1,b1 be strict SubAlgebra of A, a2,b2 be strict non-empty MSSubAlgebra of ( MSAlg A) st a2 = ( MSAlg a1) & b2 = ( MSAlg b1) holds (the Sorts of a2 (\/) the Sorts of b2) = ( 0 .--> (the carrier of a1 \/ the carrier of b1))

    proof

      let A be Universal_Algebra;

      let a1,b1 be strict SubAlgebra of A;

      let a2,b2 be strict non-empty MSSubAlgebra of ( MSAlg A) such that

       A1: a2 = ( MSAlg a1) and

       A2: b2 = ( MSAlg b1);

      a2 = MSAlgebra (# ( MSSorts a1), ( MSCharact a1) #) by A1, MSUALG_1:def 11;

      then

       A3: the Sorts of a2 = ( 0 .--> the carrier of a1) by MSUALG_1:def 9;

      reconsider ff1 = (( *--> 0 ) * ( signature A)) as Function of ( dom ( signature A)), ( { 0 } * ) by MSUALG_1: 2;

      

       A4: ( MSSign A) = ManySortedSign (# { 0 }, ( dom ( signature A)), ff1, (( dom ( signature A)) --> z) #) by MSUALG_1: 10;

      then

      reconsider W = ( 0 .--> (the carrier of a1 \/ the carrier of b1)) as ManySortedSet of the carrier of ( MSSign A);

      

       A5: b2 = MSAlgebra (# ( MSSorts b1), ( MSCharact b1) #) by A2, MSUALG_1:def 11;

      now

        let x be object;

        assume

         A6: x in the carrier of ( MSSign A);

        then

         A7: x = 0 by A4, TARSKI:def 1;

        (W . x) = (( 0 .--> (the carrier of a1 \/ the carrier of b1)) . 0 ) by A4, A6, TARSKI:def 1

        .= (the carrier of a1 \/ the carrier of b1) by FUNCOP_1: 72

        .= ((( 0 .--> the carrier of a1) . 0 ) \/ the carrier of b1) by FUNCOP_1: 72

        .= ((( 0 .--> the carrier of a1) . 0 ) \/ (( 0 .--> the carrier of b1) . 0 )) by FUNCOP_1: 72

        .= ((the Sorts of a2 . x) \/ (the Sorts of b2 . x)) by A3, A5, A7, MSUALG_1:def 9;

        hence (W . x) = ((the Sorts of a2 . x) \/ (the Sorts of b2 . x));

      end;

      hence thesis by PBOOLE:def 4;

    end;

    theorem :: MSSUBLAT:29

    

     Th29: for A be Universal_Algebra, a1,b1 be strict non-empty SubAlgebra of A, a2,b2 be strict non-empty MSSubAlgebra of ( MSAlg A) st a2 = ( MSAlg a1) & b2 = ( MSAlg b1) holds (the Sorts of a2 (/\) the Sorts of b2) = ( 0 .--> (the carrier of a1 /\ the carrier of b1))

    proof

      let A be Universal_Algebra;

      let a1,b1 be strict non-empty SubAlgebra of A;

      let a2,b2 be strict non-empty MSSubAlgebra of ( MSAlg A) such that

       A1: a2 = ( MSAlg a1) and

       A2: b2 = ( MSAlg b1);

      a2 = MSAlgebra (# ( MSSorts a1), ( MSCharact a1) #) by A1, MSUALG_1:def 11;

      then

       A3: the Sorts of a2 = ( 0 .--> the carrier of a1) by MSUALG_1:def 9;

      reconsider ff1 = (( *--> 0 ) * ( signature A)) as Function of ( dom ( signature A)), ( { 0 } * ) by MSUALG_1: 2;

      

       A4: ( MSSign A) = ManySortedSign (# { 0 }, ( dom ( signature A)), ff1, (( dom ( signature A)) --> z) #) by MSUALG_1: 10;

      then

      reconsider W = ( 0 .--> (the carrier of a1 /\ the carrier of b1)) as ManySortedSet of the carrier of ( MSSign A);

      

       A5: b2 = MSAlgebra (# ( MSSorts b1), ( MSCharact b1) #) by A2, MSUALG_1:def 11;

      now

        let x be object;

        assume x in the carrier of ( MSSign A);

        then

         A6: x = 0 by A4, TARSKI:def 1;

        

        then (W . x) = (the carrier of a1 /\ the carrier of b1) by FUNCOP_1: 72

        .= ((( 0 .--> the carrier of a1) . 0 ) /\ the carrier of b1) by FUNCOP_1: 72

        .= ((( 0 .--> the carrier of a1) . 0 ) /\ (( 0 .--> the carrier of b1) . 0 )) by FUNCOP_1: 72

        .= ((the Sorts of a2 . x) /\ (the Sorts of b2 . x)) by A3, A5, A6, MSUALG_1:def 9;

        hence (W . x) = ((the Sorts of a2 . x) /\ (the Sorts of b2 . x));

      end;

      hence thesis by PBOOLE:def 5;

    end;

    theorem :: MSSUBLAT:30

    

     Th30: for A be strict Universal_Algebra, a1,b1 be strict non-empty SubAlgebra of A, a2,b2 be strict non-empty MSSubAlgebra of ( MSAlg A) st a2 = ( MSAlg a1) & b2 = ( MSAlg b1) holds ( MSAlg (a1 "\/" b1)) = (a2 "\/" b2)

    proof

      let A be strict Universal_Algebra;

      let a1,b1 be strict non-empty SubAlgebra of A;

      reconsider MSA = ( MSAlg (a1 "\/" b1)) as MSSubAlgebra of ( MSAlg A) by Th12;

      let a2,b2 be strict non-empty MSSubAlgebra of ( MSAlg A) such that

       A1: a2 = ( MSAlg a1) and

       A2: b2 = ( MSAlg b1);

      ( MSSign (a1 "\/" b1)) = ( MSSign A) by Th7;

      then

      reconsider MSA as strict non-empty MSSubAlgebra of ( MSAlg A);

      for B be MSSubset of ( MSAlg A) st B = (the Sorts of a2 (\/) the Sorts of b2) holds MSA = ( GenMSAlg B)

      proof

        the carrier of a1 is Subset of A & the carrier of b1 is Subset of A by UNIALG_2:def 7;

        then

        reconsider K = (the carrier of a1 \/ the carrier of b1) as non empty Subset of A by XBOOLE_1: 8;

        reconsider ff1 = (( *--> 0 ) * ( signature A)) as Function of ( dom ( signature A)), ( { 0 } * ) by MSUALG_1: 2;

        set X = MSA;

        reconsider M1 = the Sorts of X as ManySortedSet of the carrier of ( MSSign A);

        

         A3: ( MSSign A) = ManySortedSign (# { 0 }, ( dom ( signature A)), ff1, (( dom ( signature A)) --> z) #) by MSUALG_1: 10;

        then

        reconsider x = 0 as Element of ( MSSign A);

        let B be MSSubset of ( MSAlg A) such that

         A4: B = (the Sorts of a2 (\/) the Sorts of b2);

        

         A5: for U1 be MSSubAlgebra of ( MSAlg A) st B is MSSubset of U1 holds X is MSSubAlgebra of U1

        proof

          let U1 be MSSubAlgebra of ( MSAlg A);

          assume

           A6: B is MSSubset of U1;

          per cases ;

            suppose U1 is non-empty;

            then

            reconsider U11 = U1 as non-empty MSSubAlgebra of ( MSAlg A);

            

             A7: ( 1-Alg U11) is SubAlgebra of ( 1-Alg ( MSAlg A)) by Th20;

            then

            reconsider A1 = ( 1-Alg U11) as strict SubAlgebra of A by MSUALG_1: 9;

            B c= the Sorts of U11 by A6, PBOOLE:def 18;

            then

             A8: (B . x) c= (the Sorts of U11 . x);

             the MSAlgebra of U11 = ( MSAlg ( 1-Alg U11)) & ( MSAlg ( 1-Alg U11)) = MSAlgebra (# ( MSSorts ( 1-Alg U11)), ( MSCharact ( 1-Alg U11)) #) by A3, Th26, MSUALG_1:def 11;

            then

             A9: (the Sorts of U11 . 0 ) = (( 0 .--> the carrier of ( 1-Alg U11)) . 0 ) by MSUALG_1:def 9;

            (B . 0 ) = (( 0 .--> K) . 0 ) by A1, A2, A4, Th28

            .= K by FUNCOP_1: 72;

            then (the carrier of a1 \/ the carrier of b1) c= the carrier of A1 by A8, A9, FUNCOP_1: 72;

            then ( GenUnivAlg K) is SubAlgebra of ( 1-Alg U11) by UNIALG_2:def 12;

            then (a1 "\/" b1) is SubAlgebra of ( 1-Alg U11) by UNIALG_2:def 13;

            then

             A10: MSA is MSSubAlgebra of ( MSAlg ( 1-Alg U11)) by Th12;

            ( 1-Alg U11) is SubAlgebra of A by A7, MSUALG_1: 9;

            then ( MSSign A) = ( MSSign ( 1-Alg U11)) by Th7;

            then X is MSSubAlgebra of the MSAlgebra of U11 by A3, A10, Th26;

            hence thesis by Th21;

          end;

            suppose not U1 is non-empty;

            then the Sorts of U1 is non non-empty by MSUALG_1:def 3;

            then

             A11: ex i be object st i in the carrier of ( MSSign A) & (the Sorts of U1 . i) is empty;

            reconsider 0a1 = ( 0 .--> the carrier of a1) as ManySortedSet of the carrier of ( MSSign A) by A3;

            set e = the Element of a1;

            B c= the Sorts of U1 by A6, PBOOLE:def 18;

            then

             A12: (B . x) c= (the Sorts of U1 . x);

            a2 = MSAlgebra (# ( MSSorts a1), ( MSCharact a1) #) by A1, MSUALG_1:def 11;

            then B = (0a1 (\/) the Sorts of b2) by A4, MSUALG_1:def 9;

            then

             A13: (B . x) = ((0a1 . x) \/ (the Sorts of b2 . x)) by PBOOLE:def 4;

            x in { 0 } by TARSKI:def 1;

            then (0a1 . x) = the carrier of a1 by FUNCOP_1: 7;

            then e in (B . x) by A13, XBOOLE_0:def 3;

            hence thesis by A3, A11, A12, TARSKI:def 1;

          end;

        end;

        X = MSAlgebra (# ( MSSorts (a1 "\/" b1)), ( MSCharact (a1 "\/" b1)) #) by MSUALG_1:def 11;

        then

         A14: the Sorts of X = ( 0 .--> the carrier of (a1 "\/" b1)) by MSUALG_1:def 9;

        (the Sorts of a2 (\/) the Sorts of b2) c= M1

        proof

          let x be object;

          

           A15: (a1 "\/" b1) = ( GenUnivAlg K) by UNIALG_2:def 13;

          assume

           A16: x in the carrier of ( MSSign A);

          

          then

           A17: (M1 . x) = (( 0 .--> the carrier of (a1 "\/" b1)) . 0 ) by A14, A3, TARSKI:def 1

          .= the carrier of (a1 "\/" b1) by FUNCOP_1: 72;

          ((the Sorts of a2 (\/) the Sorts of b2) . x) = ((the Sorts of a2 (\/) the Sorts of b2) . 0 ) by A3, A16, TARSKI:def 1

          .= (( 0 .--> (the carrier of a1 \/ the carrier of b1)) . 0 ) by A1, A2, Th28

          .= (the carrier of a1 \/ the carrier of b1) by FUNCOP_1: 72;

          hence thesis by A17, A15, UNIALG_2:def 12;

        end;

        then B is MSSubset of X by A4, PBOOLE:def 18;

        hence thesis by A5, MSUALG_2:def 17;

      end;

      hence thesis by MSUALG_2:def 18;

    end;

    registration

      let A be with_const_op Universal_Algebra;

      cluster ( MSSign A) -> non void strict segmental trivial all-with_const_op;

      coherence

      proof

        reconsider ff1 = (( *--> 0 ) * ( signature A)) as Function of ( dom ( signature A)), ( { 0 } * ) by MSUALG_1: 2;

        

         A1: ( MSSign A) = ManySortedSign (# { 0 }, ( dom ( signature A)), ff1, (( dom ( signature A)) --> z) #) by MSUALG_1: 10;

        ( MSSign A) is all-with_const_op

        proof

          let s be SortSymbol of ( MSSign A);

          consider OO be operation of A such that

           A2: ( arity OO) = 0 by UNIALG_2:def 11;

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

          then

          consider i be Nat such that

           A3: i in ( Seg ( len the charact of A)) and

           A4: (the charact of A . i) = OO by FINSEQ_2: 10;

          

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

          then

           A6: i in ( dom ( signature A)) by A3, FINSEQ_1:def 3;

          reconsider i as OperSymbol of ( MSSign A) by A1, A3, A5, FINSEQ_1:def 3;

          take i;

          (( *--> 0 ) . (( signature A) . i)) = (( *--> 0 ) . 0 ) by A2, A4, A6, UNIALG_1:def 4

          .= {} by Th1;

          hence (the Arity of ( MSSign A) . i) = {} by A1, FUNCT_1: 13;

          thus (the ResultSort of ( MSSign A) . i) = s by A1, TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    theorem :: MSSUBLAT:31

    

     Th31: for A be with_const_op Universal_Algebra, a1,b1 be strict non-empty SubAlgebra of A, a2,b2 be strict non-empty MSSubAlgebra of ( MSAlg A) st a2 = ( MSAlg a1) & b2 = ( MSAlg b1) holds ( MSAlg (a1 /\ b1)) = (a2 /\ b2)

    proof

      let A be with_const_op Universal_Algebra;

      let a1,b1 be strict non-empty SubAlgebra of A;

      reconsider ff1 = (( *--> 0 ) * ( signature A)) as Function of ( dom ( signature A)), ( { 0 } * ) by MSUALG_1: 2;

      

       A1: ( MSSign A) = ManySortedSign (# { 0 }, ( dom ( signature A)), ff1, (( dom ( signature A)) --> z) #) by MSUALG_1: 10;

      ( MSAlg (a1 /\ b1)) = MSAlgebra (# ( MSSorts (a1 /\ b1)), ( MSCharact (a1 /\ b1)) #) by MSUALG_1:def 11;

      then

       A2: the Sorts of ( MSAlg (a1 /\ b1)) = ( 0 .--> the carrier of (a1 /\ b1)) by MSUALG_1:def 9;

      then ( dom the Sorts of ( MSAlg (a1 /\ b1))) = the carrier of ( MSSign A) by A1;

      then

      reconsider D = the Sorts of ( MSAlg (a1 /\ b1)) as ManySortedSet of the carrier of ( MSSign A) by PARTFUN1:def 2, RELAT_1:def 18;

      let a2,b2 be strict non-empty MSSubAlgebra of ( MSAlg A) such that

       A3: a2 = ( MSAlg a1) & b2 = ( MSAlg b1);

      now

        let x be object;

        

         A4: the carrier of a1 meets the carrier of b1 by UNIALG_2: 17;

        assume

         A5: x in the carrier of ( MSSign A);

        

        hence (D . x) = (( 0 .--> the carrier of (a1 /\ b1)) . 0 ) by A2, A1, TARSKI:def 1

        .= the carrier of (a1 /\ b1) by FUNCOP_1: 72

        .= (the carrier of a1 /\ the carrier of b1) by A4, UNIALG_2:def 9

        .= (( 0 .--> (the carrier of a1 /\ the carrier of b1)) . 0 ) by FUNCOP_1: 72

        .= ((the Sorts of a2 (/\) the Sorts of b2) . 0 ) by A3, Th29

        .= ((the Sorts of a2 (/\) the Sorts of b2) . x) by A1, A5, TARSKI:def 1;

      end;

      then

       A6: D = (the Sorts of a2 (/\) the Sorts of b2);

      ( MSSign (a1 /\ b1)) = ( MSSign A) by Th7;

      then

      reconsider AA = ( MSAlg (a1 /\ b1)) as strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

      for B be MSSubset of ( MSAlg A) st B = the Sorts of AA holds B is opers_closed & the Charact of AA = ( Opers (( MSAlg A),B)) by MSUALG_2:def 9;

      hence thesis by A6, MSUALG_2:def 16;

    end;

    registration

      let A be quasi_total UAStr;

      cluster the UAStr of A -> quasi_total;

      coherence ;

    end

    registration

      let A be partial UAStr;

      cluster the UAStr of A -> partial;

      coherence ;

    end

    registration

      let A be non-empty UAStr;

      cluster the UAStr of A -> non-empty;

      coherence ;

    end

    registration

      let A be with_const_op Universal_Algebra;

      cluster the UAStr of A -> with_const_op;

      coherence

      proof

        consider o be operation of A such that

         A1: ( arity o) = 0 by UNIALG_2:def 11;

        reconsider oo = o as operation of the UAStr of A;

        take oo;

        thus thesis by A1;

      end;

    end

    theorem :: MSSUBLAT:32

    for A be with_const_op Universal_Algebra holds (( UnSubAlLattice the UAStr of A),( MSSubAlLattice ( MSAlg the UAStr of A))) are_isomorphic

    proof

      let Z be with_const_op Universal_Algebra;

      set A = the UAStr of Z;

      reconsider ff1 = (( *--> 0 ) * ( signature A)) as Function of ( dom ( signature A)), ( { 0 } * ) by MSUALG_1: 2;

      

       A1: ( MSSign A) = ManySortedSign (# { 0 }, ( dom ( signature A)), ff1, (( dom ( signature A)) --> z) #) by MSUALG_1: 10;

      defpred P[ set, set] means ex A1 be strict SubAlgebra of A st A1 = $1 & $2 = ( MSAlg A1);

      

       A2: for x be Element of ( Sub A) holds ex y be Element of ( MSSub ( MSAlg A)) st P[x, y]

      proof

        let x be Element of ( Sub A);

        reconsider B = x as strict SubAlgebra of A by UNIALG_2:def 14;

        ( MSSign A) = ( MSSign B) by Th7;

        then ( MSAlg B) is strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

        then

        reconsider y = ( MSAlg B) as Element of ( MSSub ( MSAlg A)) by MSUALG_2:def 19;

        take y, B;

        thus thesis;

      end;

      consider f be Function of ( Sub A), ( MSSub ( MSAlg A)) such that

       A3: for x be Element of ( Sub A) holds P[x, (f . x)] from FUNCT_2:sch 3( A2);

      reconsider f as Function of the carrier of ( UnSubAlLattice A), the carrier of ( MSSubAlLattice ( MSAlg A));

      f is Homomorphism of ( UnSubAlLattice A), ( MSSubAlLattice ( MSAlg A))

      proof

        

         AA: f is "\/"-preserving

        proof

          let a1,b1 be Element of ( UnSubAlLattice A);

          reconsider a2 = a1, b2 = b1 as Element of ( Sub A);

          reconsider a3 = a2, b3 = b2 as strict non-empty SubAlgebra of A by UNIALG_2:def 14;

          reconsider s = (a3 "\/" b3) as Element of ( Sub A) by UNIALG_2:def 14;

          reconsider m = (a3 /\ b3) as Element of ( Sub A) by UNIALG_2:def 14;

          

           A4: ex A1 be strict non-empty SubAlgebra of A st A1 = s & (f . s) = ( MSAlg A1) by A3;

          ( MSSign b3) = ( MSSign A) by Th7;

          then

          reconsider g2 = ( MSAlg b3) as strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

          consider A4 be strict non-empty SubAlgebra of A such that

           A5: A4 = b3 and

           A6: (f . b3) = ( MSAlg A4) by A3;

          ( MSSign A4) = ( MSSign A) by Th7;

          then

          reconsider g3 = ( MSAlg A4) as strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

          ( MSSign a3) = ( MSSign A) by Th7;

          then

          reconsider g1 = ( MSAlg a3) as strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

          consider A3 be strict non-empty SubAlgebra of A such that

           A7: A3 = a3 and

           A8: (f . a3) = ( MSAlg A3) by A3;

          ( MSSign A3) = ( MSSign A) by Th7;

          then

          reconsider g4 = ( MSAlg A3) as strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

          

          thus (f . (a1 "\/" b1)) = (f . (( UniAlg_join A) . (a2,b2))) by LATTICES:def 1

          .= ( MSAlg (a3 "\/" b3)) by A4, UNIALG_2:def 15

          .= (g4 "\/" g3) by A7, A5, Th30

          .= (the L_join of ( MSSubAlLattice ( MSAlg A)) . ((f . a1),(f . b1))) by A8, A6, MSUALG_2:def 20

          .= ((f . a1) "\/" (f . b1)) by LATTICES:def 1;

        end;

        f is "/\"-preserving

        proof

          let a1,b1 be Element of ( UnSubAlLattice A);

          reconsider a2 = a1, b2 = b1 as Element of ( Sub A);

          reconsider a3 = a2, b3 = b2 as strict non-empty SubAlgebra of A by UNIALG_2:def 14;

          reconsider s = (a3 "\/" b3) as Element of ( Sub A) by UNIALG_2:def 14;

          reconsider m = (a3 /\ b3) as Element of ( Sub A) by UNIALG_2:def 14;

          ( MSSign b3) = ( MSSign A) by Th7;

          then

          reconsider g2 = ( MSAlg b3) as strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

          consider A4 be strict non-empty SubAlgebra of A such that

           A5: A4 = b3 and

           A6: (f . b3) = ( MSAlg A4) by A3;

          ( MSSign A4) = ( MSSign A) by Th7;

          then

          reconsider g3 = ( MSAlg A4) as strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

          ( MSSign a3) = ( MSSign A) by Th7;

          then

          reconsider g1 = ( MSAlg a3) as strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

          consider A3 be strict non-empty SubAlgebra of A such that

           A7: A3 = a3 and

           A8: (f . a3) = ( MSAlg A3) by A3;

          ( MSSign A3) = ( MSSign A) by Th7;

          then

          reconsider g4 = ( MSAlg A3) as strict non-empty MSSubAlgebra of ( MSAlg A) by Th12;

          

           A9: ex A1 be strict non-empty SubAlgebra of A st A1 = m & (f . m) = ( MSAlg A1) by A3;

          

          thus (f . (a1 "/\" b1)) = (f . (( UniAlg_meet A) . (a2,b2))) by LATTICES:def 2

          .= ( MSAlg (a3 /\ b3)) by A9, UNIALG_2:def 16

          .= (g1 /\ g2) by Th31

          .= (the L_meet of ( MSSubAlLattice ( MSAlg A)) . ((f . a1),(f . b1))) by A7, A8, A5, A6, MSUALG_2:def 21

          .= ((f . a1) "/\" (f . b1)) by LATTICES:def 2;

        end;

        hence thesis by AA;

      end;

      then

      reconsider f as Homomorphism of ( UnSubAlLattice A), ( MSSubAlLattice ( MSAlg A));

      take f;

      now

        let x1,x2 be object such that

         A11: x1 in ( dom f) & x2 in ( dom f) and

         A12: (f . x1) = (f . x2);

        reconsider y1 = x1, y2 = x2 as Element of ( Sub A) by A11, FUNCT_2:def 1;

        consider A1 be strict SubAlgebra of A such that

         A13: A1 = y1 and

         A14: (f . y1) = ( MSAlg A1) by A3;

        consider A2 be strict SubAlgebra of A such that

         A15: A2 = y2 & (f . y2) = ( MSAlg A2) by A3;

        

         A16: ( MSSign A1) = ( MSSign A) by Th7

        .= ( MSSign A2) by Th7;

        

        thus x1 = ( 1-Alg ( MSAlg A1)) by A13, MSUALG_1: 9

        .= x2 by A12, A14, A15, A16, MSUALG_1: 9;

      end;

      hence f is one-to-one by FUNCT_1:def 4;

      

       A17: ( dom f) = ( Sub A) by FUNCT_2:def 1;

      thus ( rng f) = the carrier of ( MSSubAlLattice ( MSAlg A))

      proof

        thus ( rng f) c= the carrier of ( MSSubAlLattice ( MSAlg A)) by RELAT_1:def 19;

        let x be object;

        assume x in the carrier of ( MSSubAlLattice ( MSAlg A));

        then

        reconsider y = x as strict MSSubAlgebra of ( MSAlg A) by MSUALG_2:def 19;

        reconsider C = ( Constants ( MSAlg A)) as MSSubset of y by MSUALG_2: 10;

        C c= the Sorts of y by PBOOLE:def 18;

        then the Sorts of y is non-empty by PBOOLE: 131;

        then

        reconsider y as strict non-empty MSSubAlgebra of ( MSAlg A) by MSUALG_1:def 3;

        ( 1-Alg y) is SubAlgebra of ( 1-Alg ( MSAlg A)) by Th20;

        then ( 1-Alg y) is SubAlgebra of A by MSUALG_1: 9;

        then

        reconsider y1 = ( 1-Alg y) as Element of ( Sub A) by UNIALG_2:def 14;

        ex A1 be strict SubAlgebra of A st A1 = y1 & (f . y1) = ( MSAlg A1) by A3;

        then

         A18: (f . ( 1-Alg y)) = x by A1, Th26;

        y1 in ( dom f) by A17;

        hence thesis by A18, FUNCT_1:def 3;

      end;

    end;