group_1.miz



    begin

    reserve m,n for Nat;

    reserve i,j for Integer;

    reserve S for non empty multMagma;

    reserve r,r1,r2,s,s1,s2,t,t1,t2 for Element of S;

     Lm1:

    now

      set G = multMagma (# REAL , addreal #);

      thus for h,g,f be Element of G holds ((h * g) * f) = (h * (g * f))

      proof

        let h,g,f be Element of G;

        reconsider A = h, B = g, C = f as Real;

        

         A1: (g * f) = (B + C) by BINOP_2:def 9;

        (h * g) = (A + B) by BINOP_2:def 9;

        

        hence ((h * g) * f) = ((A + B) + C) by BINOP_2:def 9

        .= (A + (B + C))

        .= (h * (g * f)) by A1, BINOP_2:def 9;

      end;

      reconsider e = 0 as Element of G by XREAL_0:def 1;

      take e;

      let h be Element of G;

      reconsider A = h as Real;

      

      thus (h * e) = (A + 0 ) by BINOP_2:def 9

      .= h;

      

      thus (e * h) = ( 0 + A) by BINOP_2:def 9

      .= h;

      reconsider g = ( - A) as Element of G by XREAL_0:def 1;

      take g;

      

      thus (h * g) = (A + ( - A)) by BINOP_2:def 9

      .= e;

      

      thus (g * h) = (( - A) + A) by BINOP_2:def 9

      .= e;

    end;

    definition

      let IT be multMagma;

      :: GROUP_1:def1

      attr IT is unital means ex e be Element of IT st for h be Element of IT holds (h * e) = h & (e * h) = h;

      :: GROUP_1:def2

      attr IT is Group-like means

      : Def2: ex e be Element of IT st for h be Element of IT holds (h * e) = h & (e * h) = h & ex g be Element of IT st (h * g) = e & (g * h) = e;

      :: GROUP_1:def3

      attr IT is associative means

      : Def3: for x,y,z be Element of IT holds ((x * y) * z) = (x * (y * z));

    end

    registration

      cluster Group-like -> unital for multMagma;

      coherence ;

    end

    registration

      cluster strict Group-like associative non empty for multMagma;

      existence

      proof

         multMagma (# REAL , addreal #) is Group-like associative by Lm1;

        hence thesis;

      end;

    end

    definition

      mode Group is Group-like associative non empty multMagma;

    end

    theorem :: GROUP_1:1

    ((for r, s, t holds ((r * s) * t) = (r * (s * t))) & ex t st for s1 holds (s1 * t) = s1 & (t * s1) = s1 & ex s2 st (s1 * s2) = t & (s2 * s1) = t) implies S is Group by Def2, Def3;

    theorem :: GROUP_1:2

    (for r, s, t holds ((r * s) * t) = (r * (s * t))) & (for r, s holds (ex t st (r * t) = s) & (ex t st (t * r) = s)) implies S is associative Group-like

    proof

      set r = the Element of S;

      assume that

       A1: for r, s, t holds ((r * s) * t) = (r * (s * t)) and

       A2: for r, s holds (ex t st (r * t) = s) & ex t st (t * r) = s;

      consider s1 such that

       A3: (r * s1) = r by A2;

      thus for r, s, t holds ((r * s) * t) = (r * (s * t)) by A1;

      take s1;

      let s;

      ex t st (t * r) = s by A2;

      hence

       A4: (s * s1) = s by A1, A3;

      consider s2 such that

       A5: (s2 * r) = r by A2;

      consider t1 such that

       A6: (r * t1) = s1 by A2;

      

       A7: ex t2 st (t2 * r) = s2 by A2;

      

       A8: s1 = (s2 * (r * t1)) by A1, A5, A6

      .= s2 by A1, A3, A6, A7;

      ex t st (r * t) = s by A2;

      hence

       A9: (s1 * s) = s by A1, A5, A8;

      consider t1 such that

       A10: (s * t1) = s1 by A2;

      consider t2 such that

       A11: (t2 * s) = s1 by A2;

      take t1;

      consider r1 such that

       A12: (s * r1) = t1 by A2;

      

       A13: ex r2 st (r2 * s) = t2 by A2;

      t1 = (s1 * (s * r1)) by A1, A9, A12

      .= (t2 * (s * t1)) by A1, A11, A12

      .= t2 by A1, A4, A10, A13;

      hence thesis by A10, A11;

    end;

    theorem :: GROUP_1:3

    

     Th3: multMagma (# REAL , addreal #) is associative Group-like

    proof

      set G = multMagma (# REAL , addreal #);

      thus for h,g,f be Element of G holds ((h * g) * f) = (h * (g * f))

      proof

        let h,g,f be Element of G;

        reconsider A = h, B = g, C = f as Real;

        

         A1: (g * f) = (B + C) by BINOP_2:def 9;

        (h * g) = (A + B) by BINOP_2:def 9;

        

        hence ((h * g) * f) = ((A + B) + C) by BINOP_2:def 9

        .= (A + (B + C))

        .= (h * (g * f)) by A1, BINOP_2:def 9;

      end;

      reconsider e = 0 as Element of G by XREAL_0:def 1;

      take e;

      let h be Element of G;

      reconsider A = h as Real;

      

      thus (h * e) = (A + 0 ) by BINOP_2:def 9

      .= h;

      

      thus (e * h) = ( 0 + A) by BINOP_2:def 9

      .= h;

      reconsider g = ( - A) as Element of G by XREAL_0:def 1;

      take g;

      

      thus (h * g) = (A + ( - A)) by BINOP_2:def 9

      .= e;

      

      thus (g * h) = (( - A) + A) by BINOP_2:def 9

      .= e;

    end;

    reserve G for Group-like non empty multMagma;

    reserve e,h for Element of G;

    definition

      let G be multMagma;

      :: GROUP_1:def4

      func 1_ G -> Element of G means

      : Def4: for h be Element of G holds (h * it ) = h & (it * h) = h;

      existence by A1;

      uniqueness

      proof

        let e1,e2 be Element of G;

        assume that

         A2: for h be Element of G holds (h * e1) = h & (e1 * h) = h and

         A3: for h be Element of G holds (h * e2) = h & (e2 * h) = h;

        

        thus e1 = (e2 * e1) by A3

        .= e2 by A2;

      end;

    end

    theorem :: GROUP_1:4

    (for h holds (h * e) = h & (e * h) = h) implies e = ( 1_ G) by Def4;

    reserve G for Group;

    reserve f,g,h for Element of G;

    definition

      let G, h;

      :: GROUP_1:def5

      func h " -> Element of G means

      : Def5: (h * it ) = ( 1_ G) & (it * h) = ( 1_ G);

      existence

      proof

        consider e be Element of G such that

         A1: for h be Element of G holds (h * e) = h & (e * h) = h & ex g be Element of G st (h * g) = e & (g * h) = e by Def2;

        consider g be Element of G such that

         A2: (h * g) = e & (g * h) = e by A1;

        take g;

        thus thesis by A1, A2, Def4;

      end;

      uniqueness

      proof

        let h1,h2 be Element of G;

        assume that

         A3: (h * h1) = ( 1_ G) and (h1 * h) = ( 1_ G) and (h * h2) = ( 1_ G) and

         A4: (h2 * h) = ( 1_ G);

        

        thus h1 = (( 1_ G) * h1) by Def4

        .= (h2 * (h * h1)) by A4, Def3

        .= h2 by A3, Def4;

      end;

      involutiveness ;

    end

    theorem :: GROUP_1:5

    (h * g) = ( 1_ G) & (g * h) = ( 1_ G) implies g = (h " ) by Def5;

    theorem :: GROUP_1:6

    

     Th6: (h * g) = (h * f) or (g * h) = (f * h) implies g = f

    proof

      assume (h * g) = (h * f) or (g * h) = (f * h);

      then ((h " ) * (h * g)) = (((h " ) * h) * f) or ((g * h) * (h " )) = (f * (h * (h " ))) by Def3;

      then ((h " ) * (h * g)) = (( 1_ G) * f) or (g * (h * (h " ))) = (f * (h * (h " ))) by Def3, Def5;

      then ((h " ) * (h * g)) = f or (g * ( 1_ G)) = (f * (h * (h " ))) by Def4, Def5;

      then (((h " ) * h) * g) = f or g = (f * (h * (h " ))) by Def3, Def4;

      then (((h " ) * h) * g) = f or g = (f * ( 1_ G)) by Def5;

      then (( 1_ G) * g) = f or g = f by Def4, Def5;

      hence thesis by Def4;

    end;

    theorem :: GROUP_1:7

    (h * g) = h or (g * h) = h implies g = ( 1_ G)

    proof

      (h * ( 1_ G)) = h & (( 1_ G) * h) = h by Def4;

      hence thesis by Th6;

    end;

    theorem :: GROUP_1:8

    

     Th8: (( 1_ G) " ) = ( 1_ G)

    proof

      ((( 1_ G) " ) * ( 1_ G)) = ( 1_ G) by Def5;

      hence thesis by Def4;

    end;

    theorem :: GROUP_1:9

    (h " ) = (g " ) implies h = g

    proof

      assume (h " ) = (g " );

      then

       A1: (h * (g " )) = ( 1_ G) by Def5;

      (g * (g " )) = ( 1_ G) by Def5;

      hence thesis by A1, Th6;

    end;

    theorem :: GROUP_1:10

    (h " ) = ( 1_ G) implies h = ( 1_ G)

    proof

      (( 1_ G) " ) = ( 1_ G) by Th8;

      hence thesis;

    end;

    ::$Canceled

    theorem :: GROUP_1:12

    

     Th11: (h * g) = ( 1_ G) implies h = (g " ) & g = (h " )

    proof

      assume

       A1: (h * g) = ( 1_ G);

      (h * (h " )) = ( 1_ G) & ((g " ) * g) = ( 1_ G) by Def5;

      hence thesis by A1, Th6;

    end;

    theorem :: GROUP_1:13

    

     Th12: (h * f) = g iff f = ((h " ) * g)

    proof

      (h * ((h " ) * g)) = ((h * (h " )) * g) by Def3

      .= (( 1_ G) * g) by Def5

      .= g by Def4;

      hence (h * f) = g implies f = ((h " ) * g) by Th6;

      assume f = ((h " ) * g);

      

      hence (h * f) = ((h * (h " )) * g) by Def3

      .= (( 1_ G) * g) by Def5

      .= g by Def4;

    end;

    theorem :: GROUP_1:14

    

     Th13: (f * h) = g iff f = (g * (h " ))

    proof

      ((g * (h " )) * h) = (g * ((h " ) * h)) by Def3

      .= (g * ( 1_ G)) by Def5

      .= g by Def4;

      hence (f * h) = g implies f = (g * (h " )) by Th6;

      assume f = (g * (h " ));

      

      hence (f * h) = (g * ((h " ) * h)) by Def3

      .= (g * ( 1_ G)) by Def5

      .= g by Def4;

    end;

    theorem :: GROUP_1:15

    ex f st (g * f) = h

    proof

      take ((g " ) * h);

      thus thesis by Th12;

    end;

    theorem :: GROUP_1:16

    ex f st (f * g) = h

    proof

      take (h * (g " ));

      thus thesis by Th13;

    end;

    theorem :: GROUP_1:17

    

     Th16: ((h * g) " ) = ((g " ) * (h " ))

    proof

      (((g " ) * (h " )) * (h * g)) = ((((g " ) * (h " )) * h) * g) by Def3

      .= (((g " ) * ((h " ) * h)) * g) by Def3

      .= (((g " ) * ( 1_ G)) * g) by Def5

      .= ((g " ) * g) by Def4

      .= ( 1_ G) by Def5;

      hence thesis by Th11;

    end;

    theorem :: GROUP_1:18

    

     Th17: (g * h) = (h * g) iff ((g * h) " ) = ((g " ) * (h " ))

    proof

      thus (g * h) = (h * g) implies ((g * h) " ) = ((g " ) * (h " )) by Th16;

      assume ((g * h) " ) = ((g " ) * (h " ));

      

      then

       A1: ((h * g) * ((g * h) " )) = (((h * g) * (g " )) * (h " )) by Def3

      .= ((h * (g * (g " ))) * (h " )) by Def3

      .= ((h * ( 1_ G)) * (h " )) by Def5

      .= (h * (h " )) by Def4

      .= ( 1_ G) by Def5;

      ((g * h) * ((g * h) " )) = ( 1_ G) by Def5;

      hence thesis by A1, Th6;

    end;

    theorem :: GROUP_1:19

    

     Th18: (g * h) = (h * g) iff ((g " ) * (h " )) = ((h " ) * (g " ))

    proof

      thus (g * h) = (h * g) implies ((g " ) * (h " )) = ((h " ) * (g " ))

      proof

        assume

         A1: (g * h) = (h * g);

        

        hence ((g " ) * (h " )) = ((g * h) " ) by Th16

        .= ((h " ) * (g " )) by A1, Th17;

      end;

      assume

       A2: ((g " ) * (h " )) = ((h " ) * (g " ));

      

      thus (g * h) = (((g * h) " ) " )

      .= (((h " ) * (g " )) " ) by Th16

      .= (((h " ) " ) * ((g " ) " )) by A2, Th16

      .= (h * g);

    end;

    theorem :: GROUP_1:20

    

     Th19: (g * h) = (h * g) iff (g * (h " )) = ((h " ) * g)

    proof

      thus (g * h) = (h * g) implies (g * (h " )) = ((h " ) * g)

      proof

        assume

         A1: (g * h) = (h * g);

        ((g * (h " )) * ((g " ) * h)) = (((g * (h " )) * (g " )) * h) by Def3

        .= ((g * ((h " ) * (g " ))) * h) by Def3

        .= ((g * ((g " ) * (h " ))) * h) by A1, Th18

        .= (((g * (g " )) * (h " )) * h) by Def3

        .= ((( 1_ G) * (h " )) * h) by Def5

        .= ((h " ) * h) by Def4

        .= ( 1_ G) by Def5;

        

        then (g * (h " )) = (((g " ) * h) " ) by Th11

        .= ((h " ) * ((g " ) " )) by Th16;

        hence thesis;

      end;

      assume (g * (h " )) = ((h " ) * g);

      then (g * ((h " ) * h)) = (((h " ) * g) * h) by Def3;

      then (g * ( 1_ G)) = (((h " ) * g) * h) by Def5;

      then g = (((h " ) * g) * h) by Def4;

      then g = ((h " ) * (g * h)) by Def3;

      then (h * g) = ((h * (h " )) * (g * h)) by Def3;

      then (h * g) = (( 1_ G) * (g * h)) by Def5;

      hence thesis by Def4;

    end;

    reserve u for UnOp of G;

    definition

      let G;

      :: GROUP_1:def6

      func inverse_op (G) -> UnOp of G means

      : Def6: (it . h) = (h " );

      existence

      proof

        deffunc F( Element of G) = ($1 " );

        consider u such that

         A1: for h be Element of G holds (u . h) = F(h) from FUNCT_2:sch 4;

        take u;

        let h;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let u1,u2 be UnOp of G;

        assume

         A2: for h holds (u1 . h) = (h " );

        assume

         A3: for h holds (u2 . h) = (h " );

        let h be Element of G;

        

        thus (u1 . h) = (h " ) by A2

        .= (u2 . h) by A3;

      end;

    end

    registration

      let G be associative non empty multMagma;

      cluster the multF of G -> associative;

      coherence

      proof

        let h,g,f be Element of G;

        set o = the multF of G;

        

        thus (o . (h,(o . (g,f)))) = (h * (g * f))

        .= ((h * g) * f) by Def3

        .= (o . ((o . (h,g)),f));

      end;

    end

    theorem :: GROUP_1:21

    

     Th20: for G be unital non empty multMagma holds ( 1_ G) is_a_unity_wrt the multF of G

    proof

      let G be unital non empty multMagma;

      set o = the multF of G;

      now

        let h be Element of G;

        

        thus (o . (( 1_ G),h)) = (( 1_ G) * h)

        .= h by Def4;

        

        thus (o . (h,( 1_ G))) = (h * ( 1_ G))

        .= h by Def4;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: GROUP_1:22

    

     Th21: for G be unital non empty multMagma holds ( the_unity_wrt the multF of G) = ( 1_ G)

    proof

      let G be unital non empty multMagma;

      ( 1_ G) is_a_unity_wrt the multF of G by Th20;

      hence thesis by BINOP_1:def 8;

    end;

    registration

      let G be unital non empty multMagma;

      cluster the multF of G -> having_a_unity;

      coherence

      proof

        take ( 1_ G);

        thus thesis by Th20;

      end;

    end

    theorem :: GROUP_1:23

    

     Th22: ( inverse_op G) is_an_inverseOp_wrt the multF of G

    proof

      let h be Element of G;

      

      thus (the multF of G . (h,(( inverse_op G) . h))) = (h * (h " )) by Def6

      .= ( 1_ G) by Def5

      .= ( the_unity_wrt the multF of G) by Th21;

      

      thus (the multF of G . ((( inverse_op G) . h),h)) = ((h " ) * h) by Def6

      .= ( 1_ G) by Def5

      .= ( the_unity_wrt the multF of G) by Th21;

    end;

    registration

      let G;

      cluster the multF of G -> having_an_inverseOp;

      coherence

      proof

        ( inverse_op G) is_an_inverseOp_wrt the multF of G by Th22;

        hence thesis;

      end;

    end

    theorem :: GROUP_1:24

    ( the_inverseOp_wrt the multF of G) = ( inverse_op G)

    proof

      set o = the multF of G;

      o is having_an_inverseOp & ( inverse_op G) is_an_inverseOp_wrt o by Th22;

      hence thesis by FINSEQOP:def 3;

    end;

    definition

      let G be non empty multMagma;

      :: GROUP_1:def7

      func power G -> Function of [:the carrier of G, NAT :], the carrier of G means

      : Def7: for h be Element of G holds (it . (h, 0 )) = ( 1_ G) & for n be Nat holds (it . (h,(n + 1))) = ((it . (h,n)) * h);

      existence

      proof

        defpred P[ object, object] means ex g0 be sequence of the carrier of G, h be Element of G st $1 = h & g0 = $2 & (g0 . 0 ) = ( 1_ G) & for n holds (g0 . (n + 1)) = ((g0 . n) * h);

        

         A1: for x be object st x in the carrier of G holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in the carrier of G;

          then

          reconsider b = x as Element of G;

          deffunc F( Nat, Element of G) = ($2 * b);

          consider g0 be sequence of the carrier of G such that

           A2: (g0 . 0 ) = ( 1_ G) and

           A3: for n be Nat holds (g0 . (n + 1)) = F(n,.) from NAT_1:sch 12;

          reconsider y = g0 as set;

          take y;

          take g0;

          take b;

          thus x = b & g0 = y & (g0 . 0 ) = ( 1_ G) by A2;

          let n;

          thus thesis by A3;

        end;

        consider f be Function such that ( dom f) = the carrier of G and

         A4: for x be object st x in the carrier of G holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        defpred P[ Element of G, Nat, set] means ex g0 be sequence of the carrier of G st g0 = (f . $1) & $3 = (g0 . $2);

        

         A5: for a be Element of G, n be Nat holds ex b be Element of G st P[a, n, b]

        proof

          let a be Element of G, n be Nat;

          consider g0 be sequence of the carrier of G, h be Element of G such that a = h and

           A6: g0 = (f . a) and (g0 . 0 ) = ( 1_ G) and for n holds (g0 . (n + 1)) = ((g0 . n) * h) by A4;

          take (g0 . n), g0;

          thus thesis by A6;

        end;

        consider F be Function of [:the carrier of G, NAT :], the carrier of G such that

         A7: for a be Element of G, n be Nat holds P[a, n, (F . (a,n))] from NAT_1:sch 19( A5);

        take F;

        let h be Element of G;

        

         A8: ex g2 be sequence of the carrier of G, b be Element of G st h = b & g2 = (f . h) & (g2 . 0 ) = ( 1_ G) & for n holds (g2 . (n + 1)) = ((g2 . n) * b) by A4;

        ex g1 be sequence of the carrier of G st g1 = (f . h) & (F . (h, 0 )) = (g1 . 0 ) by A7;

        hence (F . (h, 0 )) = ( 1_ G) by A8;

        let n be Nat;

        

         A9: ex g2 be sequence of the carrier of G, b be Element of G st h = b & g2 = (f . h) & (g2 . 0 ) = ( 1_ G) & for n holds (g2 . (n + 1)) = ((g2 . n) * b) by A4;

        (ex g0 be sequence of the carrier of G st g0 = (f . h) & (F . (h,n)) = (g0 . n)) & ex g1 be sequence of the carrier of G st g1 = (f . h) & (F . (h,(n + 1))) = (g1 . (n + 1)) by A7;

        hence thesis by A9;

      end;

      uniqueness

      proof

        let f,g be Function of [:the carrier of G, NAT :], the carrier of G;

        assume that

         A10: for h be Element of G holds (f . (h, 0 )) = ( 1_ G) & for n be Nat holds (f . (h,(n + 1))) = ((f . (h,n)) * h) and

         A11: for h be Element of G holds (g . (h, 0 )) = ( 1_ G) & for n be Nat holds (g . (h,(n + 1))) = ((g . (h,n)) * h);

        now

          let h be Element of G, n be Element of NAT ;

          defpred P[ Nat] means (f . [h, $1]) = (g . [h, $1]);

           A12:

          now

            let n be Nat;

            assume

             A13: P[n];

            

             A14: (g . [h, n]) = (g . (h,n));

            (f . [h, (n + 1)]) = (f . (h,(n + 1)))

            .= ((f . (h,n)) * h) by A10

            .= (g . (h,(n + 1))) by A11, A13, A14

            .= (g . [h, (n + 1)]);

            hence P[(n + 1)];

          end;

          (f . [h, 0 ]) = (f . (h, 0 ))

          .= ( 1_ G) by A10

          .= (g . (h, 0 )) by A11

          .= (g . [h, 0 ]);

          then

           A15: P[ 0 ];

          for n be Nat holds P[n] from NAT_1:sch 2( A15, A12);

          hence (f . (h,n)) = (g . (h,n));

        end;

        hence thesis;

      end;

    end

    definition

      let G, h;

      let i be Integer;

      :: GROUP_1:def8

      func h |^ i -> Element of G equals

      : Def8: (( power G) . (h, |.i.|)) if 0 <= i

      otherwise ((( power G) . (h, |.i.|)) " );

      correctness ;

    end

    definition

      let G, h;

      let n be natural Number;

      :: original: |^

      redefine

      :: GROUP_1:def9

      func h |^ n equals (( power G) . (h,n));

      compatibility

      proof

        let g be Element of G;

         |.n.| = n by ABSVALUE:def 1;

        hence thesis by Def8;

      end;

    end

    

     Lm2: (h |^ (n + 1)) = ((h |^ n) * h) by Def7;

    

     Lm3: (h |^ 0 ) = ( 1_ G) by Def7;

    

     Lm4: (( 1_ G) |^ n) = ( 1_ G)

    proof

      defpred P[ Nat] means (( 1_ G) |^ $1) = ( 1_ G);

       A1:

      now

        let n;

        assume P[n];

        

        then (( 1_ G) |^ (n + 1)) = (( 1_ G) * ( 1_ G)) by Lm2

        .= ( 1_ G) by Def4;

        hence P[(n + 1)];

      end;

      

       A2: P[ 0 ] by Def7;

      for n holds P[n] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    theorem :: GROUP_1:25

    (h |^ 0 ) = ( 1_ G) by Def7;

    theorem :: GROUP_1:26

    

     Th25: (h |^ 1) = h

    proof

      

      thus (h |^ 1) = (h |^ ( 0 + 1))

      .= ((h |^ 0 ) * h) by Lm2

      .= (( 1_ G) * h) by Def7

      .= h by Def4;

    end;

    theorem :: GROUP_1:27

    

     Th26: (h |^ 2) = (h * h)

    proof

      

      thus (h |^ 2) = (h |^ (1 + 1))

      .= ((h |^ 1) * h) by Lm2

      .= (h * h) by Th25;

    end;

    theorem :: GROUP_1:28

    (h |^ 3) = ((h * h) * h)

    proof

      

      thus (h |^ 3) = (h |^ (2 + 1))

      .= ((h |^ 2) * h) by Lm2

      .= ((h * h) * h) by Th26;

    end;

    theorem :: GROUP_1:29

    (h |^ 2) = ( 1_ G) iff (h " ) = h

    proof

      thus (h |^ 2) = ( 1_ G) implies h = (h " )

      proof

        assume (h |^ 2) = ( 1_ G);

        then (h * h) = ( 1_ G) by Th26;

        hence thesis by Th11;

      end;

      assume h = (h " );

      

      hence (h |^ 2) = (h * (h " )) by Th26

      .= ( 1_ G) by Def5;

    end;

    

     Lm5: (h |^ (n + m)) = ((h |^ n) * (h |^ m))

    proof

      defpred P[ Nat] means for n holds (h |^ (n + $1)) = ((h |^ n) * (h |^ $1));

      

       A1: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        assume

         A2: for n holds (h |^ (n + m)) = ((h |^ n) * (h |^ m));

        let n;

        

        thus (h |^ (n + (m + 1))) = (h |^ ((n + m) + 1))

        .= ((h |^ (n + m)) * h) by Lm2

        .= (((h |^ n) * (h |^ m)) * h) by A2

        .= ((h |^ n) * ((h |^ m) * h)) by Def3

        .= ((h |^ n) * (h |^ (m + 1))) by Lm2;

      end;

      

       A3: P[ 0 ]

      proof

        let n;

        

        thus (h |^ (n + 0 )) = ((h |^ n) * ( 1_ G)) by Def4

        .= ((h |^ n) * (h |^ 0 )) by Def7;

      end;

      for m holds P[m] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    

     Lm6: (h |^ (n + 1)) = ((h |^ n) * h) & (h |^ (n + 1)) = (h * (h |^ n))

    proof

      thus (h |^ (n + 1)) = ((h |^ n) * h) by Lm2;

      

      thus (h |^ (n + 1)) = ((h |^ 1) * (h |^ n)) by Lm5

      .= (h * (h |^ n)) by Th25;

    end;

    

     Lm7: (h |^ (n * m)) = ((h |^ n) |^ m)

    proof

      defpred P[ Nat] means for n holds (h |^ (n * $1)) = ((h |^ n) |^ $1);

      

       A1: for m st P[m] holds P[(m + 1)]

      proof

        let m;

        assume

         A2: for n holds (h |^ (n * m)) = ((h |^ n) |^ m);

        let n;

        

        thus (h |^ (n * (m + 1))) = (h |^ ((n * m) + (n * 1)))

        .= ((h |^ (n * m)) * (h |^ n)) by Lm5

        .= (((h |^ n) |^ m) * (h |^ n)) by A2

        .= (((h |^ n) |^ m) * ((h |^ n) |^ 1)) by Th25

        .= ((h |^ n) |^ (m + 1)) by Lm5;

      end;

      

       A3: P[ 0 ]

      proof

        let n;

        

        thus (h |^ (n * 0 )) = ( 1_ G) by Def7

        .= ((h |^ n) |^ 0 ) by Def7;

      end;

      for m holds P[m] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    

     Lm8: ((h " ) |^ n) = ((h |^ n) " )

    proof

      defpred P[ Nat] means ((h " ) |^ $1) = ((h |^ $1) " );

       A1:

      now

        let n;

        assume P[n];

        

        then ((h " ) |^ (n + 1)) = (((h |^ n) " ) * (h " )) by Lm2

        .= ((h * (h |^ n)) " ) by Th16

        .= ((h |^ (n + 1)) " ) by Lm6;

        hence P[(n + 1)];

      end;

      ((h " ) |^ 0 ) = ( 1_ G) by Def7

      .= (( 1_ G) " ) by Th8

      .= ((h |^ 0 ) " ) by Def7;

      then

       A2: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A2, A1);

      hence thesis;

    end;

    

     Lm9: (g * h) = (h * g) implies (g * (h |^ n)) = ((h |^ n) * g)

    proof

      defpred P[ Nat] means (g * h) = (h * g) implies (g * (h |^ $1)) = ((h |^ $1) * g);

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A2: (g * h) = (h * g) implies (g * (h |^ n)) = ((h |^ n) * g);

        assume

         A3: (g * h) = (h * g);

        

        thus (g * (h |^ (n + 1))) = (g * (h * (h |^ n))) by Lm6

        .= ((g * h) * (h |^ n)) by Def3

        .= (h * ((h |^ n) * g)) by A2, A3, Def3

        .= ((h * (h |^ n)) * g) by Def3

        .= ((h |^ (n + 1)) * g) by Lm6;

      end;

      

       A4: P[ 0 ]

      proof

        assume (g * h) = (h * g);

        

        thus (g * (h |^ 0 )) = (g * ( 1_ G)) by Def7

        .= g by Def4

        .= (( 1_ G) * g) by Def4

        .= ((h |^ 0 ) * g) by Def7;

      end;

      for n holds P[n] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    

     Lm10: (g * h) = (h * g) implies ((g |^ n) * (h |^ m)) = ((h |^ m) * (g |^ n))

    proof

      defpred P[ Nat] means for m st (g * h) = (h * g) holds ((g |^ $1) * (h |^ m)) = ((h |^ m) * (g |^ $1));

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A2: for m st (g * h) = (h * g) holds ((g |^ n) * (h |^ m)) = ((h |^ m) * (g |^ n));

        let m;

        assume

         A3: (g * h) = (h * g);

        

        thus ((g |^ (n + 1)) * (h |^ m)) = ((g * (g |^ n)) * (h |^ m)) by Lm6

        .= (g * ((g |^ n) * (h |^ m))) by Def3

        .= (g * ((h |^ m) * (g |^ n))) by A2, A3

        .= ((g * (h |^ m)) * (g |^ n)) by Def3

        .= (((h |^ m) * g) * (g |^ n)) by A3, Lm9

        .= ((h |^ m) * (g * (g |^ n))) by Def3

        .= ((h |^ m) * (g |^ (n + 1))) by Lm6;

      end;

      

       A4: P[ 0 ]

      proof

        let m;

        assume (g * h) = (h * g);

        

        thus ((g |^ 0 ) * (h |^ m)) = (( 1_ G) * (h |^ m)) by Def7

        .= (h |^ m) by Def4

        .= ((h |^ m) * ( 1_ G)) by Def4

        .= ((h |^ m) * (g |^ 0 )) by Def7;

      end;

      for n holds P[n] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    

     Lm11: (g * h) = (h * g) implies ((g * h) |^ n) = ((g |^ n) * (h |^ n))

    proof

      defpred P[ Nat] means (g * h) = (h * g) implies ((g * h) |^ $1) = ((g |^ $1) * (h |^ $1));

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A2: (g * h) = (h * g) implies ((g * h) |^ n) = ((g |^ n) * (h |^ n));

        assume

         A3: (g * h) = (h * g);

        

        hence ((g * h) |^ (n + 1)) = (((g |^ n) * (h |^ n)) * (h * g)) by A2, Lm6

        .= ((((g |^ n) * (h |^ n)) * h) * g) by Def3

        .= (((g |^ n) * ((h |^ n) * h)) * g) by Def3

        .= (((g |^ n) * (h |^ (n + 1))) * g) by Lm6

        .= (((h |^ (n + 1)) * (g |^ n)) * g) by A3, Lm10

        .= ((h |^ (n + 1)) * ((g |^ n) * g)) by Def3

        .= ((h |^ (n + 1)) * (g |^ (n + 1))) by Lm6

        .= ((g |^ (n + 1)) * (h |^ (n + 1))) by A3, Lm10;

      end;

      

       A4: P[ 0 ]

      proof

        assume (g * h) = (h * g);

        

        thus ((g * h) |^ 0 ) = ( 1_ G) by Def7

        .= (( 1_ G) * ( 1_ G)) by Def4

        .= ((g |^ 0 ) * ( 1_ G)) by Def7

        .= ((g |^ 0 ) * (h |^ 0 )) by Def7;

      end;

      for n holds P[n] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    theorem :: GROUP_1:30

    

     Th29: i <= 0 implies (h |^ i) = ((h |^ |.i.|) " )

    proof

      assume

       A1: i <= 0 ;

      per cases by A1;

        suppose i < 0 ;

        hence thesis by Def8;

      end;

        suppose

         A2: i = 0 ;

        

        hence (h |^ i) = ( 1_ G) by Lm3

        .= (( 1_ G) " ) by Th8

        .= ((h |^ 0 ) " ) by Def7

        .= ((h |^ |.i.|) " ) by A2, ABSVALUE:def 1;

      end;

    end;

    theorem :: GROUP_1:31

    (( 1_ G) |^ i) = ( 1_ G)

    proof

      (( 1_ G) |^ i) = (( 1_ G) |^ |.i.|) or (( 1_ G) |^ i) = ((( 1_ G) |^ |.i.|) " ) & (( 1_ G) " ) = ( 1_ G) by Def8, Th8;

      hence thesis by Lm4;

    end;

    theorem :: GROUP_1:32

    

     Th31: (h |^ ( - 1)) = (h " )

    proof

       |.( - 1).| = ( - ( - 1)) by ABSVALUE:def 1;

      

      hence (h |^ ( - 1)) = ((h |^ 1) " ) by Def8

      .= (h " ) by Th25;

    end;

    

     Lm12: (h |^ ( - i)) = ((h |^ i) " )

    proof

      per cases ;

        suppose

         A1: i >= 0 ;

        per cases by A1, XREAL_1: 24;

          suppose

           A2: ( - i) < ( - 0 );

          

          hence (h |^ ( - i)) = ((h |^ |.( - i).|) " ) by Def8

          .= ((h |^ ( - ( - i))) " ) by A2, ABSVALUE:def 1

          .= ((h |^ i) " );

        end;

          suppose

           A3: i = 0 ;

          

          hence (h |^ ( - i)) = ( 1_ G) by Lm3

          .= (( 1_ G) " ) by Th8

          .= ((h |^ i) " ) by A3, Lm3;

        end;

      end;

        suppose

         A4: i < 0 ;

        then (h |^ i) = ((h |^ |.i.|) " ) by Def8;

        hence thesis by A4, ABSVALUE:def 1;

      end;

    end;

    

     Lm13: j >= 1 or j = 0 or j < 0

    proof

      j < 0 or j is Element of NAT & (j <> 0 or j = 0 ) by INT_1: 3;

      hence thesis by NAT_1: 14;

    end;

    

     Lm14: (h |^ (j - 1)) = ((h |^ j) * (h |^ ( - 1)))

    proof

       A1:

      now

        per cases by Lm13;

          suppose

           A2: j >= 1;

          then j >= (1 + 0 );

          then

           A3: (j - 1) >= 0 by XREAL_1: 19;

          

          then

           A4: ( |.(j - 1).| + 1) = ((j - 1) + 1) by ABSVALUE:def 1

          .= j;

          

           A5: |.j.| = j by A2, ABSVALUE:def 1;

          

           A6: |.j.| = |.( - j).| by COMPLEX1: 52;

          

          thus ((h |^ (j - 1)) * (h * (h |^ ( - j)))) = (((h |^ (j - 1)) * h) * (h |^ ( - j))) by Def3

          .= (((h |^ |.(j - 1).|) * h) * (h |^ ( - j))) by A3, Def8

          .= (((h |^ |.(j - 1).|) * h) * ((h |^ |.( - j).|) " )) by A2, Th29

          .= ((h |^ ( |.(j - 1).| + 1)) * ((h |^ |.( - j).|) " )) by Lm6

          .= ( 1_ G) by A4, A5, A6, Def5;

        end;

          suppose

           A7: j < 0 ;

          

           A8: (1 - j) = ( - (j - 1));

          

          thus ((h |^ (j - 1)) * (h * (h |^ ( - j)))) = (((h |^ |.(j - 1).|) " ) * (h * (h |^ ( - j)))) by A7, Def8

          .= (((h |^ |.(j - 1).|) " ) * (h * (h |^ |.( - j).|))) by A7, Def8

          .= (((h |^ |.(j - 1).|) " ) * (h |^ (1 + |.( - j).|))) by Lm6

          .= (((h |^ |.(j - 1).|) " ) * (h |^ (1 + ( - j)))) by A7, ABSVALUE:def 1

          .= (((h |^ |.(j - 1).|) " ) * (h |^ |.(j - 1).|)) by A7, A8, ABSVALUE:def 1

          .= ( 1_ G) by Def5;

        end;

          suppose

           A9: j = 0 ;

          

          hence ((h |^ (j - 1)) * (h * (h |^ ( - j)))) = ((h " ) * (h * (h |^ ( - j)))) by Th31

          .= (((h " ) * h) * (h |^ ( - j))) by Def3

          .= (( 1_ G) * (h |^ ( - j))) by Def5

          .= (h |^ 0 ) by A9, Def4

          .= ( 1_ G) by Def7;

        end;

      end;

      ((h |^ (j - 1)) * (h |^ (1 - j))) = ((h |^ (j - 1)) * (h |^ ( - (j - 1))))

      .= ((h |^ (j - 1)) * ((h |^ (j - 1)) " )) by Lm12

      .= ( 1_ G) by Def5;

      then (h * (h |^ ( - j))) = (h |^ (1 - j)) by A1, Th6;

      

      then ((h |^ (1 - j)) " ) = (((h |^ ( - j)) " ) * (h " )) by Th16

      .= ((h |^ ( - ( - j))) * (h " )) by Lm12

      .= ((h |^ j) * (h |^ ( - 1))) by Th31;

      then ((h |^ j) * (h |^ ( - 1))) = (h |^ ( - (1 - j))) by Lm12;

      hence thesis;

    end;

    

     Lm15: j >= 0 or j = ( - 1) or j < ( - 1)

    proof

      per cases ;

        suppose j >= 0 ;

        hence thesis;

      end;

        suppose

         A1: j < 0 ;

        then

        reconsider n = ( - j) as Element of NAT by INT_1: 3;

        n <> ( - 0 ) by A1;

        then n >= 1 by NAT_1: 14;

        then n > 1 or n = 1 by XXREAL_0: 1;

        then ( - 1) > ( - ( - j)) or ( - 1) = j by XREAL_1: 24;

        hence thesis;

      end;

    end;

    

     Lm16: (h |^ (j + 1)) = ((h |^ j) * (h |^ 1))

    proof

       A1:

      now

        per cases by Lm15;

          suppose

           A2: j >= 0 ;

          then

          reconsider n = j as Element of NAT by INT_1: 3;

          

           A3: (n + 1) = |.(j + 1).| by ABSVALUE:def 1;

          (n + 1) >= 0 ;

          

          hence ((h |^ (j + 1)) * ((h |^ ( - 1)) * (h |^ ( - j)))) = ((h |^ |.(j + 1).|) * ((h |^ ( - 1)) * (h |^ ( - j)))) by Def8

          .= ((h |^ |.(j + 1).|) * ((h " ) * (h |^ ( - j)))) by Th31

          .= ((h |^ |.(j + 1).|) * ((h " ) * ((h |^ j) " ))) by Lm12

          .= ((h |^ |.(j + 1).|) * ((h " ) * ((h |^ |.j.|) " ))) by A2, Def8

          .= ((h |^ |.(j + 1).|) * (((h |^ |.j.|) * h) " )) by Th16

          .= ((h |^ |.(j + 1).|) * ((h |^ ( |.j.| + 1)) " )) by Lm6

          .= ((h |^ |.(j + 1).|) * ((h |^ |.(j + 1).|) " )) by A3, ABSVALUE:def 1

          .= ( 1_ G) by Def5;

        end;

          suppose j < ( - 1);

          then

           A4: (j + 1) < (( - 1) + 1) by XREAL_1: 6;

          

          hence ((h |^ (j + 1)) * ((h |^ ( - 1)) * (h |^ ( - j)))) = (((h |^ |.(j + 1).|) " ) * ((h |^ ( - 1)) * (h |^ ( - j)))) by Def8

          .= (((h |^ |.(j + 1).|) " ) * ((h " ) * (h |^ ( - j)))) by Th31

          .= ((((h |^ |.(j + 1).|) " ) * (h " )) * (h |^ ( - j))) by Def3

          .= (((h * (h |^ |.(j + 1).|)) " ) * (h |^ ( - j))) by Th16

          .= (((h |^ ( |.(j + 1).| + 1)) " ) * (h |^ ( - j))) by Lm6

          .= (((h |^ (( - (j + 1)) + 1)) " ) * (h |^ ( - j))) by A4, ABSVALUE:def 1

          .= ( 1_ G) by Def5;

        end;

          suppose

           A5: j = ( - 1);

          

          hence ((h |^ (j + 1)) * ((h |^ ( - 1)) * (h |^ ( - j)))) = (( 1_ G) * ((h |^ ( - 1)) * (h |^ ( - j)))) by Lm3

          .= ((h |^ ( - 1)) * (h |^ ( - j))) by Def4

          .= ((h " ) * (h |^ ( - j))) by Th31

          .= ((h " ) * ((h |^ j) " )) by Lm12

          .= ((h " ) * ((h " ) " )) by A5, Th31

          .= ( 1_ G) by Def5;

        end;

      end;

      ((h |^ (j + 1)) * (h |^ ( - (j + 1)))) = ((h |^ (j + 1)) * ((h |^ (j + 1)) " )) by Lm12

      .= ( 1_ G) by Def5;

      then

       A6: (h |^ ( - (j + 1))) = ((h |^ ( - 1)) * (h |^ ( - j))) by A1, Th6;

      

      thus (h |^ (j + 1)) = (h |^ ( - ( - (j + 1))))

      .= (((h |^ ( - 1)) * (h |^ ( - j))) " ) by A6, Lm12

      .= (((h |^ ( - j)) " ) * ((h |^ ( - 1)) " )) by Th16

      .= ((h |^ ( - ( - j))) * ((h |^ ( - 1)) " )) by Lm12

      .= ((h |^ j) * (h |^ ( - ( - 1)))) by Lm12

      .= ((h |^ j) * (h |^ 1));

    end;

    theorem :: GROUP_1:33

    

     Th32: (h |^ (i + j)) = ((h |^ i) * (h |^ j))

    proof

      defpred P[ Integer] means for i holds (h |^ (i + $1)) = ((h |^ i) * (h |^ $1));

      

       A1: for j holds P[j] implies P[(j - 1)] & P[(j + 1)]

      proof

        let j;

        assume

         A2: for i holds (h |^ (i + j)) = ((h |^ i) * (h |^ j));

        thus for i holds (h |^ (i + (j - 1))) = ((h |^ i) * (h |^ (j - 1)))

        proof

          let i;

          

          thus (h |^ (i + (j - 1))) = (h |^ ((i - 1) + j))

          .= ((h |^ (i - 1)) * (h |^ j)) by A2

          .= (((h |^ i) * (h |^ ( - 1))) * (h |^ j)) by Lm14

          .= ((h |^ i) * ((h |^ ( - 1)) * (h |^ j))) by Def3

          .= ((h |^ i) * (h |^ (j + ( - 1)))) by A2

          .= ((h |^ i) * (h |^ (j - 1)));

        end;

        let i;

        

        thus (h |^ (i + (j + 1))) = (h |^ ((i + 1) + j))

        .= ((h |^ (i + 1)) * (h |^ j)) by A2

        .= (((h |^ i) * (h |^ 1)) * (h |^ j)) by Lm16

        .= ((h |^ i) * ((h |^ 1) * (h |^ j))) by Def3

        .= ((h |^ i) * (h |^ (j + 1))) by A2;

      end;

      

       A3: P[ 0 ]

      proof

        let i;

        

        thus (h |^ (i + 0 )) = ((h |^ i) * ( 1_ G)) by Def4

        .= ((h |^ i) * (h |^ 0 )) by Def7;

      end;

      for j holds P[j] from INT_1:sch 4( A3, A1);

      hence thesis;

    end;

    theorem :: GROUP_1:34

    (h |^ (i + 1)) = ((h |^ i) * h) & (h |^ (i + 1)) = (h * (h |^ i))

    proof

      (h |^ 1) = h by Th25;

      hence thesis by Th32;

    end;

    

     Lm17: ((h " ) |^ i) = ((h |^ i) " )

    proof

      per cases ;

        suppose i >= 0 ;

        then

        reconsider n = i as Element of NAT by INT_1: 3;

        

        thus ((h " ) |^ i) = ((h |^ n) " ) by Lm8

        .= ((h |^ i) " );

      end;

        suppose

         A1: i < 0 ;

        

        hence ((h " ) |^ i) = (((h " ) |^ |.i.|) " ) by Def8

        .= (((h |^ |.i.|) " ) " ) by Lm8

        .= ((h |^ i) " ) by A1, Def8;

      end;

    end;

    theorem :: GROUP_1:35

    (h |^ (i * j)) = ((h |^ i) |^ j)

    proof

      per cases ;

        suppose i >= 0 & j >= 0 ;

        then

        reconsider m = i, n = j as Element of NAT by INT_1: 3;

        

        thus (h |^ (i * j)) = ((h |^ m) |^ n) by Lm7

        .= ((h |^ i) |^ j);

      end;

        suppose i >= 0 & j < 0 ;

        then

        reconsider m = i, n = ( - j) as Element of NAT by INT_1: 3;

        (i * j) = ( - (i * n));

        

        hence (h |^ (i * j)) = ((h |^ (i * n)) " ) by Lm12

        .= ((h " ) |^ (i * n)) by Lm17

        .= (((h " ) |^ m) |^ n) by Lm7

        .= (((h |^ i) " ) |^ n) by Lm17

        .= ((((h |^ i) " ) |^ j) " ) by Lm12

        .= ((((h |^ i) |^ j) " ) " ) by Lm17

        .= ((h |^ i) |^ j);

      end;

        suppose i < 0 & j >= 0 ;

        then

        reconsider m = ( - i), n = j as Element of NAT by INT_1: 3;

        (i * j) = ( - (m * j));

        

        hence (h |^ (i * j)) = ((h |^ (m * j)) " ) by Lm12

        .= ((h " ) |^ (m * j)) by Lm17

        .= (((h " ) |^ m) |^ n) by Lm7

        .= ((((h " ) |^ i) " ) |^ n) by Lm12

        .= ((((h |^ i) " ) " ) |^ j) by Lm17

        .= ((h |^ i) |^ j);

      end;

        suppose j < 0 & i < 0 ;

        then

        reconsider m = ( - i), n = ( - j) as Element of NAT by INT_1: 3;

        ((i * j) * (( - 1) * ( - 1))) = (m * n);

        

        hence (h |^ (i * j)) = ((h |^ m) |^ n) by Lm7

        .= (((h |^ ( - i)) |^ j) " ) by Lm12

        .= ((((h |^ i) " ) |^ j) " ) by Lm12

        .= ((((h " ) |^ i) |^ j) " ) by Lm17

        .= ((((h " ) |^ i) " ) |^ j) by Lm17

        .= ((((h " ) " ) |^ i) |^ j) by Lm17

        .= ((h |^ i) |^ j);

      end;

    end;

    theorem :: GROUP_1:36

    (h |^ ( - i)) = ((h |^ i) " ) by Lm12;

    theorem :: GROUP_1:37

    ((h " ) |^ i) = ((h |^ i) " ) by Lm17;

    theorem :: GROUP_1:38

    

     Th37: (g * h) = (h * g) implies ((g * h) |^ i) = ((g |^ i) * (h |^ i))

    proof

      assume

       A1: (g * h) = (h * g);

      per cases ;

        suppose

         A2: i >= 0 ;

        then

         A3: (h |^ i) = (h |^ |.i.|) by Def8;

        ((g * h) |^ i) = ((g * h) |^ |.i.|) & (g |^ i) = (g |^ |.i.|) by A2, Def8;

        hence thesis by A1, A3, Lm11;

      end;

        suppose

         A4: i < 0 ;

        

        hence ((g * h) |^ i) = (((h * g) |^ |.i.|) " ) by A1, Def8

        .= (((h |^ |.i.|) * (g |^ |.i.|)) " ) by A1, Lm11

        .= (((g |^ |.i.|) " ) * ((h |^ |.i.|) " )) by Th16

        .= ((g |^ i) * ((h |^ |.i.|) " )) by A4, Def8

        .= ((g |^ i) * (h |^ i)) by A4, Def8;

      end;

    end;

    theorem :: GROUP_1:39

    

     Th38: (g * h) = (h * g) implies ((g |^ i) * (h |^ j)) = ((h |^ j) * (g |^ i))

    proof

      assume

       A1: (g * h) = (h * g);

      per cases ;

        suppose i >= 0 & j >= 0 ;

        then (g |^ i) = (g |^ |.i.|) & (h |^ j) = (h |^ |.j.|) by Def8;

        hence thesis by A1, Lm10;

      end;

        suppose

         A2: i >= 0 & j < 0 ;

        

         A3: ((g |^ |.i.|) * (h |^ |.j.|)) = ((h |^ |.j.|) * (g |^ |.i.|)) by A1, Lm10;

        (g |^ i) = (g |^ |.i.|) & (h |^ j) = ((h |^ |.j.|) " ) by A2, Def8;

        hence thesis by A3, Th19;

      end;

        suppose

         A4: i < 0 & j >= 0 ;

        

         A5: ((g |^ |.i.|) * (h |^ |.j.|)) = ((h |^ |.j.|) * (g |^ |.i.|)) by A1, Lm10;

        (g |^ i) = ((g |^ |.i.|) " ) & (h |^ j) = (h |^ |.j.|) by A4, Def8;

        hence thesis by A5, Th19;

      end;

        suppose i < 0 & j < 0 ;

        then

         A6: (g |^ i) = ((g |^ |.i.|) " ) & (h |^ j) = ((h |^ |.j.|) " ) by Def8;

        

        hence ((g |^ i) * (h |^ j)) = (((h |^ |.j.|) * (g |^ |.i.|)) " ) by Th16

        .= (((g |^ |.i.|) * (h |^ |.j.|)) " ) by A1, Lm10

        .= ((h |^ j) * (g |^ i)) by A6, Th16;

      end;

    end;

    theorem :: GROUP_1:40

    (g * h) = (h * g) implies (g * (h |^ i)) = ((h |^ i) * g)

    proof

      assume

       A1: (g * h) = (h * g);

      

      thus (g * (h |^ i)) = ((g |^ 1) * (h |^ i)) by Th25

      .= ((h |^ i) * (g |^ 1)) by A1, Th38

      .= ((h |^ i) * g) by Th25;

    end;

    definition

      let G, h;

      :: GROUP_1:def10

      attr h is being_of_order_0 means (h |^ n) = ( 1_ G) implies n = 0 ;

    end

    registration

      let G;

      cluster ( 1_ G) -> non being_of_order_0;

      coherence

      proof

        (( 1_ G) |^ 8) = ( 1_ G) by Lm4;

        hence thesis;

      end;

    end

    definition

      let G, h;

      :: GROUP_1:def11

      func ord h -> Element of NAT means

      : Def11: it = 0 if h is being_of_order_0

      otherwise (h |^ it ) = ( 1_ G) & it <> 0 & for m st (h |^ m) = ( 1_ G) & m <> 0 holds it <= m;

      existence

      proof

        defpred P[ Nat] means (h |^ $1) = ( 1_ G) & $1 <> 0 ;

        thus h is being_of_order_0 implies ex n be Element of NAT st n = 0 ;

        hereby

          assume not h is being_of_order_0;

          then

           A1: ex n be Nat st P[n];

          consider k be Nat such that

           A2: P[k] and

           A3: for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A1);

          reconsider k as Element of NAT by ORDINAL1:def 12;

          take k;

          thus (h |^ k) = ( 1_ G) & k <> 0 by A2;

          let m;

          assume (h |^ m) = ( 1_ G) & m <> 0 ;

          hence k <= m by A3;

        end;

      end;

      uniqueness

      proof

        let n1,n2 be Element of NAT ;

        thus h is being_of_order_0 & n1 = 0 & n2 = 0 implies n1 = n2;

        assume that not h is being_of_order_0 and

         A4: (h |^ n1) = ( 1_ G) & n1 <> 0 & (for m st (h |^ m) = ( 1_ G) & m <> 0 holds n1 <= m) & (h |^ n2) = ( 1_ G) & (n2 <> 0 & for m st (h |^ m) = ( 1_ G) & m <> 0 holds n2 <= m);

        n1 <= n2 & n2 <= n1 by A4;

        hence thesis by XXREAL_0: 1;

      end;

      correctness ;

    end

    theorem :: GROUP_1:41

    

     Th40: (h |^ ( ord h)) = ( 1_ G)

    proof

      per cases ;

        suppose h is being_of_order_0;

        then ( ord h) = 0 by Def11;

        hence thesis by Def7;

      end;

        suppose not h is being_of_order_0;

        hence thesis by Def11;

      end;

    end;

    theorem :: GROUP_1:42

    ( ord ( 1_ G)) = 1

    proof

      

       A1: for n st (( 1_ G) |^ n) = ( 1_ G) & n <> 0 holds 1 <= n by NAT_1: 14;

      ( not ( 1_ G) is being_of_order_0) & (( 1_ G) |^ 1) = ( 1_ G) by Lm4;

      hence thesis by A1, Def11;

    end;

    theorem :: GROUP_1:43

    ( ord h) = 1 implies h = ( 1_ G)

    proof

      assume

       A1: ( ord h) = 1;

      then not h is being_of_order_0 by Def11;

      then (h |^ 1) = ( 1_ G) by A1, Def11;

      hence thesis by Th25;

    end;

    theorem :: GROUP_1:44

    (h |^ n) = ( 1_ G) implies ( ord h) divides n

    proof

      defpred P[ Nat] means (h |^ $1) = ( 1_ G) implies ( ord h) divides $1;

      

       A1: for n be Nat st for k be Nat st k < n holds P[k] holds P[n]

      proof

        let n be Nat;

        assume

         A2: for k be Nat st k < n holds P[k];

        assume

         A3: (h |^ n) = ( 1_ G);

        per cases ;

          suppose n = 0 ;

          hence thesis by NAT_D: 6;

        end;

          suppose

           A4: n <> 0 ;

          per cases ;

            suppose ( ord h) = 0 ;

            then h is being_of_order_0 by Def11;

            hence thesis by A3, A4;

          end;

            suppose

             A5: ( ord h) <> 0 ;

            then not h is being_of_order_0 by Def11;

            then ( ord h) <= n by A3, A4, Def11;

            then

            consider m be Nat such that

             A6: n = (( ord h) + m) by NAT_1: 10;

            (h |^ n) = ((h |^ ( ord h)) * (h |^ m)) by A6, Lm5

            .= (( 1_ G) * (h |^ m)) by Th40

            .= (h |^ m) by Def4;

            then ( ord h) divides m by A2, A3, A5, A6, NAT_1: 16;

            then

            consider i be Nat such that

             A7: m = (( ord h) * i) by NAT_D:def 3;

            n = (( ord h) * (1 + i)) by A6, A7;

            hence thesis by NAT_D:def 3;

          end;

        end;

      end;

      for n be Nat holds P[n] from NAT_1:sch 4( A1);

      hence thesis;

    end;

    definition

      let G be finite 1-sorted;

      :: original: card

      redefine

      func card G -> Element of NAT ;

      coherence

      proof

        ( card the carrier of G) in NAT ;

        hence thesis;

      end;

    end

    theorem :: GROUP_1:45

    for G be non empty finite 1-sorted holds ( card G) >= 1

    proof

      let G be non empty finite 1-sorted;

      set g = the Element of G;

       {g} c= the carrier of G & ( card {g}) = 1 by CARD_1: 30, ZFMISC_1: 31;

      hence thesis by NAT_1: 43;

    end;

    definition

      let IT be multMagma;

      :: GROUP_1:def12

      attr IT is commutative means

      : Def12: for x,y be Element of IT holds (x * y) = (y * x);

    end

    registration

      cluster strict commutative for Group;

      existence

      proof

        reconsider G0 = multMagma (# REAL , addreal #) as Group by Th3;

        take G0;

        thus G0 is strict;

        let a,g be Element of G0;

        reconsider A = a, B = g as Real;

        

        thus (a * g) = (B + A) by BINOP_2:def 9

        .= (g * a) by BINOP_2:def 9;

      end;

    end

    definition

      let FS be commutative non empty multMagma;

      let x,y be Element of FS;

      :: original: *

      redefine

      func x * y;

      commutativity by Def12;

    end

    theorem :: GROUP_1:46

     multMagma (# REAL , addreal #) is commutative Group

    proof

      reconsider G = multMagma (# REAL , addreal #) as Group by Th3;

      G is commutative

      proof

        let h,g be Element of G;

        reconsider A = h, B = g as Real;

        

        thus (h * g) = (B + A) by BINOP_2:def 9

        .= (g * h) by BINOP_2:def 9;

      end;

      hence thesis;

    end;

    reserve A for commutative Group;

    reserve a,b for Element of A;

    theorem :: GROUP_1:47

    ((a * b) " ) = ((a " ) * (b " )) by Th16;

    theorem :: GROUP_1:48

    ((a * b) |^ i) = ((a |^ i) * (b |^ i)) by Th37;

    theorem :: GROUP_1:49

     addLoopStr (# the carrier of A, the multF of A, ( 1_ A) #) is Abelian add-associative right_zeroed right_complementable

    proof

      set G = addLoopStr (# the carrier of A, the multF of A, ( 1_ A) #);

      thus G is Abelian

      proof

        let a,b be Element of G;

        reconsider x = a, y = b as Element of A;

        

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

        

        thus (a + b) = (x * y)

        .= (b + a) by A1;

      end;

      hereby

        let a,b,c be Element of G;

        reconsider x = a, y = b, z = c as Element of A;

        

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

        .= (x * (y * z)) by Def3

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

      end;

      hereby

        let a be Element of G;

        reconsider x = a as Element of A;

        

        thus (a + ( 0. G)) = (x * ( 1_ A))

        .= a by Def4;

      end;

      let a be Element of G;

      reconsider x = a as Element of A;

      reconsider b = (( inverse_op A) . x) as Element of G;

      take b;

      

      thus (a + b) = (x * (x " )) by Def6

      .= ( 0. G) by Def5;

    end;

    begin

    theorem :: GROUP_1:50

    

     Th49: for L be unital non empty multMagma holds for x be Element of L holds (( power L) . (x,1)) = x

    proof

      let L be unital non empty multMagma;

      let x be Element of L;

      ( 0 + 1) = 1;

      

      hence (( power L) . (x,1)) = ((( power L) . (x, 0 )) * x) by Def7

      .= (( 1_ L) * x) by Def7

      .= x by Def4;

    end;

    theorem :: GROUP_1:51

    for L be unital non empty multMagma holds for x be Element of L holds (( power L) . (x,2)) = (x * x)

    proof

      let L be unital non empty multMagma;

      let x be Element of L;

      (1 + 1) = 2;

      

      hence (( power L) . (x,2)) = ((( power L) . (x,1)) * x) by Def7

      .= (x * x) by Th49;

    end;

    theorem :: GROUP_1:52

    for L be associative commutative unital non empty multMagma holds for x,y be Element of L holds for n be Nat holds (( power L) . ((x * y),n)) = ((( power L) . (x,n)) * (( power L) . (y,n)))

    proof

      let L be associative commutative unital non empty multMagma;

      let x,y be Element of L;

      defpred P[ Nat] means (( power L) . ((x * y),$1)) = ((( power L) . (x,$1)) * (( power L) . (y,$1)));

       A1:

      now

        let n be Nat;

        assume P[n];

        

        then (( power L) . ((x * y),(n + 1))) = (((( power L) . (x,n)) * (( power L) . (y,n))) * (x * y)) by Def7

        .= ((( power L) . (x,n)) * ((( power L) . (y,n)) * (x * y))) by Def3

        .= ((( power L) . (x,n)) * (x * ((( power L) . (y,n)) * y))) by Def3

        .= ((( power L) . (x,n)) * (x * (( power L) . (y,(n + 1))))) by Def7

        .= (((( power L) . (x,n)) * x) * (( power L) . (y,(n + 1)))) by Def3

        .= ((( power L) . (x,(n + 1))) * (( power L) . (y,(n + 1)))) by Def7;

        hence P[(n + 1)];

      end;

      (( power L) . ((x * y), 0 )) = ( 1_ L) by Def7

      .= (( 1_ L) * ( 1_ L)) by Def4

      .= ((( power L) . (x, 0 )) * ( 1_ L)) by Def7

      .= ((( power L) . (x, 0 )) * (( power L) . (y, 0 ))) by Def7;

      then

       A2: P[ 0 ];

      thus for n be Nat holds P[n] from NAT_1:sch 2( A2, A1);

    end;

    definition

      let G,H be multMagma;

      let IT be Function of G, H;

      :: GROUP_1:def13

      attr IT is unity-preserving means (IT . ( 1_ G)) = ( 1_ H);

    end