unialg_2.miz

    begin

    reserve U0,U1,U2,U3 for Universal_Algebra,

n for Nat,

x,y for set;

    definition

      let U1;

      mode PFuncsDomHQN of U1 is PFuncsDomHQN of the carrier of U1;

    end

    definition

      let U1 be UAStr;

      mode PartFunc of U1 is PartFunc of (the carrier of U1 * ), the carrier of U1;

    end

    definition

      let U1, U2;

      :: UNIALG_2:def1

      pred U1,U2 are_similar means ( signature U1) = ( signature U2);

      symmetry ;

      reflexivity ;

    end

    theorem :: UNIALG_2:1

    (U1,U2) are_similar implies ( len the charact of U1) = ( len the charact of U2)

    proof



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

      assume (U1,U2) are_similar ;

      hence thesis by A1;

    end;

    theorem :: UNIALG_2:2

    (U1,U2) are_similar & (U2,U3) are_similar implies (U1,U3) are_similar ;

    theorem :: UNIALG_2:3

    ( rng the charact of U0) is non empty Subset of ( PFuncs ((the carrier of U0 * ),the carrier of U0)) by FINSEQ_1:def 4, RELAT_1: 41;

    definition

      let U0;

      :: UNIALG_2:def2

      func Operations (U0) -> PFuncsDomHQN of U0 equals ( rng the charact of U0);

      coherence

      proof

        reconsider A = ( rng the charact of U0) as non empty set by RELAT_1: 41;

        now

          let x be Element of A;

          consider i be Nat such that

           A1: i in ( dom the charact of U0) and

           A2: (the charact of U0 . i) = x by FINSEQ_2: 10;

          reconsider p = (the charact of U0 . i) as PartFunc of U0 by A1, UNIALG_1: 1;

          p is homogeneous quasi_total non empty by A1, FUNCT_1:def 9, MARGREL1:def 24;

          hence x is homogeneous quasi_total non empty PartFunc of U0 by A2;

        end;

        hence thesis by MARGREL1:def 26;

      end;

    end

    definition

      let U1;

      mode operation of U1 is Element of ( Operations U1);

    end

    reserve A for non empty Subset of U0,

o for operation of U0,

x1,y1 for FinSequence of A;

    definition

      let U0 be Universal_Algebra, A be Subset of U0, o be operation of U0;

      :: UNIALG_2:def3

      pred A is_closed_on o means for s be FinSequence of A st ( len s) = ( arity o) holds (o . s) in A;

    end

    definition

      let U0 be Universal_Algebra, A be Subset of U0;

      :: UNIALG_2:def4

      attr A is opers_closed means for o be operation of U0 holds A is_closed_on o;

    end

    definition

      let U0, A, o;

      assume

       A1: A is_closed_on o;

      :: UNIALG_2:def5

      func o /. A -> homogeneous quasi_total non empty PartFunc of (A * ), A equals

      : Def5: (o | (( arity o) -tuples_on A));

      coherence

      proof



         A2: (( arity o) -tuples_on A) c= (( arity o) -tuples_on the carrier of U0)

        proof

          let x be object;

          assume x in (( arity o) -tuples_on A);

          then x in { s where s be Element of (A * ) : ( len s) = ( arity o) } by FINSEQ_2:def 4;

          then

          consider s be Element of (A * ) such that

           A3: x = s and

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

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

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

          then

          reconsider s as FinSequence of the carrier of U0 by FINSEQ_1:def 4;

          reconsider s as Element of (the carrier of U0 * ) by FINSEQ_1:def 11;

          x = s by A3;

          then x in { s1 where s1 be Element of (the carrier of U0 * ) : ( len s1) = ( arity o) } by A4;

          hence thesis by FINSEQ_2:def 4;

        end;



         A5: ( dom (o | (( arity o) -tuples_on A))) = (( dom o) /\ (( arity o) -tuples_on A)) by RELAT_1: 61

        .= ((( arity o) -tuples_on the carrier of U0) /\ (( arity o) -tuples_on A)) by MARGREL1: 22

        .= (( arity o) -tuples_on A) by A2, XBOOLE_1: 28;



         A6: ( rng (o | (( arity o) -tuples_on A))) c= A

        proof

          let x be object;

          assume x in ( rng (o | (( arity o) -tuples_on A)));

          then

          consider y be object such that

           A7: y in ( dom (o | (( arity o) -tuples_on A))) and

           A8: x = ((o | (( arity o) -tuples_on A)) . y) by FUNCT_1:def 3;

          y in { s where s be Element of (A * ) : ( len s) = ( arity o) } by A5, A7, FINSEQ_2:def 4;

          then

          consider s be Element of (A * ) such that

           A9: y = s and

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

          ((o | (( arity o) -tuples_on A)) . s) = (o . s) by A7, A9, FUNCT_1: 47;

          hence thesis by A1, A8, A9, A10;

        end;

        (( arity o) -tuples_on A) in the set of all (i -tuples_on A) where i be Nat;

        then (( arity o) -tuples_on A) c= ( union the set of all (i -tuples_on A) where i be Nat) by ZFMISC_1: 74;

        then ( dom (o | (( arity o) -tuples_on A))) c= (A * ) by A5, FINSEQ_2: 108;

        then

        reconsider oa = (o | (( arity o) -tuples_on A)) as PartFunc of (A * ), A by A6, RELSET_1: 4;



         A11: oa is homogeneous

        proof

          let x1,y1 be FinSequence;

          assume that

           A12: x1 in ( dom oa) and

           A13: y1 in ( dom oa);

          y1 in { s1 where s1 be Element of (A * ) : ( len s1) = ( arity o) } by A5, A13, FINSEQ_2:def 4;

          then

           A14: ex s1 be Element of (A * ) st y1 = s1 & ( len s1) = ( arity o);

          x1 in { s where s be Element of (A * ) : ( len s) = ( arity o) } by A5, A12, FINSEQ_2:def 4;

          then ex s be Element of (A * ) st x1 = s & ( len s) = ( arity o);

          hence thesis by A14;

        end;

        oa is quasi_total

        proof

          let x1, y1;

          assume that

           A15: ( len x1) = ( len y1) and

           A16: x1 in ( dom oa);

          x1 in { s where s be Element of (A * ) : ( len s) = ( arity o) } by A5, A16, FINSEQ_2:def 4;

          then ex s be Element of (A * ) st x1 = s & ( len s) = ( arity o);

          then y1 is Element of (( arity o) -tuples_on A) by A15, FINSEQ_2: 92;

          hence thesis by A5;

        end;

        hence thesis by A5, A11;

      end;

    end

    definition

      let U0, A;

      :: UNIALG_2:def6

      func Opers (U0,A) -> PFuncFinSequence of A means

      : Def6: ( dom it ) = ( dom the charact of U0) & for n be set, o st n in ( dom it ) & o = (the charact of U0 . n) holds (it . n) = (o /. A);

      existence

      proof

        defpred P[ Nat, set] means for o st o = (the charact of U0 . $1) holds $2 = (o /. A);



         A1: for n be Nat st n in ( Seg ( len the charact of U0)) holds ex x be Element of ( PFuncs ((A * ),A)) st P[n, x]

        proof

          let n be Nat;

          assume n in ( Seg ( len the charact of U0));

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

          then

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

          reconsider x = (o1 /. A) as Element of ( PFuncs ((A * ),A)) by PARTFUN1: 45;

          take x;

          let o;

          assume o = (the charact of U0 . n);

          hence thesis;

        end;

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

         A2: ( dom p) = ( Seg ( len the charact of U0)) and

         A3: for n be Nat st n in ( Seg ( len the charact of U0)) holds P[n, (p . n)] from FINSEQ_1:sch 5( A1);

        reconsider p as PFuncFinSequence of A;

        take p;

        thus ( dom p) = ( dom the charact of U0) by A2, FINSEQ_1:def 3;

        let n be set, o;

        assume n in ( dom p) & o = (the charact of U0 . n);

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        let p1,p2 be PFuncFinSequence of A;

        assume that

         A4: ( dom p1) = ( dom the charact of U0) and

         A5: for n be set, o st n in ( dom p1) & o = (the charact of U0 . n) holds (p1 . n) = (o /. A) and

         A6: ( dom p2) = ( dom the charact of U0) and

         A7: for n be set, o st n in ( dom p2) & o = (the charact of U0 . n) holds (p2 . n) = (o /. A);

        for n be Nat st n in ( dom the charact of U0) holds (p1 . n) = (p2 . n)

        proof

          let n be Nat;

          assume

           A8: n in ( dom the charact of U0);

          then

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

          (p1 . n) = (k /. A) by A4, A5, A8;

          hence thesis by A6, A7, A8;

        end;

        hence thesis by A4, A6, FINSEQ_1: 13;

      end;

    end

    theorem :: UNIALG_2:4



     Th4: for B be non empty Subset of U0 st B = the carrier of U0 holds B is opers_closed & for o holds (o /. B) = o

    proof

      let B be non empty Subset of U0;

      assume

       A1: B = the carrier of U0;



       A2: for o holds B is_closed_on o

      proof

        let o;

        let s be FinSequence of B;

        assume

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

        ( dom o) = (( arity o) -tuples_on B) & s is Element of (( len s) -tuples_on B) by A1, FINSEQ_2: 92, MARGREL1: 22;

        then

         A4: (o . s) in ( rng o) by A3, FUNCT_1:def 3;

        ( rng o) c= B by A1, RELAT_1:def 19;

        hence thesis by A4;

      end;

      for o holds (o /. B) = o

      proof

        let o;

        ( dom o) = (( arity o) -tuples_on B) & (o /. B) = (o | (( arity o) -tuples_on B)) by A1, A2, Def5, MARGREL1: 22;

        hence thesis by RELAT_1: 68;

      end;

      hence thesis by A2;

    end;

    theorem :: UNIALG_2:5

    for U1 be Universal_Algebra, A be non empty Subset of U1, o be operation of U1 st A is_closed_on o holds ( arity (o /. A)) = ( arity o)

    proof

      let U1 be Universal_Algebra, A be non empty Subset of U1, o be operation of U1;

      assume A is_closed_on o;

      then (o /. A) = (o | (( arity o) -tuples_on A)) by Def5;

      then ( dom (o /. A)) = (( dom o) /\ (( arity o) -tuples_on A)) by RELAT_1: 61;



      then

       A1: ( dom (o /. A)) = ((( arity o) -tuples_on the carrier of U1) /\ (( arity o) -tuples_on A)) by MARGREL1: 22

      .= (( arity o) -tuples_on A) by MARGREL1: 21;

      ( dom (o /. A)) = (( arity (o /. A)) -tuples_on A) by MARGREL1: 22;

      hence thesis by A1, FINSEQ_2: 110;

    end;

    definition

      let U0;

      :: UNIALG_2:def7

      mode SubAlgebra of U0 -> Universal_Algebra means

      : Def7: the carrier of it is Subset of U0 & for B be non empty Subset of U0 st B = the carrier of it holds the charact of it = ( Opers (U0,B)) & B is opers_closed;

      existence

      proof

        take U1 = U0;



         A1: for B be non empty Subset of U0 st B = the carrier of U0 holds the charact of U0 = ( Opers (U0,B)) & B is opers_closed

        proof

          let B be non empty Subset of U0;

          assume

           A2: B = the carrier of U0;



           A3: ( dom the charact of U0) = ( dom ( Opers (U0,B))) by Def6;

          for n be Nat st n in ( dom the charact of U0) holds (the charact of U0 . n) = (( Opers (U0,B)) . n)

          proof

            let n be Nat;

            assume

             A4: n in ( dom the charact of U0);

            then

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

            (( Opers (U0,B)) . n) = (o /. B) by A3, A4, Def6;

            hence thesis by A2, Th4;

          end;

          hence thesis by A2, A3, Th4, FINSEQ_1: 13;

        end;

        the carrier of U1 c= the carrier of U1;

        hence thesis by A1;

      end;

    end

    registration

      let U0 be Universal_Algebra;

      cluster strict for SubAlgebra of U0;

      existence

      proof

        reconsider S = UAStr (# the carrier of U0, the charact of U0 #) as strict Universal_Algebra by UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;



         A1: the carrier of S c= the carrier of U0;

        for B be non empty Subset of U0 st B = the carrier of S holds the charact of S = ( Opers (U0,B)) & B is opers_closed

        proof

          let B be non empty Subset of U0;

          assume

           A2: B = the carrier of S;

           A3:

          now

            let n be Nat;

            assume

             A4: n in ( dom the charact of U0);

            then

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

            n in ( dom ( Opers (U0,B))) by A4, Def6;



            hence (( Opers (U0,B)) . n) = (o /. B) by Def6

            .= (the charact of U0 . n) by A2, Th4;

          end;

          ( dom the charact of U0) = ( dom ( Opers (U0,B))) by Def6;

          hence thesis by A2, A3, Th4, FINSEQ_1: 13;

        end;

        then

        reconsider S as SubAlgebra of U0 by A1, Def7;

        take S;

        thus thesis;

      end;

    end

    theorem :: UNIALG_2:6



     Th6: for U0,U1 be Universal_Algebra, o0 be operation of U0, o1 be operation of U1, n be Nat st U0 is SubAlgebra of U1 & n in ( dom the charact of U0) & o0 = (the charact of U0 . n) & o1 = (the charact of U1 . n) holds ( arity o0) = ( arity o1)

    proof

      let U0,U1 be Universal_Algebra, o0 be operation of U0, o1 be operation of U1, n;

      assume that

       A1: U0 is SubAlgebra of U1 and

       A2: n in ( dom the charact of U0) & o0 = (the charact of U0 . n) and

       A3: o1 = (the charact of U1 . n);

      reconsider A = the carrier of U0 as non empty Subset of U1 by A1, Def7;

      A is opers_closed by A1, Def7;

      then

       A4: A is_closed_on o1;

      n in ( dom ( Opers (U1,A))) & o0 = (( Opers (U1,A)) . n) by A1, A2, Def7;

      then o0 = (o1 /. A) by A3, Def6;

      then o0 = (o1 | (( arity o1) -tuples_on A)) by A4, Def5;

      then ( dom o0) = (( dom o1) /\ (( arity o1) -tuples_on A)) by RELAT_1: 61;



      then

       A5: ( dom o0) = ((( arity o1) -tuples_on the carrier of U1) /\ (( arity o1) -tuples_on A)) by MARGREL1: 22

      .= (( arity o1) -tuples_on A) by MARGREL1: 21;

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

      hence thesis by A5, FINSEQ_2: 110;

    end;

    theorem :: UNIALG_2:7



     Th7: U0 is SubAlgebra of U1 implies ( dom the charact of U0) = ( dom the charact of U1)

    proof

      assume

       A1: U0 is SubAlgebra of U1;

      then

      reconsider A = the carrier of U0 as non empty Subset of U1 by Def7;

      the charact of U0 = ( Opers (U1,A)) by A1, Def7;

      hence thesis by Def6;

    end;

    theorem :: UNIALG_2:8

    U0 is SubAlgebra of U0

    proof



       A1: for B be non empty Subset of U0 st B = the carrier of U0 holds the charact of U0 = ( Opers (U0,B)) & B is opers_closed

      proof

        let B be non empty Subset of U0;

        assume

         A2: B = the carrier of U0;



         A3: ( dom the charact of U0) = ( dom ( Opers (U0,B))) by Def6;

        for n be Nat st n in ( dom the charact of U0) holds (the charact of U0 . n) = (( Opers (U0,B)) . n)

        proof

          let n be Nat;

          assume

           A4: n in ( dom the charact of U0);

          then

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

          (( Opers (U0,B)) . n) = (o /. B) by A3, A4, Def6;

          hence thesis by A2, Th4;

        end;

        hence thesis by A2, A3, Th4, FINSEQ_1: 13;

      end;

      the carrier of U0 c= the carrier of U0;

      hence thesis by A1, Def7;

    end;

    theorem :: UNIALG_2:9

    U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 implies U0 is SubAlgebra of U2

    proof

      assume that

       A1: U0 is SubAlgebra of U1 and

       A2: U1 is SubAlgebra of U2;



       A3: the carrier of U0 is Subset of U1 by A1, Def7;

      reconsider B2 = the carrier of U1 as non empty Subset of U2 by A2, Def7;



       A4: the charact of U1 = ( Opers (U2,B2)) by A2, Def7;

      the carrier of U1 is Subset of U2 by A2, Def7;

      hence the carrier of U0 is Subset of U2 by A3, XBOOLE_1: 1;

      let B be non empty Subset of U2;

      assume

       A5: B = the carrier of U0;

      reconsider B1 = the carrier of U0 as non empty Subset of U1 by A1, Def7;



       A6: the charact of U0 = ( Opers (U1,B1)) by A1, Def7;



       A7: B2 is opers_closed by A2, Def7;



       A8: ( dom the charact of U1) = ( dom ( Opers (U2,B2))) by A2, Def7

      .= ( dom the charact of U2) by Def6;



       A9: B1 is opers_closed by A1, Def7;

       A10:

      now

        let o2 be operation of U2;

        consider n be Nat such that

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

         A12: (the charact of U2 . n) = o2 by FINSEQ_2: 10;



         A13: ( dom the charact of U2) = ( dom ( Opers (U2,B2))) by Def6;

        then

        reconsider o21 = (the charact of U1 . n) as operation of U1 by A4, A11, FUNCT_1:def 3;



         A14: ( dom o21) = (( arity o21) -tuples_on the carrier of U1) by MARGREL1: 22;



         A15: ( dom the charact of U1) = ( dom ( Opers (U1,B1))) by Def6;

        then

        reconsider o20 = (the charact of U0 . n) as operation of U0 by A6, A4, A11, A13, FUNCT_1:def 3;



         A16: ( dom o20) = (( arity o20) -tuples_on the carrier of U0) by MARGREL1: 22;



         A17: ( dom o2) = (( arity o2) -tuples_on the carrier of U2) & ( dom (o2 | (( arity o2) -tuples_on B2))) = (( dom o2) /\ (( arity o2) -tuples_on B2)) by MARGREL1: 22, RELAT_1: 61;



         A18: B2 is_closed_on o2 by A7;



         A19: o21 = (o2 /. B2) by A4, A11, A12, A13, Def6;

        then o21 = (o2 | (( arity o2) -tuples_on B2)) by A18, Def5;

        then

         A20: ( arity o2) = ( arity o21) by A14, A17, FINSEQ_2: 110, MARGREL1: 21;



         A21: B1 is_closed_on o21 by A9;



         A22: o20 = (o21 /. B1) by A6, A4, A11, A13, A15, Def6;

        then o20 = (o21 | (( arity o21) -tuples_on B1)) by A21, Def5;

        then (( arity o20) -tuples_on B1) = ((( arity o21) -tuples_on the carrier of U1) /\ (( arity o21) -tuples_on B1)) by A16, A14, RELAT_1: 61;

        then

         A23: ( arity o20) = ( arity o21) by FINSEQ_2: 110, MARGREL1: 21;

        now

          let s be FinSequence of B;

          reconsider s1 = s as Element of (B1 * ) by A5, FINSEQ_1:def 11;

          reconsider s0 = s as Element of (the carrier of U0 * ) by A5, FINSEQ_1:def 11;



           A24: ( rng o20) c= B by A5, RELAT_1:def 19;

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

          then ( rng s) c= B2 by A3, A5, XBOOLE_1: 1;

          then s is FinSequence of B2 by FINSEQ_1:def 4;

          then

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

          assume

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

          then s2 in { w where w be Element of (B2 * ) : ( len w) = ( arity o2) };

          then

           A26: s2 in (( arity o2) -tuples_on B2) by FINSEQ_2:def 4;

          s0 in { w where w be Element of (the carrier of U0 * ) : ( len w) = ( arity o20) } by A23, A20, A25;

          then s0 in (( arity o20) -tuples_on the carrier of U0) by FINSEQ_2:def 4;

          then

           A27: (o20 . s0) in ( rng o20) by A16, FUNCT_1:def 3;

          s1 in { w where w be Element of (B1 * ) : ( len w) = ( arity o21) } by A20, A25;

          then

           A28: s1 in (( arity o21) -tuples_on B1) by FINSEQ_2:def 4;

          (o20 . s0) = ((o21 | (( arity o21) -tuples_on B1)) . s1) by A21, A22, Def5

          .= (o21 . s1) by A28, FUNCT_1: 49

          .= ((o2 | (( arity o2) -tuples_on B2)) . s2) by A18, A19, Def5

          .= (o2 . s) by A26, FUNCT_1: 49;

          hence (o2 . s) in B by A27, A24;

        end;

        hence B is_closed_on o2;

      end;



       A29: ( dom the charact of U0) = ( dom ( Opers (U1,B1))) by A1, Def7

      .= ( dom the charact of U1) by Def6;



       A30: ( dom the charact of U2) = ( dom ( Opers (U2,B))) by Def6;



       A31: B = B1 by A5;

      now

        let n be Nat;

        assume

         A32: n in ( dom ( Opers (U2,B)));

        then

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

        reconsider o21 = (the charact of U1 . n) as operation of U1 by A8, A30, A32, FUNCT_1:def 3;



         A33: B2 is_closed_on o2 by A7;



         A34: B1 is_closed_on o21 by A9;



        thus (( Opers (U2,B)) . n) = (o2 /. B) by A32, Def6

        .= (o2 | (( arity o2) -tuples_on B)) by A10, Def5

        .= (o2 | ((( arity o2) -tuples_on B2) /\ (( arity o2) -tuples_on B))) by A31, MARGREL1: 21

        .= ((o2 | (( arity o2) -tuples_on B2)) | (( arity o2) -tuples_on B)) by RELAT_1: 71

        .= ((o2 /. B2) | (( arity o2) -tuples_on B)) by A33, Def5

        .= (o21 | (( arity o2) -tuples_on B)) by A4, A8, A30, A32, Def6

        .= (o21 | (( arity o21) -tuples_on B1)) by A2, A5, A8, A30, A32, Th6

        .= (o21 /. B1) by A34, Def5

        .= (the charact of U0 . n) by A6, A29, A8, A30, A32, Def6;

      end;

      hence the charact of U0 = ( Opers (U2,B)) by A29, A8, A30, FINSEQ_1: 13;

      thus thesis by A10;

    end;

    theorem :: UNIALG_2:10



     Th10: U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 implies U1 = U2

    proof

      assume that

       A1: U1 is strict SubAlgebra of U2 and

       A2: U2 is strict SubAlgebra of U1;

      reconsider B = the carrier of U1 as non empty Subset of U2 by A1, Def7;

      the carrier of U2 c= the carrier of U2;

      then

      reconsider B1 = the carrier of U2 as non empty Subset of U2;



       A3: ( dom ( Opers (U2,B1))) = ( dom the charact of U2) by Def6;



       A4: for n be Nat st n in ( dom the charact of U2) holds (the charact of U2 . n) = (( Opers (U2,B1)) . n)

      proof

        let n be Nat;

        assume

         A5: n in ( dom the charact of U2);

        then

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

        (( Opers (U2,B1)) . n) = (o /. B1) by A3, A5, Def6

        .= o by Th4;

        hence thesis;

      end;

      the carrier of U2 is Subset of U1 by A2, Def7;

      then

       A6: B1 = B;

      then the charact of U1 = ( Opers (U2,B1)) by A1, Def7;

      hence thesis by A1, A2, A6, A3, A4, FINSEQ_1: 13;

    end;

    theorem :: UNIALG_2:11



     Th11: for U1,U2 be SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds U1 is SubAlgebra of U2

    proof

      let U1,U2 be SubAlgebra of U0;



       A1: ( dom the charact of U1) = ( dom the charact of U0) by Th7;

      reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7;

      assume

       A2: the carrier of U1 c= the carrier of U2;

      hence the carrier of U1 is Subset of U2;

      let B be non empty Subset of U2;

      assume

       A3: B = the carrier of U1;

      reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7;



       A4: the charact of U2 = ( Opers (U0,B2)) by Def7;



       A5: B2 is opers_closed by Def7;



       A6: ( dom ( Opers (U2,B))) = ( dom the charact of U2) by Def6;



       A7: ( dom the charact of U2) = ( dom the charact of U0) by Th7;



       A8: B1 is opers_closed by Def7;



       A9: B is opers_closed

      proof

        let o2 be operation of U2;

        let s be FinSequence of B;

        consider n be Nat such that

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

         A11: (the charact of U2 . n) = o2 by FINSEQ_2: 10;

        reconsider o0 = (the charact of U0 . n) as operation of U0 by A7, A10, FUNCT_1:def 3;



         A12: ( arity o2) = ( arity o0) by A10, A11, Th6;

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

        then ( rng s) c= B2 by XBOOLE_1: 1;

        then s is FinSequence of B2 by FINSEQ_1:def 4;

        then

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

        reconsider s1 = s as Element of (B1 * ) by A3, FINSEQ_1:def 11;

        assume

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

        set tb2 = (( arity o0) -tuples_on B2);



         A14: B2 is_closed_on o0 by A5;



         A15: o2 = (o0 /. B2) by A4, A10, A11, Def6

        .= (o0 | tb2) by A14, Def5;



         A16: B1 is_closed_on o0 by A8;

        tb2 = { w where w be Element of (B2 * ) : ( len w) = ( arity o0) } by FINSEQ_2:def 4;

        then s2 in tb2 by A13, A12;

        then (o2 . s) = (o0 . s1) by A15, FUNCT_1: 49;

        hence thesis by A3, A13, A16, A12;

      end;



       A17: the charact of U1 = ( Opers (U0,B1)) by Def7;

      now

        let n be Nat;

        assume

         A18: n in ( dom the charact of U0);

        then

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

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



         A19: o2 = (o0 /. B2) & ( arity o2) = ( arity o0) by A4, A7, A18, Def6, Th6;



         A20: B is_closed_on o2 by A9;



         A21: B2 is_closed_on o0 by A5;



         A22: B1 is_closed_on o0 by A8;



        thus (the charact of U1 . n) = (o0 /. B1) by A17, A1, A18, Def6

        .= (o0 | (( arity o0) -tuples_on B1)) by A22, Def5

        .= (o0 | ((( arity o0) -tuples_on B2) /\ (( arity o0) -tuples_on B1))) by A2, MARGREL1: 21

        .= ((o0 | (( arity o0) -tuples_on B2)) | (( arity o0) -tuples_on B)) by A3, RELAT_1: 71

        .= ((o0 /. B2) | (( arity o0) -tuples_on B)) by A21, Def5

        .= (o2 /. B) by A20, A19, Def5

        .= (( Opers (U2,B)) . n) by A7, A6, A18, Def6;

      end;

      hence the charact of U1 = ( Opers (U2,B)) by A1, A7, A6, FINSEQ_1: 13;

      thus thesis by A9;

    end;

    theorem :: UNIALG_2:12



     Th12: for U1,U2 be strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2 holds U1 = U2

    proof

      let U1,U2 be strict SubAlgebra of U0;

      assume the carrier of U1 = the carrier of U2;

      then U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 by Th11;

      hence thesis by Th10;

    end;

    theorem :: UNIALG_2:13

    U1 is SubAlgebra of U2 implies (U1,U2) are_similar

    proof

      set s1 = ( signature U1), s2 = ( signature U2);

      set X = ( dom s1);

      ( len s1) = ( len the charact of U1) by UNIALG_1:def 4;

      then

       A1: ( dom s1) = ( dom the charact of U1) by FINSEQ_3: 29;

      assume

       A2: U1 is SubAlgebra of U2;

      then

      reconsider A = the carrier of U1 as non empty Subset of U2 by Def7;

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

      then

       A3: ( dom s2) = ( dom the charact of U2) by FINSEQ_3: 29;

      ( dom the charact of U1) = ( dom ( Opers (U2,A))) by A2, Def7;

      then

       A4: ( dom s1) = ( dom s2) by A1, A3, Def6;

      the charact of U1 = ( Opers (U2,A)) by A2, Def7;

      then

       A5: ( dom s1) c= ( dom s2) by A1, A3, Def6;

      for n be Nat st n in X holds (s1 . n) = (s2 . n)

      proof

        let n be Nat;

        assume

         A6: n in X;

        then

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

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

        (s1 . n) = ( arity o1) & (s2 . n) = ( arity o2) by A5, A6, UNIALG_1:def 4;

        hence thesis by A2, A1, A6, Th6;

      end;

      then s1 = s2 by A4, FINSEQ_1: 13;

      hence thesis;

    end;

    theorem :: UNIALG_2:14



     Th14: for A be non empty Subset of U0 holds UAStr (# A, ( Opers (U0,A)) #) is strict Universal_Algebra

    proof

      let A be non empty Subset of U0;

      set C = UAStr (# A, ( Opers (U0,A)) #);



       A1: ( dom the charact of C) = ( dom the charact of U0) by Def6;

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

      proof

        let n be object;

        assume

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

        then

        reconsider o = (the charact of U0 . n) as operation of U0 by A1, FUNCT_1:def 3;

        (the charact of C . n) = (o /. A) by A2, Def6;

        hence thesis;

      end;

      then

       A3: the charact of C is non-empty by FUNCT_1:def 9;

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

      proof

        let n;

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

        assume that

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

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

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

        h = (o /. A) by A4, A5, Def6;

        hence thesis;

      end;

      then

       A6: the charact of C is quasi_total;

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

      proof

        let n;

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

        assume that

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

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

        reconsider o = (the charact of U0 . n) as operation of U0 by A1, A7, FUNCT_1:def 3;

        h = (o /. A) by A7, A8, Def6;

        hence thesis;

      end;

      then

       A9: the charact of C is homogeneous;

      the charact of C <> {} by A1, RELAT_1: 38, RELAT_1: 41;

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

    end;

    definition

      let U0 be Universal_Algebra, A be non empty Subset of U0;

      assume

       A1: A is opers_closed;

      :: UNIALG_2:def8

      func UniAlgSetClosed (A) -> strict SubAlgebra of U0 equals

      : Def8: UAStr (# A, ( Opers (U0,A)) #);

      coherence

      proof

        reconsider C = UAStr (# A, ( Opers (U0,A)) #) as strict Universal_Algebra by Th14;

        for B be non empty Subset of U0 st B = the carrier of C holds the charact of C = ( Opers (U0,B)) & B is opers_closed by A1;

        hence thesis by Def7;

      end;

    end

    definition

      let U0;

      let U1,U2 be SubAlgebra of U0;

      assume

       A1: the carrier of U1 meets the carrier of U2;

      :: UNIALG_2:def9

      func U1 /\ U2 -> strict SubAlgebra of U0 means

      : Def9: the carrier of it = (the carrier of U1 /\ the carrier of U2) & for B be non empty Subset of U0 st B = the carrier of it holds the charact of it = ( Opers (U0,B)) & B is opers_closed;

      existence

      proof



         A2: (the carrier of U1 /\ the carrier of U2) c= the carrier of U1 by XBOOLE_1: 17;

        the carrier of U1 is Subset of U0 by Def7;

        then

        reconsider C = (the carrier of U1 /\ the carrier of U2) as non empty Subset of U0 by A1, A2, XBOOLE_1: 1;

        set S = UAStr (# C, ( Opers (U0,C)) #);



         A3: (the carrier of U1 /\ the carrier of U2) c= the carrier of U2 by XBOOLE_1: 17;

         A4:

        now

          let o be operation of U0;

          now

            set B1 = the carrier of U1, B2 = the carrier of U2;

            let s be FinSequence of C;

            reconsider s2 = s as FinSequence of B2 by A3, FINSEQ_2: 24;

            reconsider s1 = s as FinSequence of B1 by A2, FINSEQ_2: 24;

            assume

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

            reconsider B1 as non empty Subset of U0 by Def7;

            reconsider B2 as non empty Subset of U0 by Def7;

            B2 is opers_closed by Def7;

            then B2 is_closed_on o;

            then

             A6: (o . s2) in B2 by A5;

            B1 is opers_closed by Def7;

            then B1 is_closed_on o;

            then (o . s1) in B1 by A5;

            hence (o . s) in C by A6, XBOOLE_0:def 4;

          end;

          hence C is_closed_on o;

        end;

        then

         A7: for B be non empty Subset of U0 st B = the carrier of S holds the charact of S = ( Opers (U0,B)) & B is opers_closed;

        reconsider S as Universal_Algebra by Th14;

        reconsider S as strict SubAlgebra of U0 by A7, Def7;

        take S;

        thus thesis by A4;

      end;

      uniqueness

      proof

        the carrier of U1 is Subset of U0 & (the carrier of U1 /\ the carrier of U2) c= the carrier of U1 by Def7, XBOOLE_1: 17;

        then

        reconsider C = (the carrier of U1 /\ the carrier of U2) as non empty Subset of U0 by A1, XBOOLE_1: 1;

        let W1,W2 be strict SubAlgebra of U0;

        assume that

         A8: the carrier of W1 = (the carrier of U1 /\ the carrier of U2) & for B1 be non empty Subset of U0 st B1 = the carrier of W1 holds the charact of W1 = ( Opers (U0,B1)) & B1 is opers_closed and

         A9: the carrier of W2 = (the carrier of U1 /\ the carrier of U2) and

         A10: for B2 be non empty Subset of U0 st B2 = the carrier of W2 holds the charact of W2 = ( Opers (U0,B2)) & B2 is opers_closed;

        the charact of W2 = ( Opers (U0,C)) by A9, A10;

        hence thesis by A8, A9;

      end;

    end

    definition

      let U0;

      :: UNIALG_2:def10

      func Constants (U0) -> Subset of U0 equals { a where a be Element of U0 : ex o be operation of U0 st ( arity o) = 0 & a in ( rng o) };

      coherence

      proof

        set E = { a where a be Element of U0 : ex o be operation of U0 st ( arity o) = 0 & a in ( rng o) };

        E c= the carrier of U0

        proof

          let x be object;

          assume x in E;

          then ex w be Element of U0 st w = x & ex o be operation of U0 st ( arity o) = 0 & w in ( rng o);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let IT be Universal_Algebra;

      :: UNIALG_2:def11

      attr IT is with_const_op means

      : Def11: ex o be operation of IT st ( arity o) = 0 ;

    end

    registration

      cluster with_const_op strict for Universal_Algebra;

      existence

      proof

        set A = the non empty set;

        set a = the Element of A;

        reconsider w = (( <*> A) .--> a) as Element of ( PFuncs ((A * ),A)) by MARGREL1: 19;

        set U0 = UAStr (# A, <*w*> #);



         A1: the charact of U0 is quasi_total & the charact of U0 is homogeneous by MARGREL1: 20;

        the charact of U0 is non-empty by MARGREL1: 20;

        then

        reconsider U0 as Universal_Algebra by A1, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;

        take U0;

        ( dom <*w*>) = {1} & 1 in {1} by FINSEQ_1: 2, FINSEQ_1: 38, TARSKI:def 1;

        then

        reconsider o = (the charact of U0 . 1) as operation of U0 by FUNCT_1:def 3;

        o = w by FINSEQ_1: 40;

        then

         A2: ( dom o) = {( <*> A)} by FUNCOP_1: 13;

         A3:

        now

          let x be FinSequence;

          assume x in ( dom o);

          then x = ( <*> A) by A2, TARSKI:def 1;

          hence ( len x) = 0 ;

        end;

        ( <*> A) in {( <*> A)} by TARSKI:def 1;

        then ( arity o) = 0 by A2, A3, MARGREL1:def 25;

        hence thesis;

      end;

    end

    registration

      let U0 be with_const_op Universal_Algebra;

      cluster ( Constants U0) -> non empty;

      coherence

      proof

        consider o be operation of U0 such that

         A1: ( arity o) = 0 by Def11;

        ( dom o) = ( 0 -tuples_on the carrier of U0) by A1, MARGREL1: 22

        .= {( <*> the carrier of U0)} by FINSEQ_2: 94;

        then ( <*> the carrier of U0) in ( dom o) by TARSKI:def 1;

        then

         A2: (o . ( <*> the carrier of U0)) in ( rng o) by FUNCT_1:def 3;

        ( rng o) c= the carrier of U0 by RELAT_1:def 19;

        then

        reconsider u = (o . ( <*> the carrier of U0)) as Element of U0 by A2;

        u in { a where a be Element of U0 : ex o be operation of U0 st ( arity o) = 0 & a in ( rng o) } by A1, A2;

        hence thesis;

      end;

    end

    theorem :: UNIALG_2:15



     Th15: for U0 be Universal_Algebra, U1 be SubAlgebra of U0 holds ( Constants U0) is Subset of U1

    proof

      let U0 be Universal_Algebra, U1 be SubAlgebra of U0;

      set u1 = the carrier of U1;

      ( Constants U0) c= u1

      proof

        reconsider B = u1 as non empty Subset of U0 by Def7;

        let x be object;

        assume x in ( Constants U0);

        then

        consider a be Element of U0 such that

         A1: a = x and

         A2: ex o be operation of U0 st ( arity o) = 0 & a in ( rng o);

        consider o0 be operation of U0 such that

         A3: ( arity o0) = 0 and

         A4: a in ( rng o0) by A2;

        consider y be object such that

         A5: y in ( dom o0) and

         A6: a = (o0 . y) by A4, FUNCT_1:def 3;

        ( dom o0) = ( 0 -tuples_on the carrier of U0) by A3, MARGREL1: 22

        .= {( <*> the carrier of U0)} by FINSEQ_2: 94;

        then y in {( <*> B)} by A5;

        then y in ( 0 -tuples_on B) by FINSEQ_2: 94;

        then y in (( dom o0) /\ (( arity o0) -tuples_on B)) by A3, A5, XBOOLE_0:def 4;

        then

         A7: y in ( dom (o0 | (( arity o0) -tuples_on B))) by RELAT_1: 61;

        consider n be Nat such that

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

         A9: (the charact of U0 . n) = o0 by FINSEQ_2: 10;



         A10: n in ( dom the charact of U1) by A8, Th7;

        then

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

        the charact of U1 = ( Opers (U0,B)) by Def7;

        then

         A11: o1 = (o0 /. B) by A9, A10, Def6;

        B is opers_closed by Def7;

        then

         A12: B is_closed_on o0;

        then y in ( dom (o0 /. B)) by A7, Def5;

        then

         A13: (o1 . y) in ( rng o1) by A11, FUNCT_1:def 3;



         A14: ( rng o1) c= the carrier of U1 by RELAT_1:def 19;

        (o1 . y) = ((o0 | (( arity o0) -tuples_on B)) . y) by A11, A12, Def5

        .= a by A6, A7, FUNCT_1: 47;

        hence thesis by A1, A13, A14;

      end;

      hence thesis;

    end;

    theorem :: UNIALG_2:16

    for U0 be with_const_op Universal_Algebra, U1 be SubAlgebra of U0 holds ( Constants U0) is non empty Subset of U1 by Th15;

    theorem :: UNIALG_2:17



     Th17: for U0 be with_const_op Universal_Algebra, U1,U2 be SubAlgebra of U0 holds the carrier of U1 meets the carrier of U2

    proof

      let U0 be with_const_op Universal_Algebra, U1,U2 be SubAlgebra of U0;

      set a = the Element of ( Constants U0);

      ( Constants U0) is non empty Subset of U1 & ( Constants U0) is non empty Subset of U2 by Th15;

      then

       A1: ( Constants U0) c= (the carrier of U1 /\ the carrier of U2) by XBOOLE_1: 19;

      thus thesis by A1;

    end;

    definition

      let U0 be Universal_Algebra, A be Subset of U0;

      assume

       A1: ( Constants U0) <> {} or A <> {} ;

      :: UNIALG_2:def12

      func GenUnivAlg (A) -> strict SubAlgebra of U0 means

      : Def12: A c= the carrier of it & for U1 be SubAlgebra of U0 st A c= the carrier of U1 holds it is SubAlgebra of U1;

      existence

      proof

        defpred P[ set] means A c= $1 & ( Constants U0) c= $1 & for B be non empty Subset of U0 st B = $1 holds B is opers_closed;

        set C = ( bool the carrier of U0);

        consider X be set such that

         A2: for x holds x in X iff x in C & P[x] from XFAMILY:sch 1;

        set P = ( meet X);

        the carrier of U0 in C & for B be non empty Subset of U0 st B = the carrier of U0 holds B is opers_closed by Th4, ZFMISC_1:def 1;

        then

         A3: the carrier of U0 in X by A2;



         A4: P c= the carrier of U0 by A3, SETFAM_1:def 1;

        now

          let x be set;

          assume x in X;

          then A c= x & ( Constants U0) c= x by A2;

          hence (A \/ ( Constants U0)) c= x by XBOOLE_1: 8;

        end;

        then

         A5: (A \/ ( Constants U0)) c= P by A3, SETFAM_1: 5;

        then

        reconsider P as non empty Subset of U0 by A1, A4;

        take E = ( UniAlgSetClosed P);



         A6: P is opers_closed

        proof

          let o be operation of U0;

          let s be FinSequence of P;

          assume

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

          now

            let a be set;



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

            assume

             A9: a in X;

            then

            reconsider a0 = a as Subset of U0 by A2;

            A c= a0 & ( Constants U0) c= a0 by A2, A9;

            then

            reconsider a0 as non empty Subset of U0 by A1;

            P c= a0 by A9, SETFAM_1: 3;

            then ( rng s) c= a0 by A8;

            then

            reconsider s0 = s as FinSequence of a0 by FINSEQ_1:def 4;

            a0 is opers_closed by A2, A9;

            then a0 is_closed_on o;

            then (o . s0) in a0 by A7;

            hence (o . s) in a;

          end;

          hence thesis by A3, SETFAM_1:def 1;

        end;

        then

         A10: E = UAStr (# P, ( Opers (U0,P)) #) by Def8;

        A c= (A \/ ( Constants U0)) by XBOOLE_1: 7;

        hence A c= the carrier of E by A5, A10;

        let U1 be SubAlgebra of U0;

        assume

         A11: A c= the carrier of U1;

        set u1 = the carrier of U1;



         A12: ( Constants U0) c= u1

        proof

          reconsider B = u1 as non empty Subset of U0 by Def7;

          let x be object;

          assume x in ( Constants U0);

          then

          consider a be Element of U0 such that

           A13: a = x and

           A14: ex o be operation of U0 st ( arity o) = 0 & a in ( rng o);

          consider o0 be operation of U0 such that

           A15: ( arity o0) = 0 and

           A16: a in ( rng o0) by A14;

          consider y be object such that

           A17: y in ( dom o0) and

           A18: a = (o0 . y) by A16, FUNCT_1:def 3;

          ( dom o0) = ( 0 -tuples_on the carrier of U0) by A15, MARGREL1: 22

          .= {( <*> the carrier of U0)} by FINSEQ_2: 94;

          then y in {( <*> B)} by A17;

          then y in ( 0 -tuples_on B) by FINSEQ_2: 94;

          then y in (( dom o0) /\ (( arity o0) -tuples_on B)) by A15, A17, XBOOLE_0:def 4;

          then

           A19: y in ( dom (o0 | (( arity o0) -tuples_on B))) by RELAT_1: 61;

          consider n be Nat such that

           A20: n in ( dom the charact of U0) and

           A21: (the charact of U0 . n) = o0 by FINSEQ_2: 10;



           A22: n in ( dom the charact of U1) by A20, Th7;

          then

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

          the charact of U1 = ( Opers (U0,B)) by Def7;

          then

           A23: o1 = (o0 /. B) by A21, A22, Def6;

          B is opers_closed by Def7;

          then

           A24: B is_closed_on o0;

          then y in ( dom (o0 /. B)) by A19, Def5;

          then

           A25: (o1 . y) in ( rng o1) by A23, FUNCT_1:def 3;



           A26: ( rng o1) c= the carrier of U1 by RELAT_1:def 19;

          (o1 . y) = ((o0 | (( arity o0) -tuples_on B)) . y) by A23, A24, Def5

          .= a by A18, A19, FUNCT_1: 47;

          hence thesis by A13, A25, A26;

        end;

        u1 is Subset of U0 & for B be non empty Subset of U0 st B = u1 holds B is opers_closed by Def7;

        then

         A27: u1 in X by A2, A11, A12;

        hence the carrier of E is Subset of U1 by A10, SETFAM_1: 3;

        let B be non empty Subset of U1;

        assume

         A28: B = the carrier of E;

        reconsider u11 = u1 as non empty Subset of U0 by Def7;



         A29: the charact of U1 = ( Opers (U0,u11)) by Def7;



         A30: ( dom the charact of U0) = ( dom ( Opers (U0,u11))) by Def6;



         A31: u11 is opers_closed by Def7;

         A32:

        now

          let o1 be operation of U1;

          consider n be Nat such that

           A33: n in ( dom the charact of U1) and

           A34: o1 = (the charact of U1 . n) by FINSEQ_2: 10;

          reconsider o0 = (the charact of U0 . n) as operation of U0 by A29, A30, A33, FUNCT_1:def 3;



           A35: ( arity o0) = ( arity o1) by A33, A34, Th6;



           A36: u11 is_closed_on o0 by A31;

          now

            let s be FinSequence of B;



             A37: P is_closed_on o0 by A6;

            reconsider sE = s as Element of (P * ) by A10, A28, FINSEQ_1:def 11;

            s is FinSequence of u11 by FINSEQ_2: 24;

            then

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



             A38: ( dom (o0 | (( arity o0) -tuples_on u11))) = (( dom o0) /\ (( arity o0) -tuples_on u11)) by RELAT_1: 61

            .= ((( arity o0) -tuples_on the carrier of U0) /\ (( arity o0) -tuples_on u11)) by MARGREL1: 22

            .= (( arity o0) -tuples_on u11) by MARGREL1: 21;

            assume

             A39: ( len s) = ( arity o1);

            then s1 in { q where q be Element of (u11 * ) : ( len q) = ( arity o0) } by A35;

            then

             A40: s1 in ( dom (o0 | (( arity o0) -tuples_on u11))) by A38, FINSEQ_2:def 4;

            (o1 . s) = ((o0 /. u11) . s1) by A29, A33, A34, Def6

            .= ((o0 | (( arity o0) -tuples_on u11)) . s1) by A36, Def5

            .= (o0 . sE) by A40, FUNCT_1: 47;

            hence (o1 . s) in B by A10, A28, A35, A39, A37;

          end;

          hence B is_closed_on o1;

        end;



         A41: ( dom ( Opers (U1,B))) = ( dom the charact of U1) by Def6;



         A42: ( dom the charact of U0) = ( dom ( Opers (U0,P))) by Def6;



         A43: P c= u1 by A27, SETFAM_1: 3;

        now

          let n be Nat;

          assume

           A44: n in ( dom the charact of U0);

          then

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

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



           A45: u11 is_closed_on o0 by A31;



           A46: P is_closed_on o0 by A6;



          thus (the charact of E . n) = (o0 /. P) by A10, A42, A44, Def6

          .= (o0 | (( arity o0) -tuples_on P)) by A46, Def5

          .= (o0 | ((( arity o0) -tuples_on u11) /\ (( arity o0) -tuples_on P))) by A43, MARGREL1: 21

          .= ((o0 | (( arity o0) -tuples_on u11)) | (( arity o0) -tuples_on P)) by RELAT_1: 71

          .= ((o0 /. u11) | (( arity o0) -tuples_on P)) by A45, Def5

          .= (o1 | (( arity o0) -tuples_on P)) by A29, A30, A44, Def6

          .= (o1 | (( arity o1) -tuples_on B)) by A10, A28, A29, A30, A44, Th6

          .= (o1 /. B) by A32, Def5

          .= (( Opers (U1,B)) . n) by A29, A30, A41, A44, Def6;

        end;

        hence thesis by A10, A29, A42, A30, A32, A41, FINSEQ_1: 13;

      end;

      uniqueness

      proof

        let W1,W2 be strict SubAlgebra of U0;

        assume A c= the carrier of W1 & (for U1 be SubAlgebra of U0 st A c= the carrier of U1 holds W1 is SubAlgebra of U1) & A c= the carrier of W2 & for U2 be SubAlgebra of U0 st A c= the carrier of U2 holds W2 is SubAlgebra of U2;

        then W1 is strict SubAlgebra of W2 & W2 is strict SubAlgebra of W1;

        hence thesis by Th10;

      end;

    end

    theorem :: UNIALG_2:18

    for U0 be strict Universal_Algebra holds ( GenUnivAlg ( [#] the carrier of U0)) = U0

    proof

      let U0 be strict Universal_Algebra;

      set W = ( GenUnivAlg ( [#] the carrier of U0));

      reconsider B = the carrier of W as non empty Subset of U0 by Def7;

      the carrier of W is Subset of U0 & the carrier of U0 c= the carrier of W by Def7, Def12;

      then

       A1: the carrier of U0 = the carrier of W;



       A2: ( dom the charact of U0) = ( dom ( Opers (U0,B))) by Def6;



       A3: for n be Nat st n in ( dom the charact of U0) holds (the charact of U0 . n) = (( Opers (U0,B)) . n)

      proof

        let n be Nat;

        assume

         A4: n in ( dom the charact of U0);

        then

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

        (( Opers (U0,B)) . n) = (o /. B) by A2, A4, Def6;

        hence thesis by A1, Th4;

      end;

      the charact of W = ( Opers (U0,B)) by Def7;

      hence thesis by A1, A2, A3, FINSEQ_1: 13;

    end;

    theorem :: UNIALG_2:19



     Th19: for U0 be Universal_Algebra, U1 be strict SubAlgebra of U0, B be non empty Subset of U0 st B = the carrier of U1 holds ( GenUnivAlg B) = U1

    proof

      let U0 be Universal_Algebra, U1 be strict SubAlgebra of U0, B be non empty Subset of U0;

      set W = ( GenUnivAlg B);

      assume

       A1: B = the carrier of U1;

      then ( GenUnivAlg B) is SubAlgebra of U1 by Def12;

      then

       A2: the carrier of W is non empty Subset of U1 by Def7;

      the carrier of U1 c= the carrier of W by A1, Def12;

      then the carrier of U1 = the carrier of W by A2;

      hence thesis by Th12;

    end;

    definition

      let U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0;

      :: UNIALG_2:def13

      func U1 "\/" U2 -> strict SubAlgebra of U0 means

      : Def13: for A be non empty Subset of U0 st A = (the carrier of U1 \/ the carrier of U2) holds it = ( GenUnivAlg A);

      existence

      proof

        reconsider B = (the carrier of U1 \/ the carrier of U2) as non empty set;

        the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 by Def7;

        then

        reconsider B as non empty Subset of U0 by XBOOLE_1: 8;

        take ( GenUnivAlg B);

        thus thesis;

      end;

      uniqueness

      proof

        reconsider B = (the carrier of U1 \/ the carrier of U2) as non empty set;

        let W1,W2 be strict SubAlgebra of U0;

        assume that

         A1: for A be non empty Subset of U0 st A = (the carrier of U1 \/ the carrier of U2) holds W1 = ( GenUnivAlg A) and

         A2: for A be non empty Subset of U0 st A = (the carrier of U1 \/ the carrier of U2) holds W2 = ( GenUnivAlg A);

        the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 by Def7;

        then

        reconsider B as non empty Subset of U0 by XBOOLE_1: 8;

        W1 = ( GenUnivAlg B) by A1;

        hence thesis by A2;

      end;

    end

    theorem :: UNIALG_2:20



     Th20: for U0 be Universal_Algebra, U1 be SubAlgebra of U0, A,B be Subset of U0 st (A <> {} or ( Constants U0) <> {} ) & B = (A \/ the carrier of U1) holds (( GenUnivAlg A) "\/" U1) = ( GenUnivAlg B)

    proof

      let U0 be Universal_Algebra, U1 be SubAlgebra of U0, A,B be Subset of U0;

      reconsider u1 = the carrier of U1, a = the carrier of ( GenUnivAlg A) as non empty Subset of U0 by Def7;

      assume that

       A1: A <> {} or ( Constants U0) <> {} and

       A2: B = (A \/ the carrier of U1);



       A3: A c= the carrier of ( GenUnivAlg A) by Def12;



       A4: B c= the carrier of ( GenUnivAlg B) by Def12;

      A c= B by A2, XBOOLE_1: 7;

      then

       A5: A c= the carrier of ( GenUnivAlg B) by A4;

      now

        per cases by A1;

          case A <> {} ;

          hence (the carrier of ( GenUnivAlg A) /\ the carrier of ( GenUnivAlg B)) <> {} by A3, A5, XBOOLE_1: 3, XBOOLE_1: 19;

        end;

          case

           A6: ( Constants U0) <> {} ;

          ( Constants U0) is Subset of ( GenUnivAlg A) & ( Constants U0) is Subset of ( GenUnivAlg B) by Th15;

          hence (the carrier of ( GenUnivAlg A) /\ the carrier of ( GenUnivAlg B)) <> {} by A6, XBOOLE_1: 3, XBOOLE_1: 19;

        end;

      end;

      then the carrier of ( GenUnivAlg A) meets the carrier of ( GenUnivAlg B);

      then

       A7: the carrier of (( GenUnivAlg A) /\ ( GenUnivAlg B)) = (the carrier of ( GenUnivAlg A) /\ the carrier of ( GenUnivAlg B)) by Def9;

      reconsider b = (a \/ u1) as non empty Subset of U0;



       A8: (the carrier of ( GenUnivAlg A) /\ the carrier of ( GenUnivAlg B)) c= a by XBOOLE_1: 17;

      A c= (the carrier of ( GenUnivAlg A) /\ the carrier of ( GenUnivAlg B)) by A3, A5, XBOOLE_1: 19;

      then ( GenUnivAlg A) is SubAlgebra of (( GenUnivAlg A) /\ ( GenUnivAlg B)) by A1, A7, Def12;

      then a is non empty Subset of (( GenUnivAlg A) /\ ( GenUnivAlg B)) by Def7;

      then a = (the carrier of ( GenUnivAlg A) /\ the carrier of ( GenUnivAlg B)) by A7, A8;

      then

       A9: a c= the carrier of ( GenUnivAlg B) by XBOOLE_1: 17;

      u1 c= B by A2, XBOOLE_1: 7;

      then u1 c= the carrier of ( GenUnivAlg B) by A4;

      then b c= the carrier of ( GenUnivAlg B) by A9, XBOOLE_1: 8;

      then

       A10: ( GenUnivAlg b) is strict SubAlgebra of ( GenUnivAlg B) by Def12;



       A11: (( GenUnivAlg A) "\/" U1) = ( GenUnivAlg b) by Def13;

      then

       A12: (a \/ u1) c= the carrier of (( GenUnivAlg A) "\/" U1) by Def12;

      (A \/ u1) c= (a \/ u1) by A3, XBOOLE_1: 13;

      then B c= the carrier of (( GenUnivAlg A) "\/" U1) by A2, A12;

      then ( GenUnivAlg B) is strict SubAlgebra of (( GenUnivAlg A) "\/" U1) by A2, Def12;

      hence thesis by A11, A10, Th10;

    end;

    theorem :: UNIALG_2:21



     Th21: for U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0 holds (U1 "\/" U2) = (U2 "\/" U1)

    proof

      let U0 be Universal_Algebra, U1,U2 be SubAlgebra of U0;

      reconsider u1 = the carrier of U1, u2 = the carrier of U2 as non empty Subset of U0 by Def7;

      reconsider A = (u1 \/ u2) as non empty Subset of U0;

      (U1 "\/" U2) = ( GenUnivAlg A) by Def13;

      hence thesis by Def13;

    end;

    theorem :: UNIALG_2:22



     Th22: for U0 be with_const_op Universal_Algebra, U1,U2 be strict SubAlgebra of U0 holds (U1 /\ (U1 "\/" U2)) = U1

    proof

      let U0 be with_const_op Universal_Algebra, U1,U2 be strict SubAlgebra of U0;

      reconsider u112 = the carrier of (U1 /\ (U1 "\/" U2)) as non empty Subset of U0 by Def7;

      reconsider u1 = the carrier of U1, u2 = the carrier of U2 as non empty Subset of U0 by Def7;

      reconsider A = (u1 \/ u2) as non empty Subset of U0;



       A1: the charact of U1 = ( Opers (U0,u1)) by Def7;



       A2: ( dom ( Opers (U0,u1))) = ( dom the charact of U0) by Def6;

      (U1 "\/" U2) = ( GenUnivAlg A) by Def13;

      then

       A3: A c= the carrier of (U1 "\/" U2) by Def12;



       A4: the carrier of U1 meets the carrier of (U1 "\/" U2) by Th17;

      then

       A5: the carrier of (U1 /\ (U1 "\/" U2)) = (the carrier of U1 /\ the carrier of (U1 "\/" U2)) by Def9;

      then

       A6: the carrier of (U1 /\ (U1 "\/" U2)) c= the carrier of U1 by XBOOLE_1: 17;

      the carrier of U1 c= A by XBOOLE_1: 7;

      then the carrier of U1 c= the carrier of (U1 "\/" U2) by A3;

      then

       A7: the carrier of U1 c= the carrier of (U1 /\ (U1 "\/" U2)) by A5, XBOOLE_1: 19;



       A8: ( dom ( Opers (U0,u112))) = ( dom the charact of U0) by Def6;



       A9: for n be Nat st n in ( dom the charact of U0) holds (the charact of (U1 /\ (U1 "\/" U2)) . n) = (the charact of U1 . n)

      proof

        let n be Nat;

        assume

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

        then

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



        thus (the charact of (U1 /\ (U1 "\/" U2)) . n) = (( Opers (U0,u112)) . n) by A4, Def9

        .= (o0 /. u112) by A8, A10, Def6

        .= (o0 /. u1) by A7, A6, XBOOLE_0:def 10

        .= (( Opers (U0,u1)) . n) by A2, A10, Def6

        .= (the charact of U1 . n) by Def7;

      end;

      the charact of (U1 /\ (U1 "\/" U2)) = ( Opers (U0,u112)) by A4, Def9;

      then the charact of (U1 /\ (U1 "\/" U2)) = the charact of U1 by A1, A8, A2, A9, FINSEQ_1: 13;

      hence thesis by A7, A6, XBOOLE_0:def 10;

    end;

    theorem :: UNIALG_2:23



     Th23: for U0 be with_const_op Universal_Algebra, U1,U2 be strict SubAlgebra of U0 holds ((U1 /\ U2) "\/" U2) = U2

    proof

      let U0 be with_const_op Universal_Algebra, U1,U2 be strict SubAlgebra of U0;

      reconsider u12 = the carrier of (U1 /\ U2), u2 = the carrier of U2 as non empty Subset of U0 by Def7;

      reconsider A = (u12 \/ u2) as non empty Subset of U0;

      the carrier of U1 meets the carrier of U2 by Th17;

      then u12 = (the carrier of U1 /\ the carrier of U2) by Def9;

      then

       A1: u12 c= u2 by XBOOLE_1: 17;

      ((U1 /\ U2) "\/" U2) = ( GenUnivAlg A) by Def13;

      hence thesis by A1, Th19, XBOOLE_1: 12;

    end;

    definition

      let U0 be Universal_Algebra;

      :: UNIALG_2:def14

      func Sub (U0) -> set means

      : Def14: for x be object holds x in it iff x is strict SubAlgebra of U0;

      existence

      proof

        reconsider X = { ( GenUnivAlg A) where A be Subset of U0 : A is non empty } as set;

        take X;

        let x be object;

        thus x in X implies x is strict SubAlgebra of U0

        proof

          assume x in X;

          then ex A be Subset of U0 st x = ( GenUnivAlg A) & A is non empty;

          hence thesis;

        end;

        assume x is strict SubAlgebra of U0;

        then

        reconsider a = x as strict SubAlgebra of U0;

        reconsider A = the carrier of a as non empty Subset of U0 by Def7;

        a = ( GenUnivAlg A) by Th19;

        hence thesis;

      end;

      uniqueness

      proof

        let A,B be set;

        assume that

         A1: for x be object holds x in A iff x is strict SubAlgebra of U0 and

         A2: for y be object holds y in B iff y is strict SubAlgebra of U0;

        now

          let x be object;

          assume x in A;

          then x is strict SubAlgebra of U0 by A1;

          hence x in B by A2;

        end;

        hence A c= B;

        let y be object;

        assume y in B;

        then y is strict SubAlgebra of U0 by A2;

        hence thesis by A1;

      end;

    end

    registration

      let U0 be Universal_Algebra;

      cluster ( Sub U0) -> non empty;

      coherence

      proof

        set x = the strict SubAlgebra of U0;

        x in ( Sub U0) by Def14;

        hence thesis;

      end;

    end

    definition

      let U0 be Universal_Algebra;

      :: UNIALG_2:def15

      func UniAlg_join (U0) -> BinOp of ( Sub U0) means

      : Def15: for x,y be Element of ( Sub U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds (it . (x,y)) = (U1 "\/" U2);

      existence

      proof

        defpred P[ Element of ( Sub U0), Element of ( Sub U0), Element of ( Sub U0)] means for U1,U2 be strict SubAlgebra of U0 st $1 = U1 & $2 = U2 holds $3 = (U1 "\/" U2);



         A1: for x,y be Element of ( Sub U0) holds ex z be Element of ( Sub U0) st P[x, y, z]

        proof

          let x,y be Element of ( Sub U0);

          reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

          reconsider z = (U1 "\/" U2) as Element of ( Sub U0) by Def14;

          take z;

          thus thesis;

        end;

        consider o be BinOp of ( Sub U0) such that

         A2: for a,b be Element of ( Sub U0) holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A1);

        take o;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( Sub U0);

        assume that

         A3: for x,y be Element of ( Sub U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds (o1 . (x,y)) = (U1 "\/" U2) and

         A4: for x,y be Element of ( Sub U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds (o2 . (x,y)) = (U1 "\/" U2);

        for x be Element of ( Sub U0) holds for y be Element of ( Sub U0) holds (o1 . (x,y)) = (o2 . (x,y))

        proof

          let x,y be Element of ( Sub U0);

          reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

          (o1 . (x,y)) = (U1 "\/" U2) by A3;

          hence thesis by A4;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let U0 be Universal_Algebra;

      :: UNIALG_2:def16

      func UniAlg_meet (U0) -> BinOp of ( Sub U0) means

      : Def16: for x,y be Element of ( Sub U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds (it . (x,y)) = (U1 /\ U2);

      existence

      proof

        defpred P[ Element of ( Sub U0), Element of ( Sub U0), Element of ( Sub U0)] means for U1,U2 be strict SubAlgebra of U0 st $1 = U1 & $2 = U2 holds $3 = (U1 /\ U2);



         A1: for x,y be Element of ( Sub U0) holds ex z be Element of ( Sub U0) st P[x, y, z]

        proof

          let x,y be Element of ( Sub U0);

          reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

          reconsider z = (U1 /\ U2) as Element of ( Sub U0) by Def14;

          take z;

          thus thesis;

        end;

        consider o be BinOp of ( Sub U0) such that

         A2: for a,b be Element of ( Sub U0) holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A1);

        take o;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( Sub U0);

        assume that

         A3: for x,y be Element of ( Sub U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds (o1 . (x,y)) = (U1 /\ U2) and

         A4: for x,y be Element of ( Sub U0) holds for U1,U2 be strict SubAlgebra of U0 st x = U1 & y = U2 holds (o2 . (x,y)) = (U1 /\ U2);

        for x be Element of ( Sub U0) holds for y be Element of ( Sub U0) holds (o1 . (x,y)) = (o2 . (x,y))

        proof

          let x,y be Element of ( Sub U0);

          reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

          (o1 . (x,y)) = (U1 /\ U2) by A3;

          hence thesis by A4;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: UNIALG_2:24



     Th24: ( UniAlg_join U0) is commutative

    proof

      set o = ( UniAlg_join U0);

      for x,y be Element of ( Sub U0) holds (o . (x,y)) = (o . (y,x))

      proof

        let x,y be Element of ( Sub U0);

        reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

        reconsider B = (the carrier of U1 \/ the carrier of U2) as non empty set;

        the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 by Def7;

        then

        reconsider B as non empty Subset of U0 by XBOOLE_1: 8;



         A1: (U1 "\/" U2) = ( GenUnivAlg B) by Def13;

        (o . (x,y)) = (U1 "\/" U2) & (o . (y,x)) = (U2 "\/" U1) by Def15;

        hence thesis by A1, Def13;

      end;

      hence thesis by BINOP_1:def 2;

    end;

    theorem :: UNIALG_2:25



     Th25: ( UniAlg_join U0) is associative

    proof

      set o = ( UniAlg_join U0);

      for x,y,z be Element of ( Sub U0) holds (o . (x,(o . (y,z)))) = (o . ((o . (x,y)),z))

      proof

        let x,y,z be Element of ( Sub U0);

        reconsider U1 = x, U2 = y, U3 = z as strict SubAlgebra of U0 by Def14;

        reconsider B = (the carrier of U1 \/ (the carrier of U2 \/ the carrier of U3)) as non empty set;



         A1: (o . (x,y)) = (U1 "\/" U2) by Def15;



         A2: the carrier of U2 is Subset of U0 by Def7;



         A3: the carrier of U3 is Subset of U0 by Def7;

        then

        reconsider C = (the carrier of U2 \/ the carrier of U3) as non empty Subset of U0 by A2, XBOOLE_1: 8;



         A4: the carrier of U1 is Subset of U0 by Def7;

        then

        reconsider D = (the carrier of U1 \/ the carrier of U2) as non empty Subset of U0 by A2, XBOOLE_1: 8;

        (the carrier of U2 \/ the carrier of U3) c= the carrier of U0 by A2, A3, XBOOLE_1: 8;

        then

        reconsider B as non empty Subset of U0 by A4, XBOOLE_1: 8;



         A5: B = (D \/ the carrier of U3) by XBOOLE_1: 4;



         A6: ((U1 "\/" U2) "\/" U3) = (( GenUnivAlg D) "\/" U3) by Def13

        .= ( GenUnivAlg B) by A5, Th20;

        (o . (y,z)) = (U2 "\/" U3) by Def15;

        then

         A7: (o . (x,(o . (y,z)))) = (U1 "\/" (U2 "\/" U3)) by Def15;

        (U1 "\/" (U2 "\/" U3)) = (U1 "\/" ( GenUnivAlg C)) by Def13

        .= (( GenUnivAlg C) "\/" U1) by Th21

        .= ( GenUnivAlg B) by Th20;

        hence thesis by A1, A7, A6, Def15;

      end;

      hence thesis by BINOP_1:def 3;

    end;

    theorem :: UNIALG_2:26



     Th26: for U0 be with_const_op Universal_Algebra holds ( UniAlg_meet U0) is commutative

    proof

      let U0 be with_const_op Universal_Algebra;

      set o = ( UniAlg_meet U0);

      for x,y be Element of ( Sub U0) holds (o . (x,y)) = (o . (y,x))

      proof

        let x,y be Element of ( Sub U0);

        reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;



         A1: (o . (x,y)) = (U1 /\ U2) & (o . (y,x)) = (U2 /\ U1) by Def16;



         A2: the carrier of U1 meets the carrier of U2 by Th17;

        then the carrier of (U2 /\ U1) = (the carrier of U2 /\ the carrier of U1) & for B2 be non empty Subset of U0 st B2 = the carrier of (U2 /\ U1) holds the charact of (U2 /\ U1) = ( Opers (U0,B2)) & B2 is opers_closed by Def9;

        hence thesis by A1, A2, Def9;

      end;

      hence thesis by BINOP_1:def 2;

    end;

    theorem :: UNIALG_2:27



     Th27: for U0 be with_const_op Universal_Algebra holds ( UniAlg_meet U0) is associative

    proof

      let U0 be with_const_op Universal_Algebra;

      set o = ( UniAlg_meet U0);

      for x,y,z be Element of ( Sub U0) holds (o . (x,(o . (y,z)))) = (o . ((o . (x,y)),z))

      proof

        let x,y,z be Element of ( Sub U0);

        reconsider U1 = x, U2 = y, U3 = z as strict SubAlgebra of U0 by Def14;

        reconsider u23 = (U2 /\ U3), u12 = (U1 /\ U2) as Element of ( Sub U0) by Def14;



         A1: (o . (x,(o . (y,z)))) = (o . (x,u23)) by Def16

        .= (U1 /\ (U2 /\ U3)) by Def16;



         A2: (o . ((o . (x,y)),z)) = (o . (u12,z)) by Def16

        .= ((U1 /\ U2) /\ U3) by Def16;

        the carrier of U2 meets the carrier of U3 by Th17;

        then

         A3: the carrier of (U2 /\ U3) = (the carrier of U2 /\ the carrier of U3) by Def9;

        then

         A4: the carrier of U1 meets (the carrier of U2 /\ the carrier of U3) by Th17;

        then

         A5: for B be non empty Subset of U0 st B = the carrier of (U1 /\ (U2 /\ U3)) holds the charact of (U1 /\ (U2 /\ U3)) = ( Opers (U0,B)) & B is opers_closed by A3, Def9;



         A6: the carrier of (U1 /\ (U2 /\ U3)) = (the carrier of U1 /\ (the carrier of U2 /\ the carrier of U3)) by A3, A4, Def9;

        then

        reconsider C = (the carrier of U1 /\ (the carrier of U2 /\ the carrier of U3)) as non empty Subset of U0 by Def7;



         A7: C = ((the carrier of U1 /\ the carrier of U2) /\ the carrier of U3) by XBOOLE_1: 16;

        the carrier of U1 meets the carrier of U2 by Th17;

        then

         A8: the carrier of (U1 /\ U2) = (the carrier of U1 /\ the carrier of U2) by Def9;

        then (the carrier of U1 /\ the carrier of U2) meets the carrier of U3 by Th17;

        hence thesis by A1, A2, A8, A6, A5, A7, Def9;

      end;

      hence thesis by BINOP_1:def 3;

    end;

    definition

      let U0 be with_const_op Universal_Algebra;

      :: UNIALG_2:def17

      func UnSubAlLattice (U0) -> strict Lattice equals LattStr (# ( Sub U0), ( UniAlg_join U0), ( UniAlg_meet U0) #);

      coherence

      proof

        set L = LattStr (# ( Sub U0), ( UniAlg_join U0), ( UniAlg_meet U0) #);



         A1: for a,b,c be Element of L holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c)

        proof

          let a,b,c be Element of L;

          reconsider x = a, y = b, z = c as Element of ( Sub U0);



           A2: ( UniAlg_join U0) is associative by Th25;



          thus (a "\/" (b "\/" c)) = (the L_join of L . (a,(b "\/" c))) by LATTICES:def 1

          .= (( UniAlg_join U0) . (x,(( UniAlg_join U0) . (y,z)))) by LATTICES:def 1

          .= (the L_join of L . ((the L_join of L . (a,b)),c)) by A2, BINOP_1:def 3

          .= ((the L_join of L . (a,b)) "\/" c) by LATTICES:def 1

          .= ((a "\/" b) "\/" c) by LATTICES:def 1;

        end;



         A3: for a,b be Element of L holds (a "/\" b) = (b "/\" a)

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of ( Sub U0);



           A4: ( UniAlg_meet U0) is commutative by Th26;



          thus (a "/\" b) = (( UniAlg_meet U0) . (x,y)) by LATTICES:def 2

          .= (the L_meet of L . (b,a)) by A4, BINOP_1:def 2

          .= (b "/\" a) by LATTICES:def 2;

        end;



         A5: for a,b be Element of L holds (a "/\" (a "\/" b)) = a

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of ( Sub U0);



           A6: (( UniAlg_meet U0) . (x,(( UniAlg_join U0) . (x,y)))) = x

          proof

            reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

            (( UniAlg_join U0) . (x,y)) = (U1 "\/" U2) by Def15;



            hence (( UniAlg_meet U0) . (x,(( UniAlg_join U0) . (x,y)))) = (U1 /\ (U1 "\/" U2)) by Def16

            .= x by Th22;

          end;



          thus (a "/\" (a "\/" b)) = (the L_meet of L . (a,(a "\/" b))) by LATTICES:def 2

          .= a by A6, LATTICES:def 1;

        end;



         A7: for a,b be Element of L holds ((a "/\" b) "\/" b) = b

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of ( Sub U0);



           A8: (( UniAlg_join U0) . ((( UniAlg_meet U0) . (x,y)),y)) = y

          proof

            reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

            (( UniAlg_meet U0) . (x,y)) = (U1 /\ U2) by Def16;



            hence (( UniAlg_join U0) . ((( UniAlg_meet U0) . (x,y)),y)) = ((U1 /\ U2) "\/" U2) by Def15

            .= y by Th23;

          end;



          thus ((a "/\" b) "\/" b) = (the L_join of L . ((a "/\" b),b)) by LATTICES:def 1

          .= b by A8, LATTICES:def 2;

        end;



         A9: for a,b,c be Element of L holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)

        proof

          let a,b,c be Element of L;

          reconsider x = a, y = b, z = c as Element of ( Sub U0);



           A10: ( UniAlg_meet U0) is associative by Th27;



          thus (a "/\" (b "/\" c)) = (the L_meet of L . (a,(b "/\" c))) by LATTICES:def 2

          .= (( UniAlg_meet U0) . (x,(( UniAlg_meet U0) . (y,z)))) by LATTICES:def 2

          .= (the L_meet of L . ((the L_meet of L . (a,b)),c)) by A10, BINOP_1:def 3

          .= ((the L_meet of L . (a,b)) "/\" c) by LATTICES:def 2

          .= ((a "/\" b) "/\" c) by LATTICES:def 2;

        end;

        for a,b be Element of L holds (a "\/" b) = (b "\/" a)

        proof

          let a,b be Element of L;

          reconsider x = a, y = b as Element of ( Sub U0);



           A11: ( UniAlg_join U0) is commutative by Th24;



          thus (a "\/" b) = (( UniAlg_join U0) . (x,y)) by LATTICES:def 1

          .= (the L_join of L . (b,a)) by A11, BINOP_1:def 2

          .= (b "\/" a) by LATTICES:def 1;

        end;

        then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1, A7, A3, A9, A5, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;

        hence thesis;

      end;

    end