mod_2.miz



    begin

    reserve D,D9 for non empty set;

    reserve R for Ring;

    reserve G,H,S for non empty ModuleStr over R;

    reserve UN for Universe;

    

     Lm1: ModuleStr (# { 0 }, op2 , op0 , ( pr2 (the carrier of R, { 0 })) #) is strict LeftMod of R

    proof

      set a = ( 0. Trivial-addLoopStr );

      set G = ModuleStr (# { 0 }, op2 , op0 , ( pr2 (the carrier of R, { 0 })) #);

      

       A1: for a,b be Element of G holds for x,y be Element of Trivial-addLoopStr st x = a & b = y holds (a + b) = (x + y);

      

       A2: G is Abelian add-associative right_zeroed right_complementable

      proof

        thus G is Abelian

        proof

          let a,b be Element of G;

          reconsider x = a, y = b as Element of Trivial-addLoopStr ;

          

          thus (a + b) = (y + x) by A1

          .= (b + a);

        end;

        hereby

          let a,b,c be Element of G;

          reconsider x = a, y = b, z = c as Element of Trivial-addLoopStr ;

          

          thus ((a + b) + c) = ((x + y) + z)

          .= (x + (y + z)) by RLVECT_1:def 3

          .= (a + (b + c));

        end;

        hereby

          let a be Element of G;

          reconsider x = a as Element of Trivial-addLoopStr ;

          

          thus (a + ( 0. G)) = (x + ( 0. Trivial-addLoopStr ))

          .= a by RLVECT_1: 4;

        end;

        let a be Element of G;

        reconsider x = a as Element of Trivial-addLoopStr ;

        consider b be Element of Trivial-addLoopStr such that

         A3: (x + b) = ( 0. Trivial-addLoopStr ) by ALGSTR_0:def 11;

        reconsider b9 = b as Element of G;

        take b9;

        thus thesis by A3;

      end;

      now

        let x,y be Scalar of R, v,w be Vector of G;

        

         A4: ((x * y) * v) = a & (( 1. R) * v) = a by GRCAT_1: 4;

        (x * (v + w)) = a & ((x + y) * v) = a by GRCAT_1: 4;

        hence (x * (v + w)) = ((x * v) + (x * w)) & ((x + y) * v) = ((x * v) + (y * v)) & ((x * y) * v) = (x * (y * v)) & (( 1. R) * v) = v by A4, GRCAT_1: 4;

      end;

      hence thesis by A2, VECTSP_1:def 14, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17;

    end;

    definition

      let R;

      :: MOD_2:def1

      func TrivialLMod (R) -> strict LeftMod of R equals ModuleStr (# { 0 }, op2 , op0 , ( pr2 (the carrier of R, { 0 })) #);

      coherence by Lm1;

    end

    theorem :: MOD_2:1

    for x be Vector of ( TrivialLMod R) holds x = ( 0. ( TrivialLMod R)) by GRCAT_1: 4;

    definition

      let R be non empty multMagma;

      let G,H be non empty ModuleStr over R;

      let f be Function of G, H;

      :: MOD_2:def2

      attr f is homogeneous means for a be Scalar of R, x be Vector of G holds (f . (a * x)) = (a * (f . x));

    end

    theorem :: MOD_2:2

    

     Th2: for f be Function of G, H, g be Function of H, S st f is homogeneous & g is homogeneous holds (g * f) is homogeneous

    proof

      let f be Function of G, H, g be Function of H, S;

      assume that

       A1: f is homogeneous and

       A2: g is homogeneous;

      set h = (g * f);

      let a be Scalar of R, x be Vector of G;

      

      thus (h . (a * x)) = (g . (f . (a * x))) by FUNCT_2: 15

      .= (g . (a * (f . x))) by A1

      .= (a * (g . (f . x))) by A2

      .= (a * (h . x)) by FUNCT_2: 15;

    end;

    reserve R for Ring;

    reserve G,H for LeftMod of R;

    registration

      let R, G, H;

      cluster ( ZeroMap (G,H)) -> homogeneous;

      coherence

      proof

        let a be Scalar of R, x be Vector of G;

        set f = ( ZeroMap (G,H));

        (f . (a * x)) = ( 0. H) & (f . x) = ( 0. H) by FUNCOP_1: 7;

        hence thesis by VECTSP_1: 14;

      end;

    end

    reserve G1,G2,G3 for LeftMod of R;

    definition

      let R;

      struct LModMorphismStr over R (# the Dom, Cod -> LeftMod of R,

the Fun -> Function of the Dom, the Cod #)

       attr strict strict;

    end

    reserve f for LModMorphismStr over R;

    definition

      let R, f;

      :: MOD_2:def3

      func dom (f) -> LeftMod of R equals the Dom of f;

      correctness ;

      :: MOD_2:def4

      func cod (f) -> LeftMod of R equals the Cod of f;

      correctness ;

    end

    definition

      let R, f;

      :: MOD_2:def5

      func fun (f) -> Function of ( dom f), ( cod f) equals the Fun of f;

      coherence ;

    end

    theorem :: MOD_2:3

    for f0 be Function of G1, G2 st f = LModMorphismStr (# G1, G2, f0 #) holds ( dom f) = G1 & ( cod f) = G2 & ( fun f) = f0;

    definition

      let R, G, H;

      :: MOD_2:def6

      func ZERO (G,H) -> strict LModMorphismStr over R equals LModMorphismStr (# G, H, ( ZeroMap (G,H)) #);

      correctness ;

    end

    definition

      let R;

      let IT be LModMorphismStr over R;

      :: MOD_2:def7

      attr IT is LModMorphism-like means

      : Def7: ( fun IT) is additive homogeneous;

    end

    registration

      let R;

      cluster strict LModMorphism-like for LModMorphismStr over R;

      existence

      proof

        set G = the LeftMod of R;

        set z = ( ZERO (G,G));

        z is LModMorphism-like;

        hence thesis;

      end;

    end

    definition

      let R;

      mode LModMorphism of R is LModMorphism-like LModMorphismStr over R;

    end

    theorem :: MOD_2:4

    

     Th4: for F be LModMorphism of R holds the Fun of F is additive homogeneous

    proof

      let F be LModMorphism of R;

      the Fun of F = ( fun F);

      hence thesis by Def7;

    end;

    registration

      let R, G, H;

      cluster ( ZERO (G,H)) -> LModMorphism-like;

      coherence ;

    end

    definition

      let R, G, H;

      :: MOD_2:def8

      mode Morphism of G,H -> LModMorphism of R means

      : Def8: ( dom it ) = G & ( cod it ) = H;

      existence

      proof

        take ( ZERO (G,H));

        thus thesis;

      end;

    end

    registration

      let R, G, H;

      cluster strict for Morphism of G, H;

      existence

      proof

        ( dom ( ZERO (G,H))) = G & ( cod ( ZERO (G,H))) = H;

        then

        reconsider z = ( ZERO (G,H)) as Morphism of G, H by Def8;

        take z;

        thus thesis;

      end;

    end

    theorem :: MOD_2:5

    

     Th5: for f be LModMorphismStr over R holds ( dom f) = G & ( cod f) = H & ( fun f) is additive homogeneous implies f is Morphism of G, H

    proof

      let f be LModMorphismStr over R;

      assume that

       A1: ( dom f) = G & ( cod f) = H and

       A2: ( fun f) is additive homogeneous;

      reconsider f9 = f as LModMorphism of R by A2, Def7;

      f9 is Morphism of G, H by A1, Def8;

      hence thesis;

    end;

    theorem :: MOD_2:6

    

     Th6: for f be Function of G, H st f is additive homogeneous holds LModMorphismStr (# G, H, f #) is strict Morphism of G, H

    proof

      let f be Function of G, H such that

       A1: f is additive homogeneous;

      set F = LModMorphismStr (# G, H, f #);

      ( fun F) = f;

      hence thesis by A1, Th5;

    end;

    registration

      let R, G;

      cluster ( id G) -> homogeneous;

      coherence

      proof

        set f = ( id G);

        let a be Scalar of R, x be Vector of G;

        

        thus (f . (a * x)) = (a * x) by FUNCT_1: 18

        .= (a * (f . x)) by FUNCT_1: 18;

      end;

    end

    definition

      let R, G;

      :: MOD_2:def9

      func ID G -> strict Morphism of G, G equals LModMorphismStr (# G, G, ( id G) #);

      coherence

      proof

        set i = LModMorphismStr (# G, G, ( id G) #);

        ( fun i) = ( id G);

        hence thesis by Th5;

      end;

    end

    definition

      let R, G, H;

      :: original: ZERO

      redefine

      func ZERO (G,H) -> strict Morphism of G, H ;

      coherence

      proof

        set i = ( ZERO (G,H));

        ( fun i) = ( ZeroMap (G,H));

        hence thesis by Th5;

      end;

    end

    theorem :: MOD_2:7

    

     Th7: for F be Morphism of G, H holds ex f be Function of G, H st the LModMorphismStr of F = LModMorphismStr (# G, H, f #) & f is additive homogeneous

    proof

      let F be Morphism of G, H;

      

       A1: the Cod of F = ( cod F)

      .= H by Def8;

      

       A2: the Dom of F = ( dom F)

      .= G by Def8;

      then

      reconsider f = the Fun of F as Function of G, H by A1;

      take f;

      thus thesis by A2, A1, Th4;

    end;

    theorem :: MOD_2:8

    

     Th8: for F be strict Morphism of G, H holds ex f be Function of G, H st F = LModMorphismStr (# G, H, f #)

    proof

      let F be strict Morphism of G, H;

      consider f be Function of G, H such that

       A1: the LModMorphismStr of F = LModMorphismStr (# G, H, f #) and f is additive homogeneous by Th7;

      take f;

      thus thesis by A1;

    end;

    theorem :: MOD_2:9

    

     Th9: for F be LModMorphism of R holds ex G, H st F is Morphism of G, H

    proof

      let F be LModMorphism of R;

      take G = the Dom of F, H = the Cod of F;

      ( dom F) = G & ( cod F) = H;

      hence thesis by Def8;

    end;

    theorem :: MOD_2:10

    for F be strict LModMorphism of R holds ex G,H be LeftMod of R, f be Function of G, H st F is strict Morphism of G, H & F = LModMorphismStr (# G, H, f #) & f is additive homogeneous

    proof

      let F be strict LModMorphism of R;

      consider G, H such that

       A1: F is Morphism of G, H by Th9;

      reconsider F9 = F as Morphism of G, H by A1;

      consider f be Function of G, H such that

       A2: the LModMorphismStr of F9 = LModMorphismStr (# G, H, f #) & f is additive homogeneous by Th7;

      take G, H, f;

      thus thesis by A2;

    end;

    theorem :: MOD_2:11

    

     Th11: for g,f be LModMorphism of R st ( dom g) = ( cod f) holds ex G1, G2, G3 st g is Morphism of G2, G3 & f is Morphism of G1, G2

    proof

      defpred P[ LModMorphism of R, LModMorphism of R] means ( dom $1) = ( cod $2);

      let g,f be LModMorphism of R such that

       A1: P[g, f];

      consider G2, G3 such that

       A2: g is Morphism of G2, G3 by Th9;

      

       A3: G2 = ( dom g) by A2, Def8;

      consider G1,G2 be LeftMod of R such that

       A4: f is Morphism of G1, G2 by Th9;

      G2 = ( cod f) by A4, Def8;

      hence thesis by A1, A2, A3, A4;

    end;

    definition

      let R;

      let G,F be LModMorphism of R;

      assume

       A1: ( dom G) = ( cod F);

      :: MOD_2:def10

      func G * F -> strict LModMorphism of R means

      : Def10: for G1,G2,G3 be LeftMod of R, g be Function of G2, G3, f be Function of G1, G2 st the LModMorphismStr of G = LModMorphismStr (# G2, G3, g #) & the LModMorphismStr of F = LModMorphismStr (# G1, G2, f #) holds it = LModMorphismStr (# G1, G3, (g * f) #);

      existence

      proof

        consider G19,G2,G39 be LeftMod of R such that

         A2: G is Morphism of G2, G39 and

         A3: F is Morphism of G19, G2 by A1, Th11;

        consider f9 be Function of G19, G2 such that

         A4: the LModMorphismStr of F = LModMorphismStr (# G19, G2, f9 #) and

         A5: f9 is additive homogeneous by A3, Th7;

        consider g9 be Function of G2, G39 such that

         A6: the LModMorphismStr of G = LModMorphismStr (# G2, G39, g9 #) and

         A7: g9 is additive homogeneous by A2, Th7;

        (g9 * f9) is additive homogeneous by A7, A5, Th2;

        then

        reconsider T9 = LModMorphismStr (# G19, G39, (g9 * f9) #) as strict LModMorphism of R by Th6;

        take T9;

        thus thesis by A6, A4;

      end;

      uniqueness

      proof

        consider G19,G29 be LeftMod of R such that

         A8: F is Morphism of G19, G29 by Th9;

        reconsider F9 = F as Morphism of G19, G29 by A8;

        consider G2,G39 be LeftMod of R such that

         A9: G is Morphism of G2, G39 by Th9;

        G2 = ( dom G) by A9, Def8;

        then

        reconsider F9 as Morphism of G19, G2 by A1, Def8;

        consider f9 be Function of G19, G2 such that

         A10: the LModMorphismStr of F9 = LModMorphismStr (# G19, G2, f9 #) and f9 is additive homogeneous by Th7;

        reconsider G9 = G as Morphism of G2, G39 by A9;

        let S1,S2 be strict LModMorphism of R such that

         A11: for G1,G2,G3 be LeftMod of R, g be Function of G2, G3, f be Function of G1, G2 st the LModMorphismStr of G = LModMorphismStr (# G2, G3, g #) & the LModMorphismStr of F = LModMorphismStr (# G1, G2, f #) holds S1 = LModMorphismStr (# G1, G3, (g * f) #) and

         A12: for G1,G2,G3 be LeftMod of R, g be Function of G2, G3, f be Function of G1, G2 st the LModMorphismStr of G = LModMorphismStr (# G2, G3, g #) & the LModMorphismStr of F = LModMorphismStr (# G1, G2, f #) holds S2 = LModMorphismStr (# G1, G3, (g * f) #);

        consider g9 be Function of G2, G39 such that

         A13: the LModMorphismStr of G9 = LModMorphismStr (# G2, G39, g9 #) and g9 is additive homogeneous by Th7;

        

        thus S1 = LModMorphismStr (# G19, G39, (g9 * f9) #) by A11, A13, A10

        .= S2 by A12, A13, A10;

      end;

    end

    theorem :: MOD_2:12

    

     Th12: for G be Morphism of G2, G3, F be Morphism of G1, G2 holds (G * F) is strict Morphism of G1, G3

    proof

      let G be Morphism of G2, G3, F be Morphism of G1, G2;

      consider g be Function of G2, G3 such that

       A1: the LModMorphismStr of G = LModMorphismStr (# G2, G3, g #) and g is additive homogeneous by Th7;

      consider f be Function of G1, G2 such that

       A2: the LModMorphismStr of F = LModMorphismStr (# G1, G2, f #) and f is additive homogeneous by Th7;

      ( dom G) = G2 by Def8

      .= ( cod F) by Def8;

      then (G * F) = LModMorphismStr (# G1, G3, (g * f) #) by A1, A2, Def10;

      then ( dom (G * F)) = G1 & ( cod (G * F)) = G3;

      hence thesis by Def8;

    end;

    definition

      let R, G1, G2, G3;

      let G be Morphism of G2, G3;

      let F be Morphism of G1, G2;

      :: MOD_2:def11

      func G *' F -> strict Morphism of G1, G3 equals (G * F);

      coherence by Th12;

    end

    theorem :: MOD_2:13

    

     Th13: for G be Morphism of G2, G3, F be Morphism of G1, G2, g be Function of G2, G3, f be Function of G1, G2 st G = LModMorphismStr (# G2, G3, g #) & F = LModMorphismStr (# G1, G2, f #) holds (G *' F) = LModMorphismStr (# G1, G3, (g * f) #) & (G * F) = LModMorphismStr (# G1, G3, (g * f) #)

    proof

      let G be Morphism of G2, G3, F be Morphism of G1, G2, g be Function of G2, G3, f be Function of G1, G2 such that

       A1: G = LModMorphismStr (# G2, G3, g #) & F = LModMorphismStr (# G1, G2, f #);

      ( dom G) = G2 by Def8

      .= ( cod F) by Def8;

      hence thesis by A1, Def10;

    end;

    theorem :: MOD_2:14

    

     Th14: for f,g be strict LModMorphism of R st ( dom g) = ( cod f) holds ex G1,G2,G3 be LeftMod of R, f0 be Function of G1, G2, g0 be Function of G2, G3 st f = LModMorphismStr (# G1, G2, f0 #) & g = LModMorphismStr (# G2, G3, g0 #) & (g * f) = LModMorphismStr (# G1, G3, (g0 * f0) #)

    proof

      let f,g be strict LModMorphism of R such that

       A1: ( dom g) = ( cod f);

      set G1 = ( dom f), G2 = ( cod f), G3 = ( cod g);

      reconsider f9 = f as strict Morphism of G1, G2 by Def8;

      reconsider g9 = g as strict Morphism of G2, G3 by A1, Def8;

      consider f0 be Function of G1, G2 such that

       A2: f9 = LModMorphismStr (# G1, G2, f0 #);

      consider g0 be Function of G2, G3 such that

       A3: g9 = LModMorphismStr (# G2, G3, g0 #) by Th8;

      take G1, G2, G3, f0, g0;

      thus thesis by A2, A3, Th13;

    end;

    theorem :: MOD_2:15

    for f,g be strict LModMorphism of R st ( dom g) = ( cod f) holds ( dom (g * f)) = ( dom f) & ( cod (g * f)) = ( cod g)

    proof

      let f,g be strict LModMorphism of R;

      assume ( dom g) = ( cod f);

      then

       A1: ex G1,G2,G3 be LeftMod of R, f0 be Function of G1, G2, g0 be Function of G2, G3 st f = LModMorphismStr (# G1, G2, f0 #) & g = LModMorphismStr (# G2, G3, g0 #) & (g * f) = LModMorphismStr (# G1, G3, (g0 * f0) #) by Th14;

      hence ( dom (g * f)) = ( dom f);

      thus thesis by A1;

    end;

    theorem :: MOD_2:16

    

     Th16: for G1,G2,G3,G4 be LeftMod of R, f be strict Morphism of G1, G2, g be strict Morphism of G2, G3, h be strict Morphism of G3, G4 holds (h * (g * f)) = ((h * g) * f)

    proof

      let G1,G2,G3,G4 be LeftMod of R, f be strict Morphism of G1, G2, g be strict Morphism of G2, G3, h be strict Morphism of G3, G4;

      consider f0 be Function of G1, G2 such that

       A1: f = LModMorphismStr (# G1, G2, f0 #) by Th8;

      consider g0 be Function of G2, G3 such that

       A2: g = LModMorphismStr (# G2, G3, g0 #) by Th8;

      consider h0 be Function of G3, G4 such that

       A3: h = LModMorphismStr (# G3, G4, h0 #) by Th8;

      

       A4: (h *' g) = LModMorphismStr (# G2, G4, (h0 * g0) #) by A2, A3, Th13;

      (g *' f) = LModMorphismStr (# G1, G3, (g0 * f0) #) by A1, A2, Th13;

      

      then (h * (g * f)) = LModMorphismStr (# G1, G4, (h0 * (g0 * f0)) #) by A3, Th13

      .= LModMorphismStr (# G1, G4, ((h0 * g0) * f0) #) by RELAT_1: 36

      .= ((h * g) * f) by A1, A4, Th13;

      hence thesis;

    end;

    theorem :: MOD_2:17

    for f,g,h be strict LModMorphism of R st ( dom h) = ( cod g) & ( dom g) = ( cod f) holds (h * (g * f)) = ((h * g) * f)

    proof

      let f,g,h be strict LModMorphism of R such that

       A1: ( dom h) = ( cod g) and

       A2: ( dom g) = ( cod f);

      set G2 = ( cod f), G3 = ( cod g);

      reconsider h9 = h as strict Morphism of G3, ( cod h) by A1, Def8;

      reconsider g9 = g as strict Morphism of G2, G3 by A2, Def8;

      reconsider f9 = f as strict Morphism of ( dom f), G2 by Def8;

      (h9 * (g9 * f9)) = ((h9 * g9) * f9) by Th16;

      hence thesis;

    end;

    theorem :: MOD_2:18

    ( dom ( ID G)) = G & ( cod ( ID G)) = G & (for f be strict LModMorphism of R st ( cod f) = G holds (( ID G) * f) = f) & for g be strict LModMorphism of R st ( dom g) = G holds (g * ( ID G)) = g

    proof

      set i = ( ID G);

      thus ( dom i) = G;

      thus ( cod i) = G;

      thus for f be strict LModMorphism of R st ( cod f) = G holds (i * f) = f

      proof

        let f be strict LModMorphism of R such that

         A1: ( cod f) = G;

        set H = ( dom f);

        reconsider f9 = f as Morphism of H, G by A1, Def8;

        consider m be Function of H, G such that

         A2: f9 = LModMorphismStr (# H, G, m #) by Th8;

        ( dom i) = G & (( id G) * m) = m by FUNCT_2: 17;

        hence thesis by A1, A2, Def10;

      end;

      thus for g be strict LModMorphism of R st ( dom g) = G holds (g * ( ID G)) = g

      proof

        let f be strict LModMorphism of R such that

         A3: ( dom f) = G;

        set H = ( cod f);

        reconsider f9 = f as Morphism of G, H by A3, Def8;

        consider m be Function of G, H such that

         A4: f9 = LModMorphismStr (# G, H, m #) by Th8;

        ( cod i) = G & (m * ( id G)) = m by FUNCT_2: 17;

        hence thesis by A3, A4, Def10;

      end;

    end;

    theorem :: MOD_2:19

    

     Th19: for u,v,w be Element of UN holds {u, v, w} is Element of UN

    proof

      let u,v,w be Element of UN;

       {u, v, w} = ( {u, v} \/ {w}) by ENUMSET1: 3;

      hence thesis;

    end;

    theorem :: MOD_2:20

    

     Th20: for u be Element of UN holds ( succ u) is Element of UN

    proof

      let u be Element of UN;

      ( succ u) = (u \/ {u});

      hence thesis;

    end;

    theorem :: MOD_2:21

    

     Th21: 0 is Element of UN & 1 is Element of UN & 2 is Element of UN

    proof

      thus 0 is Element of UN by CLASSES2: 56;

       {} is Element of UN & 1 = ( succ 0 ) by CLASSES2: 56;

      hence

       A1: 1 is Element of UN by Th20;

      2 = ( succ 1);

      hence thesis by A1, Th20;

    end;

    reserve a,b,c for Element of { 0 , 1, 2};

    

     Lm2: ex c st c = 0

    proof

      reconsider c = 0 as Element of { 0 , 1, 2} by ENUMSET1:def 1;

      take c;

      thus thesis;

    end;

    

     Lm3: ex c st c = 1

    proof

      reconsider c = 1 as Element of { 0 , 1, 2} by ENUMSET1:def 1;

      take c;

      thus thesis;

    end;

    

     Lm4: ex c st c = 2

    proof

      reconsider c = 2 as Element of { 0 , 1, 2} by ENUMSET1:def 1;

      take c;

      thus thesis;

    end;

    definition

      let a;

      :: MOD_2:def12

      func - a -> Element of { 0 , 1, 2} equals

      : Def12: 0 if a = 0 ,

2 if a = 1,

1 if a = 2;

      coherence by Lm3, Lm4;

      consistency ;

      let b;

      :: MOD_2:def13

      func a + b -> Element of { 0 , 1, 2} equals

      : Def13: b if a = 0 ,

a if b = 0 ,

2 if a = 1 & b = 1,

0 if a = 1 & b = 2,

0 if a = 2 & b = 1,

1 if a = 2 & b = 2;

      coherence by Lm2, Lm3, Lm4;

      consistency ;

      :: MOD_2:def14

      func a * b -> Element of { 0 , 1, 2} equals

      : Def14: 0 if b = 0 ,

0 if a = 0 ,

a if b = 1,

b if a = 1,

1 if a = 2 & b = 2;

      coherence by Lm3;

      consistency ;

    end

    definition

      :: MOD_2:def15

      func add3 -> BinOp of { 0 , 1, 2} means

      : Def15: (it . (a,b)) = (a + b);

      existence

      proof

        deffunc O( Element of { 0 , 1, 2}, Element of { 0 , 1, 2}) = ($1 + $2);

        ex o be BinOp of { 0 , 1, 2} st for a,b be Element of { 0 , 1, 2} holds (o . (a,b)) = O(a,b) from BINOP_1:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of { 0 , 1, 2} such that

         A1: for a, b holds (o1 . (a,b)) = (a + b) and

         A2: for a, b holds (o2 . (a,b)) = (a + b);

        now

          let a, b;

          

          thus (o1 . (a,b)) = (a + b) by A1

          .= (o2 . (a,b)) by A2;

        end;

        hence thesis by BINOP_1: 2;

      end;

      :: MOD_2:def16

      func mult3 -> BinOp of { 0 , 1, 2} means

      : Def16: (it . (a,b)) = (a * b);

      existence

      proof

        deffunc O( Element of { 0 , 1, 2}, Element of { 0 , 1, 2}) = ($1 * $2);

        ex o be BinOp of { 0 , 1, 2} st for a,b be Element of { 0 , 1, 2} holds (o . (a,b)) = O(a,b) from BINOP_1:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of { 0 , 1, 2} such that

         A3: for a, b holds (o1 . (a,b)) = (a * b) and

         A4: for a, b holds (o2 . (a,b)) = (a * b);

        now

          let a, b;

          

          thus (o1 . (a,b)) = (a * b) by A3

          .= (o2 . (a,b)) by A4;

        end;

        hence thesis by BINOP_1: 2;

      end;

      :: MOD_2:def17

      func compl3 -> UnOp of { 0 , 1, 2} means

      : Def17: (it . a) = ( - a);

      existence

      proof

        deffunc F( Element of { 0 , 1, 2}) = ( - $1);

        ex f be UnOp of { 0 , 1, 2} st for x be Element of { 0 , 1, 2} holds (f . x) = F(x) from FUNCT_2:sch 4;

        hence thesis;

      end;

      uniqueness

      proof

        let o1,o2 be UnOp of { 0 , 1, 2} such that

         A5: for a holds (o1 . a) = ( - a) and

         A6: for a holds (o2 . a) = ( - a);

        now

          let a;

          

          thus (o1 . a) = ( - a) by A5

          .= (o2 . a) by A6;

        end;

        hence thesis by FUNCT_2: 63;

      end;

      :: MOD_2:def18

      func unit3 -> Element of { 0 , 1, 2} equals 1;

      coherence by ENUMSET1:def 1;

      :: MOD_2:def19

      func zero3 -> Element of { 0 , 1, 2} equals 0 ;

      coherence by ENUMSET1:def 1;

    end

    definition

      :: MOD_2:def20

      func Z_3 -> strict doubleLoopStr equals

      : Def20: doubleLoopStr (# { 0 , 1, 2}, add3 , mult3 , unit3 , zero3 #);

      coherence ;

    end

    registration

      cluster Z_3 -> non empty;

      coherence ;

    end

     Lm5:

    now

      let h,e be Element of Z_3 ;

      assume

       A1: e = 1;

      reconsider a = e, b = h as Element of { 0 , 1, 2};

      

      thus (h * e) = (b * a) by Def16

      .= h by A1, Def14;

      

      thus (e * h) = (a * b) by Def16

      .= h by A1, Def14;

    end;

    registration

      cluster Z_3 -> well-unital;

      coherence by Lm5;

    end

    theorem :: MOD_2:22

    

     Th22: ( 0. Z_3 ) = 0 & ( 1. Z_3 ) = 1 & ( 0. Z_3 ) is Element of { 0 , 1, 2} & ( 1. Z_3 ) is Element of { 0 , 1, 2} & the addF of Z_3 = add3 & the multF of Z_3 = mult3 ;

    

     Lm6: for x,y,z be Scalar of Z_3 , X,Y,Z be Element of { 0 , 1, 2} st X = x & Y = y & Z = z holds ((x + y) + z) = ((X + Y) + Z) & (x + (y + z)) = (X + (Y + Z)) & ((x * y) * z) = ((X * Y) * Z) & (x * (y * z)) = (X * (Y * Z))

    proof

      let x,y,z be Scalar of Z_3 , X,Y,Z be Element of { 0 , 1, 2};

      assume that

       A1: X = x and

       A2: Y = y and

       A3: Z = z;

      

       A4: (x * y) = (X * Y) & (y * z) = (Y * Z) by A1, A2, A3, Def16;

      (x + y) = (X + Y) & (y + z) = (Y + Z) by A1, A2, A3, Def15;

      hence thesis by A1, A3, A4, Def15, Def16;

    end;

    

     Lm7: for x,y,z,a be Element of { 0 , 1, 2} st a = 0 holds (x + ( - x)) = a & (x + a) = x & ((x + y) + z) = (x + (y + z))

    proof

      let x,y,z,a be Element of { 0 , 1, 2} such that

       A1: a = 0 ;

      thus (x + ( - x)) = a

      proof

        now

          per cases by ENUMSET1:def 1;

            suppose

             A2: x = 0 ;

            then ( - x) = 0 by Def12;

            hence thesis by A1, A2, Def13;

          end;

            suppose

             A3: x = 1;

            then ( - x) = 2 by Def12;

            hence thesis by A1, A3, Def13;

          end;

            suppose

             A4: x = 2;

            then ( - x) = 1 by Def12;

            hence thesis by A1, A4, Def13;

          end;

        end;

        hence thesis;

      end;

      thus (x + a) = x by A1, Def13;

      thus ((x + y) + z) = (x + (y + z))

      proof

        now

          per cases by ENUMSET1:def 1;

            suppose

             A5: x = 0 ;

            

            hence ((x + y) + z) = (y + z) by Def13

            .= (x + (y + z)) by A5, Def13;

          end;

            suppose

             A6: y = 0 ;

            then (x + y) = x by Def13;

            hence thesis by A6, Def13;

          end;

            suppose

             A7: z = 0 ;

            then (y + z) = y by Def13;

            hence thesis by A7, Def13;

          end;

            suppose

             A8: x = 1 & y = 1 & z = 1;

            

            thus ((x + y) + z) = 0 by A8, Def13

            .= (x + (y + z)) by A8, Def13;

          end;

            suppose

             A9: x = 1 & y = 1 & z = 2;

            then

             A10: (y + z) = 0 by Def13;

            (x + y) = 2 by A9, Def13;

            

            hence ((x + y) + z) = 1 by A9, Def13

            .= (x + (y + z)) by A9, A10, Def13;

          end;

            suppose

             A11: x = 1 & y = 2 & z = 1;

            then

             A12: (y + z) = 0 by Def13;

            (x + y) = 0 by A11, Def13;

            

            hence ((x + y) + z) = 1 by A11, Def13

            .= (x + (y + z)) by A11, A12, Def13;

          end;

            suppose

             A13: x = 1 & y = 2 & z = 2;

            then

             A14: (y + z) = 1 by Def13;

            (x + y) = 0 by A13, Def13;

            

            hence ((x + y) + z) = 2 by A13, Def13

            .= (x + (y + z)) by A13, A14, Def13;

          end;

            suppose

             A15: x = 2 & y = 1 & z = 1;

            then

             A16: (y + z) = 2 by Def13;

            (x + y) = 0 by A15, Def13;

            

            hence ((x + y) + z) = 1 by A15, Def13

            .= (x + (y + z)) by A15, A16, Def13;

          end;

            suppose

             A17: x = 2 & y = 1 & z = 2;

            then

             A18: (y + z) = 0 by Def13;

            (x + y) = 0 by A17, Def13;

            

            hence ((x + y) + z) = 2 by A17, Def13

            .= (x + (y + z)) by A17, A18, Def13;

          end;

            suppose

             A19: x = 2 & y = 2 & z = 1;

            then

             A20: (y + z) = 0 by Def13;

            (x + y) = 1 by A19, Def13;

            

            hence ((x + y) + z) = 2 by A19, Def13

            .= (x + (y + z)) by A19, A20, Def13;

          end;

            suppose

             A21: x = 2 & y = 2 & z = 2;

            

            thus ((x + y) + z) = 0 by A21, Def13

            .= (x + (y + z)) by A21, Def13;

          end;

        end;

        hence thesis;

      end;

    end;

    registration

      cluster Z_3 -> add-associative right_zeroed right_complementable;

      coherence

      proof

        thus Z_3 is add-associative

        proof

          let x,y,z be Element of Z_3 ;

          reconsider X = x, Y = y, Z = z as Element of { 0 , 1, 2};

          

          thus ((x + y) + z) = ((X + Y) + Z) by Lm6

          .= (X + (Y + Z)) by Lm7

          .= (x + (y + z)) by Lm6;

        end;

        thus Z_3 is right_zeroed

        proof

          let x be Element of Z_3 ;

          reconsider X = x, a = 0 as Element of { 0 , 1, 2} by Def20;

          

          thus (x + ( 0. Z_3 )) = (X + a) by Def15

          .= x by Lm7;

        end;

        let x be Element of Z_3 ;

        reconsider x9 = x as Element of { 0 , 1, 2};

        reconsider y = ( compl3 . x9) as Element of Z_3 ;

        reconsider y9 = y as Element of { 0 , 1, 2};

        take y;

        

         A1: y9 = ( - x9) by Def17;

        thus (x + y) = ( 0. Z_3 )

        proof

          per cases by ENUMSET1:def 1;

            suppose

             A2: x = 0 ;

            then

             A3: y9 = 0 by A1, Def12;

            

            thus (x + y) = (x9 + y9) by Def15

            .= ( 0. Z_3 ) by A2, A3, Def13;

          end;

            suppose

             A4: x = 1;

            then

             A5: y9 = 2 by A1, Def12;

            

            thus (x + y) = (x9 + y9) by Def15

            .= ( 0. Z_3 ) by A4, A5, Def13;

          end;

            suppose

             A6: x = 2;

            then

             A7: y9 = 1 by A1, Def12;

            

            thus (x + y) = (x9 + y9) by Def15

            .= ( 0. Z_3 ) by A6, A7, Def13;

          end;

        end;

      end;

    end

    theorem :: MOD_2:23

    

     Th23: for x,y be Scalar of Z_3 , X,Y be Element of { 0 , 1, 2} st X = x & Y = y holds (x + y) = (X + Y) & (x * y) = (X * Y) & ( - x) = ( - X)

    proof

      let x,y be Scalar of Z_3 , X,Y be Element of { 0 , 1, 2};

      assume that

       A1: X = x and

       A2: Y = y;

      thus (x + y) = (X + Y) by A1, A2, Def15;

      thus (x * y) = (X * Y) by A1, A2, Def16;

      reconsider a = ( - X) as Element of Z_3 ;

      (x + a) = (X + ( - X)) by A1, Def15

      .= ( 0. Z_3 ) by Lm7;

      hence thesis by RLVECT_1:def 10;

    end;

    theorem :: MOD_2:24

    

     Th24: for x,y,z be Scalar of Z_3 , X,Y,Z be Element of { 0 , 1, 2} st X = x & Y = y & Z = z holds ((x + y) + z) = ((X + Y) + Z) & (x + (y + z)) = (X + (Y + Z)) & ((x * y) * z) = ((X * Y) * Z) & (x * (y * z)) = (X * (Y * Z))

    proof

      let x,y,z be Scalar of Z_3 , X,Y,Z be Element of { 0 , 1, 2};

      assume that

       A1: X = x and

       A2: Y = y and

       A3: Z = z;

      

       A4: (x * y) = (X * Y) & (y * z) = (Y * Z) by A1, A2, A3, Th23;

      (x + y) = (X + Y) & (y + z) = (Y + Z) by A1, A2, A3, Th23;

      hence thesis by A1, A3, A4, Th23;

    end;

    theorem :: MOD_2:25

    

     Th25: for x,y,z,a,b be Element of { 0 , 1, 2} st a = 0 & b = 1 holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + a) = x & (x + ( - x)) = a & (x * y) = (y * x) & ((x * y) * z) = (x * (y * z)) & (b * x) = x & (x <> a implies ex y be Element of { 0 , 1, 2} st (x * y) = b) & a <> b & (x * (y + z)) = ((x * y) + (x * z))

    proof

      let x,y,z,a,b be Element of { 0 , 1, 2} such that

       A1: a = 0 and

       A2: b = 1;

      thus (x + y) = (y + x)

      proof

        now

          per cases by ENUMSET1:def 1;

            suppose

             A3: x = 0 ;

            

            hence (x + y) = y by Def13

            .= (y + x) by A3, Def13;

          end;

            suppose

             A4: y = 0 ;

            

            hence (x + y) = x by Def13

            .= (y + x) by A4, Def13;

          end;

            suppose x = 1 & y = 1;

            hence thesis;

          end;

            suppose

             A5: x = 1 & y = 2;

            

            hence (x + y) = 0 by Def13

            .= (y + x) by A5, Def13;

          end;

            suppose

             A6: x = 2 & y = 1;

            

            hence (x + y) = 0 by Def13

            .= (y + x) by A6, Def13;

          end;

            suppose x = 2 & y = 2;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      thus ((x + y) + z) = (x + (y + z)) by A1, Lm7;

      thus (x + a) = x by A1, Def13;

      thus (x + ( - x)) = a by A1, Lm7;

      thus (x * y) = (y * x)

      proof

        now

          per cases by ENUMSET1:def 1;

            suppose

             A7: y = 0 ;

            

            hence (x * y) = 0 by Def14

            .= (y * x) by A7, Def14;

          end;

            suppose

             A8: x = 0 ;

            

            hence (x * y) = 0 by Def14

            .= (y * x) by A8, Def14;

          end;

            suppose

             A9: y = 1;

            

            hence (x * y) = x by Def14

            .= (y * x) by A9, Def14;

          end;

            suppose

             A10: x = 1;

            

            hence (x * y) = y by Def14

            .= (y * x) by A10, Def14;

          end;

            suppose x = 2 & y = 2;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      thus ((x * y) * z) = (x * (y * z))

      proof

        now

          per cases by ENUMSET1:def 1;

            suppose

             A11: z = 0 ;

            then

             A12: (y * z) = 0 by Def14;

            

            thus ((x * y) * z) = 0 by A11, Def14

            .= (x * (y * z)) by A12, Def14;

          end;

            suppose

             A13: y = 0 ;

            then

             A14: (y * z) = 0 by Def14;

            (x * y) = 0 by A13, Def14;

            

            hence ((x * y) * z) = 0 by Def14

            .= (x * (y * z)) by A14, Def14;

          end;

            suppose

             A15: x = 0 ;

            then (x * y) = 0 by Def14;

            

            hence ((x * y) * z) = 0 by Def14

            .= (x * (y * z)) by A15, Def14;

          end;

            suppose

             A16: z = 1;

            then (y * z) = y by Def14;

            hence thesis by A16, Def14;

          end;

            suppose

             A17: y = 1;

            then (x * y) = x by Def14;

            hence thesis by A17, Def14;

          end;

            suppose

             A18: x = 1;

            

            hence ((x * y) * z) = (y * z) by Def14

            .= (x * (y * z)) by A18, Def14;

          end;

            suppose

             A19: x = 2 & y = 2 & z = 2;

            then

             A20: (y * z) = 1 by Def14;

            (x * y) = 1 by A19, Def14;

            

            hence ((x * y) * z) = x by A19, Def14

            .= (x * (y * z)) by A20, Def14;

          end;

        end;

        hence thesis;

      end;

      thus (b * x) = x by A2, Def14;

      thus x <> a implies ex y be Element of { 0 , 1, 2} st (x * y) = b

      proof

        now

          per cases by ENUMSET1:def 1;

            case x = 0 ;

            hence thesis by A1;

          end;

            case

             A21: x = 1;

            reconsider y = 1 as Element of { 0 , 1, 2} by ENUMSET1:def 1;

            take y;

            (x * y) = 1 by A21, Def14;

            hence thesis by A2;

          end;

            case

             A22: x = 2;

            reconsider y = 2 as Element of { 0 , 1, 2} by ENUMSET1:def 1;

            take y;

            (x * y) = 1 by A22, Def14;

            hence thesis by A2;

          end;

        end;

        hence thesis;

      end;

      thus a <> b by A1, A2;

      thus (x * (y + z)) = ((x * y) + (x * z))

      proof

        now

          per cases by ENUMSET1:def 1;

            suppose

             A23: x = 0 ;

            then

             A24: (x * y) = 0 & (x * z) = 0 by Def14;

            

            thus (x * (y + z)) = 0 by A23, Def14

            .= ((x * y) + (x * z)) by A24, Def13;

          end;

            suppose y = 0 ;

            then (y + z) = z & (x * y) = 0 by Def13, Def14;

            hence thesis by Def13;

          end;

            suppose z = 0 ;

            then (y + z) = y & (x * z) = 0 by Def13, Def14;

            hence thesis by Def13;

          end;

            suppose

             A25: x = 1 & y = 1 & z = 1;

            then (x * y) = 1 by Def14;

            hence thesis by A25, Def14;

          end;

            suppose

             A26: x = 1 & y = 1 & z = 2;

            then

             A27: (x * y) = 1 & (x * z) = 2 by Def14;

            (y + z) = 0 by A26, Def13;

            

            hence (x * (y + z)) = 0 by Def14

            .= ((x * y) + (x * z)) by A27, Def13;

          end;

            suppose

             A28: x = 1 & y = 2 & z = 1;

            then

             A29: (x * y) = 2 & (x * z) = 1 by Def14;

            (y + z) = 0 by A28, Def13;

            

            hence (x * (y + z)) = 0 by Def14

            .= ((x * y) + (x * z)) by A29, Def13;

          end;

            suppose

             A30: x = 1 & y = 2 & z = 2;

            then (x * y) = 2 by Def14;

            hence thesis by A30, Def14;

          end;

            suppose

             A31: x = 2 & y = 1 & z = 1;

            then

             A32: (x * y) = 2 by Def14;

            (y + z) = 2 by A31, Def13;

            

            hence (x * (y + z)) = 1 by A31, Def14

            .= ((x * y) + (x * z)) by A31, A32, Def13;

          end;

            suppose

             A33: x = 2 & y = 1 & z = 2;

            then

             A34: (x * y) = 2 & (x * z) = 1 by Def14;

            (y + z) = 0 by A33, Def13;

            

            hence (x * (y + z)) = 0 by Def14

            .= ((x * y) + (x * z)) by A34, Def13;

          end;

            suppose

             A35: x = 2 & y = 2 & z = 1;

            then

             A36: (x * y) = 1 & (x * z) = 2 by Def14;

            (y + z) = 0 by A35, Def13;

            

            hence (x * (y + z)) = 0 by Def14

            .= ((x * y) + (x * z)) by A36, Def13;

          end;

            suppose

             A37: x = 2 & y = 2 & z = 2;

            then

             A38: (x * y) = 1 by Def14;

            (y + z) = 1 by A37, Def13;

            

            hence (x * (y + z)) = 2 by A37, Def14

            .= ((x * y) + (x * z)) by A37, A38, Def13;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: MOD_2:26

    

     Th26: for F be non empty doubleLoopStr st for x,y,z be Scalar of F holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. F)) = x & (x + ( - x)) = ( 0. F) & (x * y) = (y * x) & ((x * y) * z) = (x * (y * z)) & (( 1. F) * x) = x & (x * ( 1. F)) = x & (x <> ( 0. F) implies ex y be Scalar of F st (x * y) = ( 1. F)) & ( 0. F) <> ( 1. F) & (x * (y + z)) = ((x * y) + (x * z)) holds F is Field

    proof

      let F be non empty doubleLoopStr such that

       A1: for x,y,z be Scalar of F holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. F)) = x & (x + ( - x)) = ( 0. F) & (x * y) = (y * x) & ((x * y) * z) = (x * (y * z)) & (( 1. F) * x) = x & (x * ( 1. F)) = x & (x <> ( 0. F) implies ex y be Scalar of F st (x * y) = ( 1. F)) & ( 0. F) <> ( 1. F) & (x * (y + z)) = ((x * y) + (x * z));

      

       A2: for x be Scalar of F st x <> ( 0. F) holds ex y be Scalar of F st (y * x) = ( 1. F)

      proof

        let x be Scalar of F;

        assume x <> ( 0. F);

        then

        consider y be Scalar of F such that

         A3: (x * y) = ( 1. F) by A1;

        take y;

        thus thesis by A1, A3;

      end;

       A4:

      now

        let x,y,z be Scalar of F;

        thus (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. F)) = x & (x + ( - x)) = ( 0. F) & (x * y) = (y * x) & ((x * y) * z) = (x * (y * z)) & (( 1. F) * x) = x & (x * ( 1. F)) = x & (x <> ( 0. F) implies ex y be Scalar of F st (x * y) = ( 1. F)) & ( 0. F) <> ( 1. F) & (x * (y + z)) = ((x * y) + (x * z)) by A1;

        

        thus ((y + z) * x) = (x * (y + z)) by A1

        .= ((x * y) + (x * z)) by A1

        .= ((y * x) + (x * z)) by A1

        .= ((y * x) + (z * x)) by A1;

      end;

      F is right_complementable

      proof

        let v be Element of F;

        take ( - v);

        thus thesis by A4;

      end;

      hence thesis by A2, A4, GROUP_1:def 3, GROUP_1:def 12, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, STRUCT_0:def 8, VECTSP_1:def 6, VECTSP_1:def 7, VECTSP_1:def 9;

    end;

    theorem :: MOD_2:27

    

     Th27: Z_3 is Fanoian Field

    proof

      set F = Z_3 ;

      reconsider a = ( 0. F), b = ( 1. F) as Element of { 0 , 1, 2};

      now

        let x,y,z be Scalar of Z_3 ;

        thus (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. Z_3 )) = x & (x + ( - x)) = ( 0. Z_3 ) & (x * y) = (y * x) & ((x * y) * z) = (x * (y * z)) & (( 1. Z_3 ) * x) = x & (x * ( 1. Z_3 )) = x & (x <> ( 0. Z_3 ) implies ex y be Scalar of Z_3 st (x * y) = ( 1. Z_3 )) & ( 0. Z_3 ) <> ( 1. Z_3 ) & (x * (y + z)) = ((x * y) + (x * z))

        proof

          reconsider X = x, Y = y, Z = z as Element of { 0 , 1, 2};

          

           A1: (x * y) = (X * Y) & (x * z) = (X * Z) by Th23;

          

          thus (x + y) = (X + Y) by Th23

          .= (Y + X) by Th25

          .= (y + x) by Th23;

          

          thus ((x + y) + z) = ((X + Y) + Z) by Th24

          .= (X + (Y + Z)) by Th25

          .= (x + (y + z)) by Th24;

          

          thus (x + ( 0. Z_3 )) = (X + a) by Th23

          .= x by Th25;

          ( - x) = ( - X) by Th23;

          

          hence (x + ( - x)) = (X + ( - X)) by Th23

          .= ( 0. Z_3 ) by Th25;

          

          thus (x * y) = (X * Y) by Th23

          .= (Y * X) by Th25

          .= (y * x) by Th23;

          

          thus ((x * y) * z) = ((X * Y) * Z) by Th24

          .= (X * (Y * Z)) by Th25

          .= (x * (y * z)) by Th24;

          

          thus (( 1. Z_3 ) * x) = (b * X) by Th23

          .= x by Th25;

          

          thus (x * ( 1. Z_3 )) = (X * b) by Th23

          .= (b * X) by Th25

          .= x by Th25;

          thus x <> ( 0. Z_3 ) implies ex y be Scalar of Z_3 st (x * y) = ( 1. Z_3 )

          proof

            assume x <> ( 0. Z_3 );

            then

            consider Y be Element of { 0 , 1, 2} such that

             A2: (X * Y) = b by Th25;

            reconsider y = Y as Scalar of Z_3 ;

            take y;

            thus thesis by A2, Th23;

          end;

          thus ( 0. Z_3 ) <> ( 1. Z_3 );

          (y + z) = (Y + Z) by Th23;

          

          hence (x * (y + z)) = (X * (Y + Z)) by Th23

          .= ((X * Y) + (X * Z)) by Th25

          .= ((x * y) + (x * z)) by A1, Th23;

        end;

      end;

      then

      reconsider F as Field by Th26;

      (( 1. F) + ( 1. F)) = (b + b) by Def15

      .= 2 by Def13;

      hence thesis by Th22, VECTSP_1:def 19;

    end;

    registration

      cluster Z_3 -> Fanoian add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible;

      coherence by Th27;

    end

    

     Lm8: the carrier of Z_3 in UN

    proof

      reconsider a = 0 , b = 1, c = 2 as Element of UN by Th21;

       {a, b, c} is Element of UN by Th19;

      hence thesis;

    end;

    theorem :: MOD_2:28

    

     Th28: for f be Function of D, D9 st D in UN & D9 in UN holds f in UN

    proof

      let f be Function of D, D9;

      assume D in UN & D9 in UN;

      then

       A1: ( Funcs (D,D9)) in UN by CLASSES2: 61;

      f in ( Funcs (D,D9)) by FUNCT_2: 8;

      hence thesis by A1, ORDINAL1: 10;

    end;

    

     Lm9: (for f be BinOp of D st D in UN holds f in UN) & for f be UnOp of D st D in UN holds f in UN

    proof

      now

        let f be BinOp of D;

        assume

         A1: D in UN;

        then [:D, D:] in UN by CLASSES2: 61;

        then

         A2: ( Funcs ( [:D, D:],D)) in UN by A1, CLASSES2: 61;

        f in ( Funcs ( [:D, D:],D)) by FUNCT_2: 8;

        hence f in UN by A2, ORDINAL1: 10;

      end;

      hence thesis by Th28;

    end;

    theorem :: MOD_2:29

    the carrier of Z_3 in UN & the addF of Z_3 in UN & ( comp Z_3 ) in UN & ( 0. Z_3 ) in UN & the multF of Z_3 in UN & ( 1. Z_3 ) in UN

    proof

      thus the carrier of Z_3 in UN by Lm8;

      hence thesis by Lm9, ORDINAL1: 10;

    end;