bcialg_6.miz



    begin

    reserve X for BCI-algebra;

    reserve n for Nat;

    definition

      let G be non empty BCIStr_0;

      :: BCIALG_6:def1

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

      : Def1: for x be Element of G holds (it . (x, 0 )) = ( 0. G) & for n holds (it . (x,(n + 1))) = (x \ ((it . (x,n)) ` ));

      existence

      proof

        defpred P[ object, object] means ex f be sequence of the carrier of G, x be Element of G st $1 = x & f = $2 & (f . 0 ) = ( 0. G) & for n holds (f . (n + 1)) = (x \ ((f . n) ` ));

        

         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 Ff( Nat, Element of G) = (b \ ($2 ` ));

          consider g0 be sequence of the carrier of G such that

           A2: (g0 . 0 ) = ( 0. G) & for n be Nat holds (g0 . (n + 1)) = Ff(n,.) from NAT_1:sch 12;

          reconsider y = g0 as set;

          take y, g0, b;

          thus thesis by A2;

        end;

        consider f be Function such that

         A3: ( dom f) = the carrier of G & 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);

        

         A4: 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

           A5: g0 = (f . a) and (g0 . 0 ) = ( 0. G) and for n holds (g0 . (n + 1)) = (h \ ((g0 . n) ` )) by A3;

          take (g0 . n), g0;

          thus thesis by A5;

        end;

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

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

        take F;

        let h be Element of G;

        

         A7: ex g2 be sequence of the carrier of G, b be Element of G st h = b & g2 = (f . h) & (g2 . 0 ) = ( 0. G) & for n holds (g2 . (n + 1)) = (b \ ((g2 . n) ` )) by A3;

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

        hence (F . (h, 0 )) = ( 0. G) by A7;

        let n;

        

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

        (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 A6;

        hence thesis by A8;

      end;

      uniqueness

      proof

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

        assume that

         A9: for h be Element of G holds (f . (h, 0 )) = ( 0. G) & for n holds (f . (h,(n + 1))) = (h \ ((f . (h,n)) ` )) and

         A10: for h be Element of G holds (g . (h, 0 )) = ( 0. G) & for n holds (g . (h,(n + 1))) = (h \ ((g . (h,n)) ` ));

        now

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

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

           A11:

          now

            let n;

            assume

             A12: P[n];

            

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

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

            .= (h \ ((f . (h,n)) ` )) by A9

            .= (g . (h,(n + 1))) by A10, A12, A13

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

            hence P[(n + 1)];

          end;

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

          .= ( 0. G) by A9

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

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

          then

           A14: P[ 0 ];

          for n holds P[n] from NAT_1:sch 2( A14, A11);

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

        end;

        hence thesis;

      end;

    end

    reserve x,y for Element of X;

    reserve a,b for Element of ( AtomSet X);

    reserve m,n for Nat;

    reserve i,j for Integer;

    definition

      let X, x;

      let i be Integer;

      :: BCIALG_6:def2

      func x |^ i -> Element of X equals

      : Def2: (( BCI-power X) . (x, |.i.|)) if 0 <= i

      otherwise (( BCI-power X) . ((x ` ), |.i.|));

      correctness ;

    end

    definition

      let X, x;

      let n be natural Number;

      :: original: |^

      redefine

      :: BCIALG_6:def3

      func x |^ n equals (( BCI-power X) . (x,n));

      compatibility

      proof

        let g be Element of X;

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

        hence thesis by Def2;

      end;

    end

    theorem :: BCIALG_6:1

    

     Th1: (a \ (x \ b)) = (b \ (x \ a))

    proof

      b in ( AtomSet X);

      then

       A1: ex y1 be Element of X st b = y1 & y1 is atom;

      ((x \ (x \ b)) \ b) = ( 0. X) by BCIALG_1: 1;

      then ((b \ (x \ a)) \ (a \ (x \ b))) = (((x \ (x \ b)) \ (x \ a)) \ (a \ (x \ b))) by A1;

      then ((b \ (x \ a)) \ (a \ (x \ b))) = (((x \ (x \ a)) \ (x \ b)) \ (a \ (x \ b))) by BCIALG_1: 7;

      then ((b \ (x \ a)) \ (a \ (x \ b))) = ((((x \ (x \ a)) \ (x \ b)) \ (a \ (x \ b))) \ ( 0. X)) by BCIALG_1: 2;

      then ((b \ (x \ a)) \ (a \ (x \ b))) = ((((x \ (x \ a)) \ (x \ b)) \ (a \ (x \ b))) \ ((x \ (x \ a)) \ a)) by BCIALG_1: 1;

      then

       A2: ((b \ (x \ a)) \ (a \ (x \ b))) = ( 0. X) by BCIALG_1:def 3;

      (a \ (x \ b)) <= (b \ (x \ a)) by BCIALG_1: 26;

      then ((a \ (x \ b)) \ (b \ (x \ a))) = ( 0. X);

      hence thesis by A2, BCIALG_1:def 7;

    end;

    theorem :: BCIALG_6:2

    

     Th2: (x |^ (n + 1)) = (x \ ((x |^ n) ` )) by Def1;

    theorem :: BCIALG_6:3

    

     Th3: (x |^ 0 ) = ( 0. X) by Def1;

    theorem :: BCIALG_6:4

    

     Th4: (x |^ 1) = x

    proof

      (x |^ 1) = (x |^ ( 0 + 1))

      .= (x \ ((x |^ 0 ) ` )) by Def1

      .= (x \ (( 0. X) ` )) by Def1

      .= (x \ ( 0. X)) by BCIALG_1:def 5;

      hence thesis by BCIALG_1: 2;

    end;

    theorem :: BCIALG_6:5

    

     Th5: (x |^ ( - 1)) = (x ` )

    proof

      (x |^ ( - 1)) = (( BCI-power X) . ((x ` ), |.( - 1).|)) by Def2;

      then (x |^ ( - 1)) = (( BCI-power X) . ((x ` ),( - ( - 1)))) by ABSVALUE:def 1;

      then (x |^ ( - 1)) = ((x ` ) |^ 1);

      hence thesis by Th4;

    end;

    theorem :: BCIALG_6:6

    (x |^ 2) = (x \ (x ` ))

    proof

      (x |^ 2) = (x |^ (1 + 1))

      .= (x \ ((x |^ 1) ` )) by Def1;

      hence thesis by Th4;

    end;

    theorem :: BCIALG_6:7

    

     Th7: (( 0. X) |^ n) = ( 0. X)

    proof

      defpred P[ Nat] means (( 0. X) |^ $1) = ( 0. X);

       A1:

      now

        let n;

        assume P[n];

        

        then (( 0. X) |^ (n + 1)) = ((( 0. X) ` ) ` ) by Th2

        .= (( 0. X) ` ) by BCIALG_1:def 5

        .= ( 0. X) by BCIALG_1:def 5;

        hence P[(n + 1)];

      end;

      

       A2: P[ 0 ] by Def1;

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

      hence thesis;

    end;

    theorem :: BCIALG_6:8

    ((a |^ ( - 1)) |^ ( - 1)) = a

    proof

      ((a |^ ( - 1)) |^ ( - 1)) = ((a ` ) |^ ( - 1)) by Th5

      .= ((a ` ) ` ) by Th5;

      hence thesis by BCIALG_1: 29;

    end;

    theorem :: BCIALG_6:9

    (x |^ ( - n)) = (((x ` ) ` ) |^ ( - n))

    proof

      defpred P[ Nat] means (x |^ ( - $1)) = (((x ` ) ` ) |^ ( - $1));

       A1:

      now

        let n;

        assume P[n];

        set m = ( - (n + 1));

        (x |^ m) = (( BCI-power X) . ((x ` ), |.m.|)) by Def2

        .= (( BCI-power X) . ((((x ` ) ` ) ` ), |.m.|)) by BCIALG_1: 8

        .= (((x ` ) ` ) |^ ( - (n + 1))) by Def2;

        hence P[(n + 1)];

      end;

      (x |^ 0 ) = ( 0. X) by Def1

      .= (((x ` ) ` ) |^ 0 ) by Def1;

      then

       A2: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BCIALG_6:10

    

     Th10: ((a ` ) |^ n) = (a |^ ( - n))

    proof

      per cases ;

        suppose

         A1: n = 0 ;

        

        hence ((a ` ) |^ n) = ( 0. X) by Def1

        .= (a |^ ( - n)) by A1, Th3;

      end;

        suppose

         A2: n > 0 ;

        set m = ( - n);

        ( - ( - n)) > 0 by A2;

        then

         A3: m < 0 ;

        

        then (a |^ m) = (( BCI-power X) . ((a ` ), |.m.|)) by Def2

        .= (( BCI-power X) . ((a ` ),( - ( - n)))) by A3, ABSVALUE:def 1;

        hence thesis;

      end;

    end;

    theorem :: BCIALG_6:11

    x in ( BCK-part X) & n >= 1 implies (x |^ n) = x

    proof

      assume that

       A1: x in ( BCK-part X) and

       A2: n >= 1;

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

      

       A3: ex y be Element of X st y = x & ( 0. X) <= y by A1;

       A4:

      now

        let n;

        assume n >= 1;

        assume P[n];

        

        then (x |^ (n + 1)) = (x \ (x ` )) by Th2

        .= (x \ ( 0. X)) by A3

        .= x by BCIALG_1: 2;

        hence P[(n + 1)];

      end;

      

       A5: P[1] by Th4;

      for n st n >= 1 holds P[n] from NAT_1:sch 8( A5, A4);

      hence thesis by A2;

    end;

    theorem :: BCIALG_6:12

    x in ( BCK-part X) implies (x |^ ( - n)) = ( 0. X)

    proof

      defpred P[ Nat] means (x |^ ( - $1)) = ( 0. X);

      assume x in ( BCK-part X);

      then

       A1: ex y be Element of X st y = x & ( 0. X) <= y;

       A2:

      now

        let n;

        assume

         A3: P[n];

        per cases ;

          suppose ( - n) = 0 ;

          

          then (x |^ ( - (n + 1))) = (x ` ) by Th5

          .= ( 0. X) by A1;

          hence P[(n + 1)];

        end;

          suppose

           A4: ( - n) < 0 ;

          then (( BCI-power X) . ((x ` ), |.( - n).|)) = ( 0. X) by A3, Def2;

          then (( BCI-power X) . ((x ` ),( - ( - n)))) = ( 0. X) by A4, ABSVALUE:def 1;

          

          then ((x ` ) \ (((x ` ) |^ n) ` )) = ((x \ ( 0. X)) ` ) by BCIALG_1: 9

          .= (x ` ) by BCIALG_1: 2;

          then ((x ` ) \ (((x ` ) |^ n) ` )) = ( 0. X) by A1;

          

          then ( 0. X) = ((x ` ) |^ (n + 1)) by Th2

          .= (( BCI-power X) . ((x ` ),( - ( - (n + 1)))))

          .= (( BCI-power X) . ((x ` ), |.( - (n + 1)).|)) by ABSVALUE:def 1

          .= (x |^ ( - (n + 1))) by Def2;

          hence P[(n + 1)];

        end;

      end;

      (x |^ ( - 0 )) = (x |^ 0 )

      .= ( 0. X) by Def1;

      then

       A5: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BCIALG_6:13

    

     Th13: (a |^ i) in ( AtomSet X)

    proof

      defpred P[ Integer] means (a |^ $1) in ( AtomSet X);

      ( 0. X) in ( AtomSet X);

      then

       A1: P[ 0 ] by Def1;

      per cases ;

        suppose

         A2: i >= 0 ;

        

         A3: for i2 be Integer st i2 >= 0 holds P[i2] implies P[(i2 + 1)]

        proof

          let i2 be Integer;

          assume i2 >= 0 ;

          then

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

          (((a |^ (j + 1)) ` ) ` ) = (((a \ ((a |^ j) ` )) ` ) ` ) by Def1;

          then (((a |^ (j + 1)) ` ) ` ) = (((a ` ) \ (((a |^ j) ` ) ` )) ` ) by BCIALG_1: 9;

          then (((a |^ (j + 1)) ` ) ` ) = (((a ` ) ` ) \ ((((a |^ j) ` ) ` ) ` )) by BCIALG_1: 9;

          then

           A4: (((a |^ (j + 1)) ` ) ` ) = (a \ ((((a |^ j) ` ) ` ) ` )) by BCIALG_1: 29;

          assume P[i2];

          then (((a |^ (j + 1)) ` ) ` ) = (a \ ((a |^ j) ` )) by A4, BCIALG_1: 29;

          then (((a |^ (j + 1)) ` ) ` ) = (a |^ (j + 1)) by Def1;

          hence thesis by BCIALG_1: 29;

        end;

        for i st i >= 0 holds P[i] from INT_1:sch 2( A1, A3);

        hence thesis by A2;

      end;

        suppose

         A5: i <= 0 ;

        

         A6: for i2 be Integer st i2 <= 0 holds P[i2] implies P[(i2 - 1)]

        proof

          let i2 be Integer;

          assume

           A7: i2 <= 0 ;

          assume

           A8: P[i2];

          per cases by A7;

            suppose

             A9: i2 = 0 ;

            (((a ` ) ` ) ` ) = (a ` ) by BCIALG_1: 8;

            then (a ` ) in ( AtomSet X) by BCIALG_1: 29;

            hence thesis by A9, Th5;

          end;

            suppose

             A10: i2 < 0 ;

            set j = i2;

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

            (a |^ (j - 1)) = (( BCI-power X) . ((a ` ), |.(j - 1).|)) by A10, Def2;

            then (a |^ (j - 1)) = (( BCI-power X) . ((a ` ),( - (j - 1)))) by A10, ABSVALUE:def 1;

            then (a |^ (j - 1)) = ((a ` ) |^ (m + 1));

            then (a |^ (j - 1)) = ((a ` ) \ (((a ` ) |^ m) ` )) by Def1;

            then (a |^ (j - 1)) = ((a ` ) \ ((a |^ ( - ( - j))) ` )) by Th10;

            then (((a |^ (j - 1)) ` ) ` ) = ((((a ` ) ` ) \ (((a |^ j) ` ) ` )) ` ) by BCIALG_1: 9;

            then (((a |^ (j - 1)) ` ) ` ) = ((a \ (((a |^ j) ` ) ` )) ` ) by BCIALG_1: 29;

            then (((a |^ (j - 1)) ` ) ` ) = ((a \ (a |^ j)) ` ) by A8, BCIALG_1: 29;

            then (((a |^ (j - 1)) ` ) ` ) = ((a ` ) \ ((a |^ ( - m)) ` )) by BCIALG_1: 9;

            then (((a |^ (j - 1)) ` ) ` ) = ((a ` ) \ (((a ` ) |^ m) ` )) by Th10;

            then (((a |^ (j - 1)) ` ) ` ) = ((a ` ) |^ (m + 1)) by Def1;

            then (((a |^ (j - 1)) ` ) ` ) = (( BCI-power X) . ((a ` ),( - (j - 1))));

            then (((a |^ (j - 1)) ` ) ` ) = (( BCI-power X) . ((a ` ), |.(j - 1).|)) by A10, ABSVALUE:def 1;

            then (((a |^ (j - 1)) ` ) ` ) = (a |^ (j - 1)) by A10, Def2;

            hence thesis by BCIALG_1: 29;

          end;

        end;

        for i st i <= 0 holds P[i] from INT_1:sch 3( A1, A6);

        hence thesis by A5;

      end;

    end;

    theorem :: BCIALG_6:14

    

     Th14: ((a |^ (n + 1)) ` ) = (((a |^ n) ` ) \ a)

    proof

      

       A1: (a |^ n) in ( AtomSet X) by Th13;

      ((a |^ (n + 1)) ` ) = ((a \ ((a |^ n) ` )) ` ) by Th2

      .= ((a ` ) \ (((a |^ n) ` ) ` )) by BCIALG_1: 9

      .= ((a ` ) \ (a |^ n)) by A1, BCIALG_1: 29;

      hence thesis by BCIALG_1: 7;

    end;

    

     Lm1: (a |^ (n + m)) = ((a |^ m) \ ((a |^ n) ` ))

    proof

      reconsider p = (a |^ n) as Element of ( AtomSet X) by Th13;

      defpred P[ Nat] means (a |^ (n + $1)) = ((a |^ $1) \ ((a |^ n) ` ));

       A1:

      now

        let m;

        reconsider q = (a |^ (m + 1)) as Element of ( AtomSet X) by Th13;

        assume

         A2: P[m];

        (a |^ (n + (m + 1))) = (a |^ ((n + m) + 1))

        .= (a \ (((a |^ m) \ ((a |^ n) ` )) ` )) by A2, Th2

        .= (a \ (((a |^ m) ` ) \ (((a |^ n) ` ) ` ))) by BCIALG_1: 9

        .= (a \ (((a |^ m) ` ) \ p)) by BCIALG_1: 29

        .= (p \ (((a |^ m) ` ) \ a)) by Th1

        .= ((a |^ n) \ ((a |^ (m + 1)) ` )) by Th14

        .= (q \ (p ` )) by Th1

        .= ((a |^ (m + 1)) \ ((a |^ n) ` ));

        hence P[(m + 1)];

      end;

      ((a |^ 0 ) \ ((a |^ n) ` )) = (((a |^ n) ` ) ` ) by Def1

      .= p by BCIALG_1: 29;

      then

       A3: P[ 0 ];

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

      hence thesis;

    end;

    

     Lm2: ((a |^ m) |^ n) = (a |^ (m * n))

    proof

      defpred P[ Nat] means ((a |^ m) |^ $1) = (a |^ (m * $1));

       A1:

      now

        let n;

        assume P[n];

        

        then ((a |^ m) |^ (n + 1)) = ((a |^ m) \ ((a |^ (m * n)) ` )) by Th2

        .= (a |^ (m + (m * n))) by Lm1

        .= (a |^ (m * (n + 1)));

        hence P[(n + 1)];

      end;

      ((a |^ m) |^ 0 ) = ( 0. X) by Def1;

      then

       A2: P[ 0 ] by Def1;

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

      hence thesis;

    end;

    theorem :: BCIALG_6:15

    

     Th15: ((a \ b) |^ n) = ((a |^ n) \ (b |^ n))

    proof

      defpred P[ Nat] means ((a \ b) |^ $1) = ((a |^ $1) \ (b |^ $1));

       A1:

      now

        let n;

        

         A2: ((b |^ n) ` ) in ( AtomSet X) by BCIALG_1: 34;

        

         A3: (a |^ (n + 1)) in ( AtomSet X) by Th13;

        assume P[n];

        

        then ((a \ b) |^ (n + 1)) = ((a \ b) \ (((a |^ n) \ (b |^ n)) ` )) by Th2

        .= ((a \ (((a |^ n) \ (b |^ n)) ` )) \ b) by BCIALG_1: 7

        .= ((a \ (((a |^ n) ` ) \ ((b |^ n) ` ))) \ b) by BCIALG_1: 9

        .= ((((b |^ n) ` ) \ (((a |^ n) ` ) \ a)) \ b) by A2, Th1

        .= ((((b |^ n) ` ) \ b) \ (((a |^ n) ` ) \ a)) by BCIALG_1: 7

        .= (((b |^ (n + 1)) ` ) \ (((a |^ n) ` ) \ a)) by Th14

        .= (((b |^ (n + 1)) ` ) \ ((a |^ (n + 1)) ` )) by Th14

        .= (((b |^ (n + 1)) \ (a |^ (n + 1))) ` ) by BCIALG_1: 9

        .= ((a |^ (n + 1)) \ (b |^ (n + 1))) by A3, BCIALG_1: 30;

        hence P[(n + 1)];

      end;

      ((a \ b) |^ 0 ) = ( 0. X) by Def1

      .= (( 0. X) ` ) by BCIALG_1:def 5

      .= ((a |^ 0 ) \ ( 0. X)) by Def1;

      then

       A4: P[ 0 ] by Def1;

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

      hence thesis;

    end;

    theorem :: BCIALG_6:16

    ((a \ b) |^ ( - n)) = ((a |^ ( - n)) \ (b |^ ( - n)))

    proof

      set c = (a ` ), d = (b ` );

      reconsider c, d as Element of ( AtomSet X) by BCIALG_1: 34;

      

       A1: (c |^ n) = (a |^ ( - n)) & (d |^ n) = (b |^ ( - n)) by Th10;

      ((a \ b) |^ ( - n)) = (((a \ b) ` ) |^ n) by Th10

      .= (((a ` ) \ (b ` )) |^ n) by BCIALG_1: 9;

      hence thesis by A1, Th15;

    end;

    theorem :: BCIALG_6:17

    

     Th17: ((a ` ) |^ n) = ((a |^ n) ` )

    proof

      defpred P[ Nat] means ((a ` ) |^ $1) = ((a |^ $1) ` );

       A1:

      now

        let n;

        assume P[n];

        ( 0. X) in ( AtomSet X);

        

        then ((a ` ) |^ (n + 1)) = ((( 0. X) |^ (n + 1)) \ (a |^ (n + 1))) by Th15

        .= ((a |^ (n + 1)) ` ) by Th7;

        hence P[(n + 1)];

      end;

      ((a ` ) |^ 0 ) = ( 0. X) by Def1

      .= (( 0. X) ` ) by BCIALG_1:def 5;

      then

       A2: P[ 0 ] by Def1;

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

      hence thesis;

    end;

    theorem :: BCIALG_6:18

    

     Th18: ((x ` ) |^ n) = ((x |^ n) ` )

    proof

      defpred P[ Nat] means ((x ` ) |^ $1) = ((x |^ $1) ` );

       A1:

      now

        let n;

        assume P[n];

        

        then ((x ` ) |^ (n + 1)) = ((x ` ) \ (((x |^ n) ` ) ` )) by Th2

        .= ((x \ ((x |^ n) ` )) ` ) by BCIALG_1: 9

        .= ((x |^ (n + 1)) ` ) by Th2;

        hence P[(n + 1)];

      end;

      ((x ` ) |^ 0 ) = ( 0. X) by Def1

      .= (( 0. X) ` ) by BCIALG_1:def 5;

      then

       A2: P[ 0 ] by Def1;

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

      hence thesis;

    end;

    theorem :: BCIALG_6:19

    ((a ` ) |^ ( - n)) = ((a |^ ( - n)) ` )

    proof

      reconsider c = (a ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

      (c |^ ( - n)) = ((c ` ) |^ n) by Th10

      .= ((c |^ n) ` ) by Th17

      .= ((a |^ ( - n)) ` ) by Th10;

      hence thesis;

    end;

    theorem :: BCIALG_6:20

    

     Th20: a = (((x ` ) ` ) |^ n) implies (x |^ n) in ( BranchV a)

    proof

      defpred P[ Nat] means for a st a = (((x ` ) ` ) |^ $1) holds (x |^ $1) in ( BranchV a);

       A1:

      now

        let n;

        assume

         A2: P[n];

        now

          set b = (((x ` ) ` ) |^ n);

          let a;

          assume a = (((x ` ) ` ) |^ (n + 1));

          ((x ` ) ` ) in ( AtomSet X) by BCIALG_1: 34;

          then

          reconsider b as Element of ( AtomSet X) by Th13;

          ( 0. X) in ( AtomSet X) & (x |^ n) in ( BranchV b) by A2;

          then ((x |^ n) ` ) = ((((x ` ) ` ) |^ n) ` ) by BCIALG_1: 37;

          then

           A3: (x |^ (n + 1)) = (x \ ((((x ` ) ` ) |^ n) ` )) by Th2;

          (((((x ` ) ` ) \ ((((x ` ) ` ) |^ n) ` )) \ (x \ ((((x ` ) ` ) |^ n) ` ))) \ (((x ` ) ` ) \ x)) = ( 0. X) by BCIALG_1:def 3;

          then (((((x ` ) ` ) |^ (n + 1)) \ (x |^ (n + 1))) \ (((x ` ) ` ) \ x)) = ( 0. X) by A3, Th2;

          then (((((x ` ) ` ) |^ (n + 1)) \ (x |^ (n + 1))) \ ( 0. X)) = ( 0. X) by BCIALG_1: 1;

          then ((((x ` ) ` ) |^ (n + 1)) \ (x |^ (n + 1))) = ( 0. X) by BCIALG_1: 2;

          then (((x ` ) ` ) |^ (n + 1)) <= (x |^ (n + 1));

          hence a = (((x ` ) ` ) |^ (n + 1)) implies (x |^ (n + 1)) in ( BranchV a);

        end;

        hence P[(n + 1)];

      end;

      (x |^ 0 ) = ( 0. X) by Def1;

      then (( 0. X) \ (x |^ 0 )) = ( 0. X) by BCIALG_1: 2;

      then ( 0. X) <= (x |^ 0 );

      then (((x ` ) ` ) |^ 0 ) <= (x |^ 0 ) by Def1;

      then

       A4: P[ 0 ];

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

      hence thesis;

    end;

    theorem :: BCIALG_6:21

    

     Th21: ((x |^ n) ` ) = ((((x ` ) ` ) |^ n) ` )

    proof

      set b = (((x ` ) ` ) |^ n);

      ((x ` ) ` ) in ( AtomSet X) by BCIALG_1: 34;

      then

      reconsider b as Element of ( AtomSet X) by Th13;

      ( 0. X) in ( AtomSet X) & (x |^ n) in ( BranchV b) by Th20;

      hence thesis by BCIALG_1: 37;

    end;

    

     Lm3: i > 0 & j > 0 implies ((a |^ i) \ (a |^ j)) = (a |^ (i - j))

    proof

      assume that

       A1: i > 0 and

       A2: j > 0 ;

      per cases by XXREAL_0: 1;

        suppose

         A3: i = j;

        then ((a |^ i) \ (a |^ j)) = ( 0. X) by BCIALG_1:def 5;

        then ((a |^ i) \ (a |^ j)) = (a |^ 0 ) by Def1;

        hence thesis by A3;

      end;

        suppose

         A4: i > j;

        set m = (i - j);

        m > 0 by A4, XREAL_1: 50;

        then

        reconsider j, m as Element of NAT by A2, INT_1: 3;

        (a |^ i) = (a |^ ((i - j) + j))

        .= ((a |^ j) \ ((a |^ m) ` )) by Lm1;

        then

         A5: ((a |^ i) \ (a |^ j)) = (((a |^ j) \ (a |^ j)) \ ((a |^ m) ` )) by BCIALG_1: 7;

        (a |^ m) in ( AtomSet X) by Th13;

        then (((a |^ m) ` ) ` ) = (a |^ m) by BCIALG_1: 29;

        hence thesis by A5, BCIALG_1:def 5;

      end;

        suppose

         A6: i < j;

        set m = (j - i);

        m > 0 by A6, XREAL_1: 50;

        then

        reconsider i, m as Element of NAT by A1, INT_1: 3;

        

         A7: ( 0. X) in ( AtomSet X);

        (a |^ j) = (a |^ (i + (j - i)))

        .= ((a |^ i) \ ((a |^ m) ` )) by Lm1;

        then ((a |^ i) \ (a |^ j)) = ((a |^ m) ` ) by A7, BCIALG_1: 32;

        then ((a |^ i) \ (a |^ j)) = ((a ` ) |^ m) by Th17;

        then ((a |^ i) \ (a |^ j)) = (a |^ ( - m)) by Th10;

        hence thesis;

      end;

    end;

    theorem :: BCIALG_6:22

    

     Th22: ((a |^ i) \ (a |^ j)) = (a |^ (i - j))

    proof

      per cases ;

        suppose

         A1: i > 0 ;

        per cases ;

          suppose j > 0 ;

          hence thesis by A1, Lm3;

        end;

          suppose

           A2: j = 0 ;

          (a |^ (i - 0 )) = ((a |^ i) \ ( 0. X)) by BCIALG_1: 2

          .= ((a |^ i) \ (a |^ 0 )) by Def1;

          hence thesis by A2;

        end;

          suppose

           A3: j < 0 ;

          set m = ( - j);

          reconsider i, m as Element of NAT by A1, A3, INT_1: 3;

          (a |^ j) = (( BCI-power X) . ((a ` ), |.j.|)) by A3, Def2

          .= ((a ` ) |^ m) by A3, ABSVALUE:def 1

          .= ((a |^ m) ` ) by Th17;

          then ((a |^ i) \ (a |^ j)) = (a |^ (i + m)) by Lm1;

          hence thesis;

        end;

      end;

        suppose

         A4: i = 0 ;

        per cases ;

          suppose j >= 0 ;

          then

          reconsider j as Element of NAT by INT_1: 3;

          ((a |^ 0 ) \ (a |^ j)) = ((a |^ j) ` ) by Def1

          .= ((a ` ) |^ j) by Th17

          .= (a |^ ( - j)) by Th10;

          hence thesis by A4;

        end;

          suppose

           A5: j < 0 ;

          set m = ( - j);

          reconsider m as Element of NAT by A5, INT_1: 3;

          (a |^ j) = (( BCI-power X) . ((a ` ), |.j.|)) by A5, Def2

          .= ((a ` ) |^ m) by A5, ABSVALUE:def 1

          .= ((a |^ m) ` ) by Th17;

          then ((a |^ 0 ) \ (a |^ j)) = (a |^ ( 0 + m)) by Lm1;

          hence thesis by A4;

        end;

      end;

        suppose

         A6: i < 0 ;

        then

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

        

         A7: ( - i) > 0 by A6;

        per cases ;

          suppose

           A8: j >= 0 ;

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

          reconsider n, j as Element of NAT by A6, A8, INT_1: 3;

          reconsider b = (a ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

          

           A9: (((a ` ) |^ j) ` ) = ((b ` ) |^ j) by Th17

          .= (a |^ j) by BCIALG_1: 29;

          

           A10: (a |^ i) = (( BCI-power X) . ((a ` ), |.i.|)) by A6, Def2

          .= ((a ` ) |^ m) by A6, ABSVALUE:def 1;

          (a |^ (i - j)) = (( BCI-power X) . ((a ` ), |.(i - j).|)) by A6, Def2

          .= ((a ` ) |^ n) by A6, ABSVALUE:def 1

          .= (b |^ (j + m))

          .= (((a ` ) |^ m) \ (((a ` ) |^ j) ` )) by Lm1;

          hence thesis by A10, A9;

        end;

          suppose

           A11: j < 0 ;

          reconsider b = (a ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

          

           A12: ( - j) > 0 by A11;

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

          

           A13: (a |^ j) = (( BCI-power X) . ((a ` ), |.j.|)) by A11, Def2

          .= ((a ` ) |^ n) by A11, ABSVALUE:def 1;

          (a |^ i) = (( BCI-power X) . ((a ` ), |.i.|)) by A6, Def2

          .= ((a ` ) |^ m) by A6, ABSVALUE:def 1;

          then

           A14: ((a |^ i) \ (a |^ j)) = (b |^ (m - n)) by A7, A12, A13, Lm3;

          per cases ;

            suppose m >= n;

            then

            reconsider q = (m - n) as Element of NAT by INT_1: 3, XREAL_1: 48;

            ((a |^ i) \ (a |^ j)) = (a |^ ( - q)) by A14, Th10;

            hence thesis;

          end;

            suppose

             A15: m < n;

            then (n - m) > 0 by XREAL_1: 50;

            then

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

            

             A16: (m - n) < 0 by A15, XREAL_1: 49;

            

            then ((a |^ i) \ (a |^ j)) = (( BCI-power X) . ((b ` ), |.(m - n).|)) by A14, Def2

            .= (( BCI-power X) . ((b ` ),( - (m - n)))) by A16, ABSVALUE:def 1

            .= (a |^ p) by BCIALG_1: 29;

            hence thesis;

          end;

        end;

      end;

    end;

    theorem :: BCIALG_6:23

    

     Th23: ((a |^ i) |^ j) = (a |^ (i * j))

    proof

      per cases ;

        suppose

         A1: i >= 0 ;

        per cases ;

          suppose j >= 0 ;

          then

          reconsider i, j as Element of NAT by A1, INT_1: 3;

          ((a |^ i) |^ j) = (a |^ (i * j)) by Lm2;

          hence thesis;

        end;

          suppose

           A2: j < 0 ;

          then

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

          reconsider i as Element of NAT by A1, INT_1: 3;

          per cases by A2;

            suppose

             A3: (i * j) < 0 ;

            then

            reconsider p = ( - (i * j)) as Element of NAT by INT_1: 3;

            reconsider b = (a ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

            reconsider d = (a |^ i) as Element of ( AtomSet X) by Th13;

            (a |^ (i * j)) = (( BCI-power X) . ((a ` ), |.(i * j).|)) by A3, Def2

            .= ((a ` ) |^ p) by A3, ABSVALUE:def 1

            .= ((a ` ) |^ (i * ( - j)))

            .= ((b |^ i) |^ m) by Lm2

            .= (((a |^ i) ` ) |^ m) by Th17

            .= (d |^ ( - m)) by Th10

            .= ((a |^ i) |^ ( - ( - j)));

            hence thesis;

          end;

            suppose

             A4: (i * j) = 0 ;

            reconsider d = ( 0. X) as Element of ( AtomSet X) by BCIALG_1: 23;

            ((a |^ 0 ) |^ j) = (( 0. X) |^ j) by Def1

            .= (( BCI-power X) . ((( 0. X) ` ), |.j.|)) by A2, Def2

            .= ((( 0. X) ` ) |^ m) by A2, ABSVALUE:def 1

            .= ((d |^ m) ` ) by Th17

            .= (( 0. X) ` ) by Th7

            .= ( 0. X) by BCIALG_1: 2

            .= (a |^ (i * j)) by A4, Th3;

            hence thesis by A2, A4, XCMPLX_1: 6;

          end;

        end;

      end;

        suppose

         A5: i < 0 ;

        then

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

        per cases ;

          suppose

           A6: j > 0 ;

          then

          reconsider j as Element of NAT by INT_1: 3;

          reconsider b = (a ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

          reconsider p = ( - (i * j)) as Element of NAT by A5, INT_1: 3;

          

           A7: (i * j) < ( 0 * j) by A5, A6;

          

          then (a |^ (i * j)) = (( BCI-power X) . ((a ` ), |.(i * j).|)) by Def2

          .= ((a ` ) |^ p) by A7, ABSVALUE:def 1

          .= ((a ` ) |^ (( - i) * j))

          .= ((b |^ m) |^ j) by Lm2

          .= ((a |^ ( - m)) |^ j) by Th10;

          hence thesis;

        end;

          suppose

           A8: j = 0 ;

          reconsider b = (a |^ i) as Element of ( AtomSet X) by Th13;

          ((a |^ i) |^ j) = (b |^ 0 ) by A8

          .= ( 0. X) by Def1

          .= (a |^ (i * 0 )) by Th3;

          hence thesis by A8;

        end;

          suppose j < 0 ;

          then

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

          reconsider d = (a |^ m) as Element of ( AtomSet X) by Th13;

          reconsider e = (d ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

          (a |^ i) = (( BCI-power X) . ((a ` ), |.i.|)) by A5, Def2

          .= ((a ` ) |^ m) by A5, ABSVALUE:def 1;

          

          then ((a |^ i) |^ j) = (e |^ ( - n)) by Th17

          .= ((e ` ) |^ n) by Th10

          .= (d |^ n) by BCIALG_1: 29

          .= (a |^ (( - i) * ( - j))) by Lm2;

          hence thesis;

        end;

      end;

    end;

    theorem :: BCIALG_6:24

    

     Th24: (a |^ (i + j)) = ((a |^ i) \ ((a |^ j) ` ))

    proof

      per cases ;

        suppose j > 0 ;

        then

        reconsider j as Element of NAT by INT_1: 3;

        ((a |^ i) \ ((a |^ j) ` )) = ((a |^ i) \ ((a ` ) |^ j)) by Th17

        .= ((a |^ i) \ (a |^ ( - j))) by Th10

        .= (a |^ (i - ( - j))) by Th22;

        hence thesis;

      end;

        suppose

         A1: j = 0 ;

        

        then (a |^ (i + j)) = ((a |^ i) \ ( 0. X)) by BCIALG_1: 2

        .= ((a |^ i) \ (( 0. X) ` )) by BCIALG_1: 2

        .= ((a |^ i) \ ((a |^ j) ` )) by A1, Th3;

        hence thesis;

      end;

        suppose j < 0 ;

        then

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

        reconsider b = (a ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

        ((a |^ i) \ ((a |^ j) ` )) = ((a |^ i) \ ((a |^ ( - ( - j))) ` ))

        .= ((a |^ i) \ (((a ` ) |^ n) ` )) by Th10

        .= ((a |^ i) \ ((b ` ) |^ n)) by Th17

        .= ((a |^ i) \ (a |^ n)) by BCIALG_1: 29

        .= (a |^ (i - n)) by Th22;

        hence thesis;

      end;

    end;

    definition

      let X, x;

      :: BCIALG_6:def4

      attr x is finite-period means ex n be Element of NAT st n <> 0 & (x |^ n) in ( BCK-part X);

    end

    theorem :: BCIALG_6:25

    

     Th25: x is finite-period implies ((x ` ) ` ) is finite-period

    proof

      reconsider b = ((x ` ) ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

      assume x is finite-period;

      then

      consider p be Element of NAT such that

       A1: p <> 0 and

       A2: (x |^ p) in ( BCK-part X);

      ex y be Element of X st y = (x |^ p) & ( 0. X) <= y by A2;

      then ((x |^ p) ` ) = ( 0. X);

      then ((b |^ p) ` ) = ( 0. X) by Th21;

      then ( 0. X) <= (b |^ p);

      then (b |^ p) in ( BCK-part X);

      hence thesis by A1;

    end;

    definition

      let X, x;

      :: BCIALG_6:def5

      func ord x -> Element of NAT means

      : Def5: (x |^ it ) in ( BCK-part X) & it <> 0 & for m be Element of NAT st (x |^ m) in ( BCK-part X) & m <> 0 holds it <= m;

      existence

      proof

        defpred P[ Nat] means (x |^ $1) in ( BCK-part X) & $1 <> 0 ;

        ex n be Element of NAT st n <> 0 & (x |^ n) in ( BCK-part X) by A1;

        then

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

        consider k be Nat such that

         A3: P[k] and

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

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

        take k;

        thus (x |^ k) in ( BCK-part X) & k <> 0 by A3;

        let m be Element of NAT ;

        assume (x |^ m) in ( BCK-part X) & m <> 0 ;

        hence thesis by A4;

      end;

      uniqueness

      proof

        let n1,n2 be Element of NAT ;

        assume (x |^ n1) in ( BCK-part X) & n1 <> 0 & (for m be Element of NAT st (x |^ m) in ( BCK-part X) & m <> 0 holds n1 <= m) & (x |^ n2) in ( BCK-part X) & (n2 <> 0 & for m be Element of NAT st (x |^ m) in ( BCK-part X) & m <> 0 holds n2 <= m);

        then n1 <= n2 & n2 <= n1;

        hence thesis by XXREAL_0: 1;

      end;

    end

    theorem :: BCIALG_6:26

    

     Th26: a is finite-period & ( ord a) = n implies (a |^ n) = ( 0. X)

    proof

      assume a is finite-period & ( ord a) = n;

      then (a |^ n) in ( BCK-part X) by Def5;

      then ex x be Element of X st x = (a |^ n) & ( 0. X) <= x;

      then

       A1: (( 0. X) \ (a |^ n)) = ( 0. X);

      (a |^ n) in ( AtomSet X) by Th13;

      then ex y be Element of X st y = (a |^ n) & y is atom;

      hence thesis by A1;

    end;

    theorem :: BCIALG_6:27

    X is BCK-algebra iff for x holds x is finite-period & ( ord x) = 1

    proof

      thus X is BCK-algebra implies for x holds x is finite-period & ( ord x) = 1

      proof

        assume

         A1: X is BCK-algebra;

        let x;

        

         A2: for m be Element of NAT st (x |^ m) in ( BCK-part X) & m <> 0 holds 1 <= m

        proof

          let m be Element of NAT ;

          assume that (x |^ m) in ( BCK-part X) and

           A3: m <> 0 ;

          ( 0 + 1) <= m by A3, INT_1: 7;

          hence thesis;

        end;

        (x ` ) = ( 0. X) by A1, BCIALG_1:def 8;

        then ( 0. X) <= x;

        then x in ( BCK-part X);

        then

         A4: (x |^ 1) in ( BCK-part X) by Th4;

        then x is finite-period;

        hence thesis by A4, A2, Def5;

      end;

      assume

       A5: for x holds x is finite-period & ( ord x) = 1;

      for y,z be Element of X holds ((y \ z) \ y) = ( 0. X)

      proof

        let y,z be Element of X;

        z is finite-period & ( ord z) = 1 by A5;

        then (z |^ 1) in ( BCK-part X) by Def5;

        then z in ( BCK-part X) by Th4;

        then

         A6: ex z1 be Element of X st z = z1 & ( 0. X) <= z1;

        ((y \ z) \ y) = ((y \ y) \ z) by BCIALG_1: 7;

        then ((y \ z) \ y) = (z ` ) by BCIALG_1:def 5;

        hence thesis by A6;

      end;

      then X is being_K;

      hence thesis by BCIALG_1: 18;

    end;

    theorem :: BCIALG_6:28

    

     Th28: x is finite-period & a is finite-period & x in ( BranchV a) implies ( ord x) = ( ord a)

    proof

      assume that

       A1: x is finite-period and

       A2: a is finite-period and

       A3: x in ( BranchV a);

      set na = ( ord a);

      na <> 0 by A2, Def5;

      then

       A4: na >= 1 by NAT_1: 14;

      per cases by A4, XXREAL_0: 1;

        suppose

         A5: na = 1;

        then (a |^ 1) in ( BCK-part X) by A2, Def5;

        then a in ( BCK-part X) by Th4;

        then ex aa be Element of X st a = aa & ( 0. X) <= aa;

        then

         A6: (a ` ) = ( 0. X);

        a in ( AtomSet X);

        then ex ab be Element of X st a = ab & ab is atom;

        then a = ( 0. X) by A6;

        then

         A7: (x |^ 1) in ( BCK-part X) by A3, Th4;

        for m be Element of NAT st (x |^ m) in ( BCK-part X) & m <> 0 holds 1 <= m by NAT_1: 14;

        hence thesis by A1, A5, A7, Def5;

      end;

        suppose

         A8: na > 1;

        ( 0. X) in ( AtomSet X);

        then

         A9: (x ` ) = (a ` ) by A3, BCIALG_1: 37;

        

         A10: for m be Element of NAT st (x |^ m) in ( BCK-part X) & m <> 0 holds na <= m

        proof

          let m be Element of NAT ;

          assume that

           A11: (x |^ m) in ( BCK-part X) and

           A12: m <> 0 ;

          ex xx be Element of X st (x |^ m) = xx & ( 0. X) <= xx by A11;

          then ((x |^ m) ` ) = ( 0. X);

          then ((a ` ) |^ m) = ( 0. X) by A9, Th18;

          then ((a |^ m) ` ) = ( 0. X) by Th17;

          then ( 0. X) <= (a |^ m);

          then (a |^ m) in ( BCK-part X);

          hence thesis by A2, A12, Def5;

        end;

        (a |^ na) in ( BCK-part X) by A2, Def5;

        then ex aa be Element of X st (a |^ na) = aa & ( 0. X) <= aa;

        then ((a |^ na) ` ) = ( 0. X);

        then ((x ` ) |^ na) = ( 0. X) by A9, Th17;

        then ((x |^ na) ` ) = ( 0. X) by Th18;

        then ( 0. X) <= (x |^ na);

        then (x |^ na) in ( BCK-part X);

        hence thesis by A1, A8, A10, Def5;

      end;

    end;

    theorem :: BCIALG_6:29

    

     Th29: x is finite-period & ( ord x) = n implies ((x |^ m) in ( BCK-part X) iff n divides m)

    proof

      reconsider b = ((x ` ) ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

      reconsider bn = (b |^ n) as Element of ( AtomSet X) by Th13;

      assume that

       A1: x is finite-period and

       A2: ( ord x) = n;

      

       A3: b is finite-period by A1, Th25;

      thus (x |^ m) in ( BCK-part X) implies n divides m

      proof

        defpred P[ Nat] means (x |^ $1) in ( BCK-part X) implies n divides $1;

        

         A4: for m be Nat st for k be Nat st k < m holds P[k] holds P[m]

        proof

          let m be Nat;

          assume

           A5: for k be Nat st k < m holds P[k];

          assume

           A6: (x |^ m) in ( BCK-part X);

          per cases ;

            suppose m = 0 ;

            hence thesis by INT_2: 12;

          end;

            suppose

             A7: m <> 0 ;

            reconsider mm = m as Element of NAT by ORDINAL1:def 12;

            (x |^ mm) in ( BCK-part X) by A6;

            then n <= m by A1, A2, A7, Def5;

            then

            consider k be Nat such that

             A8: m = (n + k) by NAT_1: 10;

            reconsider b = ((x ` ) ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

            

             A9: b is finite-period by A1, Th25;

            (b \ x) = ( 0. X) by BCIALG_1: 1;

            then b <= x;

            then x in ( BranchV b);

            then n = ( ord b) by A1, A2, A9, Th28;

            then (b |^ n) in ( BCK-part X) by A9, Def5;

            then ex z be Element of X st z = (b |^ n) & ( 0. X) <= z;

            then

             A10: ((b |^ n) ` ) = ( 0. X);

            ex zz be Element of X st zz = (x |^ m) & ( 0. X) <= zz by A6;

            then ((x |^ m) ` ) = ( 0. X);

            then ((b |^ (n + k)) ` ) = ( 0. X) by A8, Th21;

            then (((b |^ n) \ ((b |^ k) ` )) ` ) = ( 0. X) by Th24;

            then ((((b |^ k) ` ) ` ) ` ) = ( 0. X) by A10, BCIALG_1: 9;

            then ((b |^ k) ` ) = ( 0. X) by BCIALG_1: 8;

            then ((x |^ k) ` ) = ( 0. X) by Th21;

            then ( 0. X) <= (x |^ k);

            then

             A11: (x |^ k) in ( BCK-part X);

            n <> 0 by A1, A2, Def5;

            then n divides k by A5, A8, A11, NAT_1: 16;

            then

            consider i be Nat such that

             A12: k = (n * i) by NAT_D:def 3;

            m = (n * (1 + i)) by A8, A12;

            hence thesis by NAT_D:def 3;

          end;

        end;

        for m be Nat holds P[m] from NAT_1:sch 4( A4);

        hence thesis;

      end;

      assume n divides m;

      then

      consider i be Nat such that

       A13: m = (n * i) by NAT_D:def 3;

      (b \ x) = ( 0. X) by BCIALG_1: 1;

      then b <= x;

      then x in ( BranchV b);

      then n = ( ord b) by A1, A2, A3, Th28;

      then (b |^ n) in ( BCK-part X) by A3, Def5;

      then ex z be Element of X st z = (b |^ n) & ( 0. X) <= z;

      then

       A14: ((b |^ n) ` ) = ( 0. X);

      ((b |^ m) ` ) = ((bn |^ i) ` ) by A13, Th23;

      then ((b |^ m) ` ) = (( 0. X) |^ i) by A14, Th17;

      then ((b |^ m) ` ) = ( 0. X) by Th7;

      then ((x |^ m) ` ) = ( 0. X) by Th21;

      then ( 0. X) <= (x |^ m);

      hence thesis;

    end;

    theorem :: BCIALG_6:30

    x is finite-period & (x |^ m) is finite-period & ( ord x) = n & m > 0 implies ( ord (x |^ m)) = (n div (m gcd n))

    proof

      assume that

       A1: x is finite-period and

       A2: (x |^ m) is finite-period and

       A3: ( ord x) = n and

       A4: m > 0 ;

      reconsider b = ((x ` ) ` ) as Element of ( AtomSet X) by BCIALG_1: 34;

      

       A5: b is finite-period by A1, Th25;

      (b \ x) = ( 0. X) by BCIALG_1: 1;

      then b <= x;

      then x in ( BranchV b);

      then

       A6: n = ( ord b) by A1, A3, A5, Th28;

      then (b |^ n) in ( BCK-part X) by A5, Def5;

      then

       A7: ex z be Element of X st z = (b |^ n) & ( 0. X) <= z;

      reconsider mgn = (m gcd n) as Element of NAT ;

      (m gcd n) divides n by INT_2: 21;

      then

      consider vn be Nat such that

       A8: n = (mgn * vn) by NAT_D:def 3;

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

      (m gcd n) divides m by INT_2: 21;

      then

      consider i be Nat such that

       A9: m = (mgn * i) by NAT_D:def 3;

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

      

       A10: n = ((mgn * vn) + 0 ) by A8;

      

       A11: (vn,i) are_coprime

      proof

        (i gcd vn) divides i by NAT_D:def 5;

        then

        consider b2 be Nat such that

         A12: i = ((i gcd vn) * b2) by NAT_D:def 3;

        m = (((m gcd n) * (i gcd vn)) * b2) by A9, A12;

        then

         A13: ((m gcd n) * (i gcd vn)) divides m by NAT_D:def 3;

        (i gcd vn) divides vn by NAT_D:def 5;

        then

        consider b1 be Nat such that

         A14: vn = ((i gcd vn) * b1) by NAT_D:def 3;

        n = (((m gcd n) * (i gcd vn)) * b1) by A8, A14;

        then ((m gcd n) * (i gcd vn)) divides n by NAT_D:def 3;

        then ((m gcd n) * (i gcd vn)) divides (m gcd n) by A13, NAT_D:def 5;

        then

        consider c be Nat such that

         A15: (m gcd n) = (((m gcd n) * (i gcd vn)) * c) by NAT_D:def 3;

        

         A16: (m gcd n) <> 0 by A4, INT_2: 5;

        ((m gcd n) * 1) = ((m gcd n) * ((i gcd vn) * c)) by A15;

        then 1 = (i gcd vn) by A16, NAT_1: 15, XCMPLX_1: 5;

        hence thesis by INT_2:def 3;

      end;

      

       A17: for mm be Element of NAT st ((x |^ m) |^ mm) in ( BCK-part X) & mm <> 0 holds vn <= mm

      proof

        let mm be Element of NAT ;

        assume that

         A18: ((x |^ m) |^ mm) in ( BCK-part X) and

         A19: mm <> 0 ;

        ex z be Element of X st z = ((x |^ m) |^ mm) & ( 0. X) <= z by A18;

        then (((x |^ m) |^ mm) ` ) = ( 0. X);

        then (((x |^ m) ` ) |^ mm) = ( 0. X) by Th18;

        then (((b |^ m) ` ) |^ mm) = ( 0. X) by Th21;

        then (((b |^ m) |^ mm) ` ) = ( 0. X) by Th18;

        then ((b |^ (m * mm)) ` ) = ( 0. X) by Th23;

        then ( 0. X) <= (b |^ (m * mm));

        then (b |^ (m * mm)) in ( BCK-part X);

        then (mgn * vn) divides ((mgn * i) * mm) by A8, A9, A5, A6, Th29;

        then

        consider c be Nat such that

         A20: ((mgn * i) * mm) = ((mgn * vn) * c) by NAT_D:def 3;

        

         A21: mgn <> 0 by A4, INT_2: 5;

        (mgn * (i * mm)) = (mgn * (vn * c)) by A20;

        then (i * mm) = (vn * c) by A21, XCMPLX_1: 5;

        then vn divides (i * mm) by NAT_D:def 3;

        then vn divides mm by A11, INT_2: 25;

        then

        consider cc be Nat such that

         A22: mm = (vn * cc) by NAT_D:def 3;

        cc <> 0 by A19, A22;

        hence thesis by A22, NAT_1: 24;

      end;

      (((x |^ m) |^ vn) ` ) = (((x |^ m) ` ) |^ vn) by Th18

      .= (((b |^ m) ` ) |^ vn) by Th21

      .= (((b |^ m) |^ vn) ` ) by Th18

      .= ((b |^ ((mgn * i) * vn)) ` ) by A9, Th23

      .= ((b |^ (n * i)) ` ) by A8

      .= (((b |^ n) |^ i) ` ) by Th23

      .= (((b |^ n) ` ) |^ i) by Th18

      .= (( 0. X) |^ i) by A7

      .= ( 0. X) by Th7;

      then ( 0. X) <= ((x |^ m) |^ vn);

      then

       A23: ((x |^ m) |^ vn) in ( BCK-part X);

      (n gcd m) > 0 by A4, NEWTON: 58;

      then

       A24: (n div mgn) = vn by A10, NAT_D:def 1;

      vn <> 0 by A1, A3, A8, Def5;

      hence thesis by A2, A24, A23, A17, Def5;

    end;

    theorem :: BCIALG_6:31

    x is finite-period & (x ` ) is finite-period implies ( ord x) = ( ord (x ` ))

    proof

      assume that

       A1: x is finite-period and

       A2: (x ` ) is finite-period;

      set m = ( ord (x ` ));

      ((x ` ) |^ m) in ( BCK-part X) by A2, Def5;

      then ex zz be Element of X st zz = ((x ` ) |^ m) & ( 0. X) <= zz;

      then (((x ` ) |^ m) ` ) = ( 0. X);

      then (((x ` ) ` ) |^ m) = ( 0. X) by Th18;

      then ((((x ` ) ` ) |^ m) ` ) = ( 0. X) by BCIALG_1:def 5;

      then ((x |^ m) ` ) = ( 0. X) by Th21;

      then ( 0. X) <= (x |^ m);

      then

       A3: (x |^ m) in ( BCK-part X);

      set n = ( ord x);

      m <> 0 by A2, Def5;

      then

       A4: n <= m by A1, A3, Def5;

      (x |^ n) in ( BCK-part X) by A1, Def5;

      then ex zz be Element of X st zz = (x |^ n) & ( 0. X) <= zz;

      then ((x |^ n) ` ) = ( 0. X);

      then ((x ` ) |^ n) = ( 0. X) by Th18;

      then (((x ` ) |^ n) ` ) = ( 0. X) by BCIALG_1:def 5;

      then ( 0. X) <= ((x ` ) |^ n);

      then

       A5: ((x ` ) |^ n) in ( BCK-part X);

      n <> 0 by A1, Def5;

      then m <= n by A2, A5, Def5;

      hence thesis by A4, XXREAL_0: 1;

    end;

    theorem :: BCIALG_6:32

    (x \ y) is finite-period & x in ( BranchV a) & y in ( BranchV a) implies ( ord (x \ y)) = 1

    proof

      assume that

       A1: (x \ y) is finite-period and

       A2: x in ( BranchV a) & y in ( BranchV a);

      

       A3: for m be Element of NAT st ((x \ y) |^ m) in ( BCK-part X) & m <> 0 holds 1 <= m by NAT_1: 14;

      (x \ y) in ( BCK-part X) by A2, BCIALG_1: 40;

      then ((x \ y) |^ 1) in ( BCK-part X) by Th4;

      hence thesis by A1, A3, Def5;

    end;

    theorem :: BCIALG_6:33

    (a \ b) is finite-period & x is finite-period & y is finite-period & a is finite-period & b is finite-period & x in ( BranchV a) & y in ( BranchV b) implies ( ord (a \ b)) divides (( ord x) lcm ( ord y))

    proof

      assume that

       A1: (a \ b) is finite-period and

       A2: x is finite-period and

       A3: y is finite-period and

       A4: a is finite-period and

       A5: b is finite-period and

       A6: x in ( BranchV a) and

       A7: y in ( BranchV b);

      ( ord y) divides (( ord x) lcm ( ord y)) by NAT_D:def 4;

      then

      consider yx be Nat such that

       A8: (( ord x) lcm ( ord y)) = (( ord y) * yx) by NAT_D:def 3;

      reconsider na = ( ord a) as Element of NAT ;

      reconsider xly = (( ord x) lcm ( ord y)) as Element of NAT ;

      ( ord x) divides (( ord x) lcm ( ord y)) by NAT_D:def 4;

      then

      consider xy be Nat such that

       A9: (( ord x) lcm ( ord y)) = (( ord x) * xy) by NAT_D:def 3;

      ((a \ b) |^ xly) = ((a |^ (( ord x) * xy)) \ (b |^ (( ord y) * yx))) by A9, A8, Th15

      .= (((a |^ ( ord x)) |^ xy) \ (b |^ (( ord y) * yx))) by Th23

      .= (((a |^ ( ord x)) |^ xy) \ ((b |^ ( ord y)) |^ yx)) by Th23

      .= (((a |^ na) |^ xy) \ ((b |^ ( ord y)) |^ yx)) by A2, A4, A6, Th28

      .= ((( 0. X) |^ xy) \ ((b |^ ( ord y)) |^ yx)) by A4, Th26

      .= ((( 0. X) |^ xy) \ ((b |^ ( ord b)) |^ yx)) by A3, A5, A7, Th28

      .= ((( 0. X) |^ xy) \ (( 0. X) |^ yx)) by A5, Th26

      .= ((( 0. X) |^ yx) ` ) by Th7

      .= (( 0. X) ` ) by Th7

      .= ( 0. X) by BCIALG_1:def 5;

      then (((a \ b) |^ xly) ` ) = ( 0. X) by BCIALG_1:def 5;

      then ( 0. X) <= ((a \ b) |^ xly);

      then ((a \ b) |^ xly) in ( BCK-part X);

      hence thesis by A1, Th29;

    end;

    begin

    reserve X,X9,Y for BCI-algebra,

H9 for SubAlgebra of X9,

G for SubAlgebra of X,

A9 for non empty Subset of X9,

I for Ideal of X,

CI,K for closed Ideal of X,

x,y,a,b for Element of X,

RI for I-congruence of X, I,

RK for I-congruence of X, K;

    theorem :: BCIALG_6:34

    

     Th34: for X be BCI-algebra holds for Y be SubAlgebra of X holds for x,y be Element of X, x9,y9 be Element of Y st x = x9 & y = y9 holds (x \ y) = (x9 \ y9)

    proof

      let X be BCI-algebra;

      let Y be SubAlgebra of X;

      let x,y be Element of X, x9,y9 be Element of Y such that

       A1: x = x9 & y = y9;

      

       A2: [x9, y9] in [:the carrier of Y, the carrier of Y:] by ZFMISC_1: 87;

      (x9 \ y9) = ((the InternalDiff of X || the carrier of Y) . (x9,y9)) by BCIALG_1:def 10

      .= (x \ y) by A1, A2, FUNCT_1: 49;

      hence thesis;

    end;

    definition

      let X,X9 be non empty BCIStr_0;

      let f be Function of X, X9;

      :: BCIALG_6:def6

      attr f is multiplicative means

      : Def6: for a,b be Element of X holds (f . (a \ b)) = ((f . a) \ (f . b));

    end

    registration

      let X,X9 be BCI-algebra;

      cluster multiplicative for Function of X, X9;

      existence

      proof

        reconsider f = (the carrier of X --> ( 0. X9)) as Function of X, X9;

        take f;

        for x,y be Element of X holds (f . (x \ y)) = ((f . x) \ (f . y))

        proof

          let x,y be Element of X;

          (f . (x \ y)) = ( 0. X9) by FUNCOP_1: 7

          .= (( 0. X9) ` ) by BCIALG_1: 2

          .= ((f . x) \ ( 0. X9)) by FUNCOP_1: 7;

          hence thesis by FUNCOP_1: 7;

        end;

        hence thesis;

      end;

    end

    definition

      let X,X9 be BCI-algebra;

      mode BCI-homomorphism of X,X9 is multiplicative Function of X, X9;

    end

    reserve f for BCI-homomorphism of X, X9;

    reserve g for BCI-homomorphism of X9, X;

    reserve h for BCI-homomorphism of X9, Y;

    definition

      let X, X9, f;

      :: BCIALG_6:def7

      attr f is isotonic means for x, y st x <= y holds (f . x) <= (f . y);

    end

    definition

      let X;

      mode Endomorphism of X is BCI-homomorphism of X, X;

    end

    definition

      let X, X9, f;

      :: BCIALG_6:def8

      func Ker f -> set equals { x where x be Element of X : (f . x) = ( 0. X9) };

      coherence ;

    end

    theorem :: BCIALG_6:35

    

     Th35: (f . ( 0. X)) = ( 0. X9)

    proof

      (f . ( 0. X)) = (f . (( 0. X) ` )) by BCIALG_1: 2

      .= ((f . ( 0. X)) \ (f . ( 0. X))) by Def6;

      hence thesis by BCIALG_1:def 5;

    end;

    registration

      let X, X9, f;

      cluster ( Ker f) -> non empty;

      coherence

      proof

        (f . ( 0. X)) = ( 0. X9) by Th35;

        then ( 0. X) in ( Ker f);

        hence thesis;

      end;

    end

    theorem :: BCIALG_6:36

    x <= y implies (f . x) <= (f . y)

    proof

      assume

       A1: x <= y;

      ((f . x) \ (f . y)) = (f . (x \ y)) by Def6

      .= (f . ( 0. X)) by A1

      .= ( 0. X9) by Th35;

      hence thesis;

    end;

    theorem :: BCIALG_6:37

    f is one-to-one iff ( Ker f) = {( 0. X)}

    proof

      thus f is one-to-one implies ( Ker f) = {( 0. X)}

      proof

        assume

         A1: f is one-to-one;

        thus ( Ker f) c= {( 0. X)}

        proof

          let a be object;

          assume a in ( Ker f);

          then

           A2: ex x be Element of X st a = x & (f . x) = ( 0. X9);

          then

          reconsider a as Element of X;

          (f . a) = (f . ( 0. X)) by A2, Th35;

          then a = ( 0. X) by A1, FUNCT_2: 19;

          hence thesis by TARSKI:def 1;

        end;

        let a be object;

        assume

         A3: a in {( 0. X)};

        then

        reconsider a as Element of X by TARSKI:def 1;

        a = ( 0. X) by A3, TARSKI:def 1;

        then (f . a) = ( 0. X9) by Th35;

        hence thesis;

      end;

      assume

       A4: ( Ker f) = {( 0. X)};

      now

        let a, b;

        assume that

         A5: a <> b and

         A6: (f . a) = (f . b);

        ((f . b) \ (f . a)) = ( 0. X9) by A6, BCIALG_1:def 5;

        then (f . (b \ a)) = ( 0. X9) by Def6;

        then (b \ a) in ( Ker f);

        then

         A7: (b \ a) = ( 0. X) by A4, TARSKI:def 1;

        ((f . a) \ (f . b)) = ( 0. X9) by A6, BCIALG_1:def 5;

        then (f . (a \ b)) = ( 0. X9) by Def6;

        then (a \ b) in ( Ker f);

        then (a \ b) = ( 0. X) by A4, TARSKI:def 1;

        hence contradiction by A5, A7, BCIALG_1:def 7;

      end;

      then for a, b st (f . a) = (f . b) holds a = b;

      hence thesis by GROUP_6: 1;

    end;

    theorem :: BCIALG_6:38

    f is bijective & g = (f " ) implies g is bijective

    proof

      assume

       A1: f is bijective & g = (f " );

      ( dom f) = the carrier of X by FUNCT_2:def 1;

      then ( rng g) = the carrier of X by A1, FUNCT_1: 33;

      then

       A2: g is onto by FUNCT_2:def 3;

      g is one-to-one by A1, FUNCT_1: 40;

      hence thesis by A2;

    end;

    theorem :: BCIALG_6:39

    (h * f) is BCI-homomorphism of X, Y

    proof

      reconsider g = (h * f) as Function of X, Y;

      now

        let a, b;

        

        thus (g . (a \ b)) = (h . (f . (a \ b))) by FUNCT_2: 15

        .= (h . ((f . a) \ (f . b))) by Def6

        .= ((h . (f . a)) \ (h . (f . b))) by Def6

        .= ((g . a) \ (h . (f . b))) by FUNCT_2: 15

        .= ((g . a) \ (g . b)) by FUNCT_2: 15;

      end;

      hence thesis by Def6;

    end;

    theorem :: BCIALG_6:40

    for Z be SubAlgebra of X9 st the carrier of Z = ( rng f) holds f is BCI-homomorphism of X, Z

    proof

      let Z be SubAlgebra of X9;

      

       A1: ( dom f) = the carrier of X by FUNCT_2:def 1;

      assume the carrier of Z = ( rng f);

      then

      reconsider f9 = f as Function of X, Z by A1, RELSET_1: 4;

      now

        let a, b;

        

        thus ((f9 . a) \ (f9 . b)) = ((f . a) \ (f . b)) by Th34

        .= (f9 . (a \ b)) by Def6;

      end;

      hence thesis by Def6;

    end;

    theorem :: BCIALG_6:41

    

     Th41: ( Ker f) is closed Ideal of X

    proof

      now

        let x be object;

        assume x in ( Ker f);

        then ex x9 be Element of X st x = x9 & (f . x9) = ( 0. X9);

        hence x in the carrier of X;

      end;

      then

       A1: ( Ker f) is non empty Subset of X by TARSKI:def 3;

       A2:

      now

        let x, y;

        assume (x \ y) in ( Ker f) & y in ( Ker f);

        then (ex y9 be Element of X st y = y9 & (f . y9) = ( 0. X9)) & ex x9 be Element of X st (x \ y) = x9 & (f . x9) = ( 0. X9);

        then ((f . x) \ ( 0. X9)) = ( 0. X9) by Def6;

        then (f . x) = ( 0. X9) by BCIALG_1: 2;

        hence x in ( Ker f);

      end;

      (f . ( 0. X)) = ( 0. X9) by Th35;

      then ( 0. X) in ( Ker f);

      then

      reconsider Kf = ( Ker f) as Ideal of X by A1, A2, BCIALG_1:def 18;

      Kf is closed

      proof

        let x be Element of Kf;

        x in Kf;

        then

         A3: ex x9 be Element of X st x = x9 & (f . x9) = ( 0. X9);

        (f . (x ` )) = ((f . ( 0. X)) \ (f . x)) by Def6;

        then (f . (x ` )) = (( 0. X9) ` ) by A3, Th35;

        then (f . (x ` )) = ( 0. X9) by BCIALG_1:def 5;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      let X, X9, f;

      cluster ( Ker f) -> closed;

      coherence by Th41;

    end

    theorem :: BCIALG_6:42

    

     Th42: f is onto implies for c be Element of X9 holds ex x st c = (f . x)

    proof

      

       A1: for c be set holds c in ( rng f) iff ex x st c = (f . x)

      proof

        let c be set;

        thus c in ( rng f) implies ex x st c = (f . x)

        proof

          assume c in ( rng f);

          then

          consider y be object such that

           A2: y in ( dom f) and

           A3: (f . y) = c by FUNCT_1:def 3;

          reconsider y as Element of X by A2;

          take y;

          thus thesis by A3;

        end;

        given x such that

         A4: c = (f . x);

        the carrier of X = ( dom f) by FUNCT_2:def 1;

        hence thesis by A4, FUNCT_1:def 3;

      end;

      assume f is onto;

      then ( rng f) = the carrier of X9 by FUNCT_2:def 3;

      hence thesis by A1;

    end;

    theorem :: BCIALG_6:43

    for a be Element of X st a is minimal holds (f . a) is minimal

    proof

      let a be Element of X;

      assume a is minimal;

      then (f . a) = (f . ((a ` ) ` )) by BCIALG_2: 29;

      then (f . a) = ((f . ( 0. X)) \ (f . (( 0. X) \ a))) by Def6;

      then (f . a) = ((f . ( 0. X)) \ ((f . ( 0. X)) \ (f . a))) by Def6;

      then (f . a) = (((f . ( 0. X)) \ (f . a)) ` ) by Th35;

      then (f . a) = (((f . a) ` ) ` ) by Th35;

      hence thesis by BCIALG_2: 29;

    end;

    theorem :: BCIALG_6:44

    for a be Element of ( AtomSet X), b be Element of ( AtomSet X9) st b = (f . a) holds (f .: ( BranchV a)) c= ( BranchV b)

    proof

      let a be Element of ( AtomSet X), b be Element of ( AtomSet X9) such that

       A1: b = (f . a);

      let y be object;

      assume y in (f .: ( BranchV a));

      then

      consider x be object such that x in ( dom f) and

       A2: x in ( BranchV a) and

       A3: y = (f . x) by FUNCT_1:def 6;

      

       A4: ex x1 be Element of X st x = x1 & a <= x1 by A2;

      reconsider x as Element of X by A2;

      ((f . a) \ (f . x)) = (f . (a \ x)) by Def6;

      then ((f . a) \ (f . x)) = (f . ( 0. X)) by A4;

      then ((f . a) \ (f . x)) = ( 0. X9) by Th35;

      then b <= (f . x) by A1;

      hence thesis by A3;

    end;

    theorem :: BCIALG_6:45

    

     Th45: A9 is Ideal of X9 implies (f " A9) is Ideal of X

    proof

      assume

       A1: A9 is Ideal of X9;

       A2:

      now

        let x,y be Element of X;

        assume that

         A3: (x \ y) in (f " A9) and

         A4: y in (f " A9);

        (f . (x \ y)) in A9 by A3, FUNCT_2: 38;

        then

         A5: ((f . x) \ (f . y)) in A9 by Def6;

        (f . y) in A9 by A4, FUNCT_2: 38;

        then (f . x) in A9 by A1, A5, BCIALG_1:def 18;

        hence x in (f " A9) by FUNCT_2: 38;

      end;

      ( 0. X9) in A9 by A1, BCIALG_1:def 18;

      then (f . ( 0. X)) in A9 by Th35;

      then ( 0. X) in (f " A9) by FUNCT_2: 38;

      hence thesis by A2, BCIALG_1:def 18;

    end;

    theorem :: BCIALG_6:46

    A9 is closed Ideal of X9 implies (f " A9) is closed Ideal of X

    proof

      assume

       A1: A9 is closed Ideal of X9;

      then

      reconsider XY = (f " A9) as Ideal of X by Th45;

      for y be Element of XY holds (y ` ) in XY

      proof

        let y be Element of XY;

        

         A2: (f . y) in A9 by FUNCT_2: 38;

        reconsider y as Element of X;

        ((f . y) ` ) in A9 by A1, A2, BCIALG_1:def 19;

        then ((f . ( 0. X)) \ (f . y)) in A9 by Th35;

        then (f . (y ` )) in A9 by Def6;

        hence thesis by FUNCT_2: 38;

      end;

      hence thesis by BCIALG_1:def 19;

    end;

    theorem :: BCIALG_6:47

    

     Th47: f is onto implies (f .: I) is Ideal of X9

    proof

      ( 0. X) in the carrier of X;

      then

       A1: ( 0. X) in ( dom f) by FUNCT_2:def 1;

      ( 0. X) in I & (f . ( 0. X)) = ( 0. X9) by Th35, BCIALG_1:def 18;

      then

      reconsider imaf = (f .: I) as non empty Subset of X9 by A1, FUNCT_1:def 6;

      ( 0. X) in the carrier of X;

      then

       A2: ( 0. X) in ( dom f) by FUNCT_2:def 1;

      assume

       A3: f is onto;

      

       A4: for x,y be Element of X9 st (x \ y) in imaf & y in imaf holds x in imaf

      proof

        let x,y be Element of X9;

        assume that

         A5: (x \ y) in imaf and

         A6: y in imaf;

        consider y9 be object such that

         A7: y9 in ( dom f) and

         A8: y9 in I and

         A9: y = (f . y9) by A6, FUNCT_1:def 6;

        consider yy be Element of X such that

         A10: (f . yy) = x by A3, Th42;

        consider z be object such that

         A11: z in ( dom f) and

         A12: z in I and

         A13: (x \ y) = (f . z) by A5, FUNCT_1:def 6;

        reconsider y9, z as Element of X by A7, A11;

        set u = (yy \ ((yy \ y9) \ z));

        (((yy \ y9) \ ((yy \ y9) \ z)) \ z) = ( 0. X) by BCIALG_1: 1;

        then ((u \ y9) \ z) = ( 0. X) by BCIALG_1: 7;

        then ((u \ y9) \ z) in I by BCIALG_1:def 18;

        then (u \ y9) in I by A12, BCIALG_1:def 18;

        then

         A14: u in I by A8, BCIALG_1:def 18;

        u in the carrier of X;

        then u in ( dom f) by FUNCT_2:def 1;

        then [u, (f . u)] in f by FUNCT_1: 1;

        then (f . (yy \ ((yy \ y9) \ z))) in (f .: I) by A14, RELAT_1:def 13;

        then ((f . yy) \ (f . ((yy \ y9) \ z))) in (f .: I) by Def6;

        then ((f . yy) \ ((f . (yy \ y9)) \ (f . z))) in (f .: I) by Def6;

        then ((f . yy) \ ((x \ y) \ (x \ y))) in (f .: I) by A9, A13, A10, Def6;

        then ((f . yy) \ ( 0. X9)) in (f .: I) by BCIALG_1:def 5;

        hence thesis by A10, BCIALG_1: 2;

      end;

      ( 0. X) in I & (f . ( 0. X)) = ( 0. X9) by Th35, BCIALG_1:def 18;

      then ( 0. X9) in imaf by A2, FUNCT_1:def 6;

      hence thesis by A4, BCIALG_1:def 18;

    end;

    theorem :: BCIALG_6:48

    f is onto implies (f .: CI) is closed Ideal of X9

    proof

      assume f is onto;

      then

      reconsider Kf = (f .: CI) as Ideal of X9 by Th47;

      now

        let x9 be Element of Kf;

        consider x be object such that x in ( dom f) and

         A1: x in CI and

         A2: x9 = (f . x) by FUNCT_1:def 6;

        reconsider x as Element of CI by A1;

        (x ` ) in the carrier of X;

        then (x ` ) in ( dom f) by FUNCT_2:def 1;

        then (x ` ) in CI & [(x ` ), (f . (x ` ))] in f by BCIALG_1:def 19, FUNCT_1: 1;

        then (f . (x ` )) in (f .: CI) by RELAT_1:def 13;

        then ((f . ( 0. X)) \ (f . x)) in (f .: CI) by Def6;

        hence (x9 ` ) in Kf by A2, Th35;

      end;

      hence thesis by BCIALG_1:def 19;

    end;

    definition

      let X,X9 be BCI-algebra;

      :: BCIALG_6:def9

      pred X,X9 are_isomorphic means ex f be BCI-homomorphism of X, X9 st f is bijective;

    end

    registration

      let X;

      let I be Ideal of X, RI be I-congruence of X, I;

      cluster (X ./. RI) -> strict being_B being_C being_I being_BCI-4;

      coherence ;

    end

    definition

      let X;

      let I be Ideal of X, RI be I-congruence of X, I;

      :: BCIALG_6:def10

      func nat_hom RI -> BCI-homomorphism of X, (X ./. RI) means

      : Def10: for x holds (it . x) = ( Class (RI,x));

      existence

      proof

        defpred P[ Element of X, set] means $2 = ( Class (RI,$1));

        

         A1: for x be Element of X holds ex y be Element of (X ./. RI) st P[x, y]

        proof

          let x be Element of X;

          reconsider y = ( Class (RI,x)) as Element of (X ./. RI) by EQREL_1:def 3;

          take y;

          thus thesis;

        end;

        consider f be Function of X, (X ./. RI) such that

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

        now

          let a,b be Element of X;

          (f . a) = ( Class (RI,a)) & (f . b) = ( Class (RI,b)) by A2;

          then ((f . a) \ (f . b)) = ( Class (RI,(a \ b))) by BCIALG_2:def 17;

          hence ((f . a) \ (f . b)) = (f . (a \ b)) by A2;

        end;

        then

        reconsider f as BCI-homomorphism of X, (X ./. RI) by Def6;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let f,g be BCI-homomorphism of X, (X ./. RI);

        assume that

         A3: for x be Element of X holds (f . x) = ( Class (RI,x)) and

         A4: for x be Element of X holds (g . x) = ( Class (RI,x));

        now

          let x be Element of X;

          (f . x) = ( Class (RI,x)) by A3;

          hence (f . x) = (g . x) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    begin

    theorem :: BCIALG_6:49

    ( nat_hom RI) is onto

    proof

      set f = ( nat_hom RI);

      set Y = (X ./. RI);

      reconsider Y as BCI-algebra;

      reconsider f as BCI-homomorphism of X, Y;

      for y be object st y in the carrier of Y holds ex x be object st x in the carrier of X & y = (f . x)

      proof

        let y be object;

        assume

         A1: y in the carrier of Y;

        then

        reconsider y as Element of Y;

        consider x be object such that

         A2: x in the carrier of X and

         A3: y = ( Class (RI,x)) by A1, EQREL_1:def 3;

        take x;

        thus thesis by A2, A3, Def10;

      end;

      then ( rng f) = the carrier of Y by FUNCT_2: 10;

      hence thesis by FUNCT_2:def 3;

    end;

    theorem :: BCIALG_6:50

    

     Th50: I = ( Ker f) implies ex h be BCI-homomorphism of (X ./. RI), X9 st f = (h * ( nat_hom RI)) & h is one-to-one

    proof

      set J = (X ./. RI);

      defpred P[ set, set] means for a be Element of X st $1 = ( Class (RI,a)) holds $2 = (f . a);

      

       A1: ( dom ( nat_hom RI)) = the carrier of X by FUNCT_2:def 1;

      assume

       A2: I = ( Ker f);

      

       A3: for x be Element of J holds ex y be Element of X9 st P[x, y]

      proof

        let x be Element of J;

        x in ( Class RI);

        then

        consider y be object such that

         A4: y in the carrier of X and

         A5: x = ( Class (RI,y)) by EQREL_1:def 3;

        reconsider y as Element of X by A4;

        reconsider t = (f . y) as Element of X9;

        take t;

        let a be Element of X;

        assume x = ( Class (RI,a));

        then y in ( Class (RI,a)) by A5, EQREL_1: 23;

        then

         A6: [a, y] in RI by EQREL_1: 18;

        then (y \ a) in ( Ker f) by A2, BCIALG_2:def 12;

        then ex x2 be Element of X st (y \ a) = x2 & (f . x2) = ( 0. X9);

        then

         A7: ((f . y) \ (f . a)) = ( 0. X9) by Def6;

        (a \ y) in ( Ker f) by A2, A6, BCIALG_2:def 12;

        then ex x1 be Element of X st (a \ y) = x1 & (f . x1) = ( 0. X9);

        then ((f . a) \ (f . y)) = ( 0. X9) by Def6;

        hence thesis by A7, BCIALG_1:def 7;

      end;

      consider h be Function of J, X9 such that

       A8: for x be Element of J holds P[x, (h . x)] from FUNCT_2:sch 3( A3);

      now

        let a,b be Element of J;

        a in ( Class RI);

        then

        consider a1 be object such that

         A9: a1 in the carrier of X and

         A10: a = ( Class (RI,a1)) by EQREL_1:def 3;

        b in ( Class RI);

        then

        consider b1 be object such that

         A11: b1 in the carrier of X and

         A12: b = ( Class (RI,b1)) by EQREL_1:def 3;

        reconsider a1, b1 as Element of X by A9, A11;

        

         A13: (a \ b) = ( Class (RI,(a1 \ b1))) by A10, A12, BCIALG_2:def 17;

        

         A14: (h . b) = (f . b1) by A8, A12;

        (h . a) = (f . a1) by A8, A10;

        then ((h . a) \ (h . b)) = (f . (a1 \ b1)) by A14, Def6;

        hence ((h . a) \ (h . b)) = (h . (a \ b)) by A8, A13;

      end;

      then

      reconsider h as BCI-homomorphism of (X ./. RI), X9 by Def6;

      

       A15: h is one-to-one

      proof

        let y1,y2 be object;

        assume that

         A16: y1 in ( dom h) & y2 in ( dom h) and

         A17: (h . y1) = (h . y2);

        reconsider S = y1, T = y2 as Element of J by A16;

        S in ( Class RI);

        then

        consider a1 be object such that

         A18: a1 in the carrier of X and

         A19: S = ( Class (RI,a1)) by EQREL_1:def 3;

        T in ( Class RI);

        then

        consider b1 be object such that

         A20: b1 in the carrier of X and

         A21: T = ( Class (RI,b1)) by EQREL_1:def 3;

        reconsider a1, b1 as Element of X by A18, A20;

        

         A22: (h . T) = (f . b1) by A8, A21;

        

         A23: (h . S) = (f . a1) by A8, A19;

        then ((f . b1) \ (f . a1)) = ( 0. X9) by A17, A22, BCIALG_1:def 5;

        then (f . (b1 \ a1)) = ( 0. X9) by Def6;

        then

         A24: (b1 \ a1) in ( Ker f);

        ((f . a1) \ (f . b1)) = ( 0. X9) by A17, A23, A22, BCIALG_1:def 5;

        then (f . (a1 \ b1)) = ( 0. X9) by Def6;

        then (a1 \ b1) in ( Ker f);

        then [a1, b1] in RI by A2, A24, BCIALG_2:def 12;

        then b1 in ( Class (RI,a1)) by EQREL_1: 18;

        hence thesis by A19, A21, EQREL_1: 23;

      end;

      

       A25: ( dom f) = the carrier of X by FUNCT_2:def 1;

       A26:

      now

        let x be object;

        thus x in ( dom f) implies x in ( dom ( nat_hom RI)) & (( nat_hom RI) . x) in ( dom h)

        proof

          assume

           A27: x in ( dom f);

          hence x in ( dom ( nat_hom RI)) by A1;

          

           A28: ( dom h) = the carrier of (X ./. RI) by FUNCT_2:def 1;

          (( nat_hom RI) . x) in ( rng ( nat_hom RI)) by A1, A27, FUNCT_1:def 3;

          hence thesis by A28;

        end;

        assume that

         A29: x in ( dom ( nat_hom RI)) and (( nat_hom RI) . x) in ( dom h);

        thus x in ( dom f) by A25, A29;

      end;

      take h;

      now

        let x be object;

        assume x in ( dom f);

        then

        reconsider a = x as Element of X;

        (( nat_hom RI) . a) = ( Class (RI,a)) by Def10;

        hence (f . x) = (h . (( nat_hom RI) . x)) by A8;

      end;

      hence thesis by A15, A26, FUNCT_1: 10;

    end;

    ::$Canceled

    theorem :: BCIALG_6:52

    ( Ker ( nat_hom RK)) = K

    proof

      set h = ( nat_hom RK);

      set Y = (X ./. RK);

      thus ( Ker h) c= K

      proof

        let y be object;

        assume y in ( Ker h);

        then

        consider x be Element of X such that

         A1: y = x and

         A2: (h . x) = ( 0. Y);

        ( Class (RK,( 0. X))) = ( Class (RK,x)) by A2, Def10;

        then x in ( Class (RK,( 0. X))) by EQREL_1: 23;

        then [( 0. X), x] in RK by EQREL_1: 18;

        then (x \ ( 0. X)) in K by BCIALG_2:def 12;

        hence thesis by A1, BCIALG_1: 2;

      end;

      let y be object;

      assume

       A3: y in K;

      then

      reconsider x = y as Element of X;

      (x \ ( 0. X)) in K & (x ` ) in K by A3, BCIALG_1: 2, BCIALG_1:def 19;

      then [( 0. X), x] in RK by BCIALG_2:def 12;

      then x in ( Class (RK,( 0. X))) by EQREL_1: 18;

      then ( Class (RK,( 0. X))) = ( Class (RK,x)) by EQREL_1: 23;

      then (h . x) = ( 0. Y) by Def10;

      hence thesis;

    end;

    

     Lm4: the carrier of H9 = ( rng f) implies f is BCI-homomorphism of X, H9

    proof

      

       A1: the carrier of X = ( dom f) by FUNCT_2:def 1;

      assume the carrier of H9 = ( rng f);

      then

      reconsider h = f as Function of X, H9 by A1, RELSET_1: 4;

      now

        let a,b be Element of X;

        ((h . a) \ (h . b)) = ((f . a) \ (f . b)) by Th34;

        hence (h . (a \ b)) = ((h . a) \ (h . b)) by Def6;

      end;

      hence thesis by Def6;

    end;

    begin

    theorem :: BCIALG_6:53

    I = ( Ker f) & the carrier of H9 = ( rng f) implies ((X ./. RI),H9) are_isomorphic

    proof

      assume that

       A1: I = ( Ker f) and

       A2: the carrier of H9 = ( rng f);

      defpred P[ set, set] means for a be Element of X st $1 = ( Class (RI,a)) holds $2 = (f . a);

      set J = (X ./. RI);

      

       A3: for x be Element of J holds ex y be Element of H9 st P[x, y]

      proof

        let x be Element of J;

        x in ( Class RI);

        then

        consider y be object such that

         A4: y in the carrier of X and

         A5: x = ( Class (RI,y)) by EQREL_1:def 3;

        reconsider y as Element of X by A4;

        ( dom f) = the carrier of X by FUNCT_2:def 1;

        then

        reconsider t = (f . y) as Element of H9 by A2, FUNCT_1:def 3;

        take t;

        let a be Element of X;

        assume x = ( Class (RI,a));

        then y in ( Class (RI,a)) by A5, EQREL_1: 23;

        then

         A6: [a, y] in RI by EQREL_1: 18;

        then (y \ a) in ( Ker f) by A1, BCIALG_2:def 12;

        then ex x2 be Element of X st (y \ a) = x2 & (f . x2) = ( 0. X9);

        then

         A7: ((f . y) \ (f . a)) = ( 0. X9) by Def6;

        (a \ y) in ( Ker f) by A1, A6, BCIALG_2:def 12;

        then ex x1 be Element of X st (a \ y) = x1 & (f . x1) = ( 0. X9);

        then ((f . a) \ (f . y)) = ( 0. X9) by Def6;

        hence thesis by A7, BCIALG_1:def 7;

      end;

      consider h be Function of J, H9 such that

       A8: for x be Element of J holds P[x, (h . x)] from FUNCT_2:sch 3( A3);

      now

        reconsider f as BCI-homomorphism of X, H9 by A2, Lm4;

        let a,b be Element of J;

        a in ( Class RI);

        then

        consider a1 be object such that

         A9: a1 in the carrier of X and

         A10: a = ( Class (RI,a1)) by EQREL_1:def 3;

        b in ( Class RI);

        then

        consider b1 be object such that

         A11: b1 in the carrier of X and

         A12: b = ( Class (RI,b1)) by EQREL_1:def 3;

        reconsider a1, b1 as Element of X by A9, A11;

        

         A13: (a \ b) = ( Class (RI,(a1 \ b1))) by A10, A12, BCIALG_2:def 17;

        

         A14: (h . b) = (f . b1) by A8, A12;

        (h . a) = (f . a1) by A8, A10;

        then ((h . a) \ (h . b)) = (f . (a1 \ b1)) by A14, Def6;

        hence ((h . a) \ (h . b)) = (h . (a \ b)) by A8, A13;

      end;

      then

      reconsider h as BCI-homomorphism of (X ./. RI), H9 by Def6;

      

       A15: h is one-to-one

      proof

        let y1,y2 be object;

        assume that

         A16: y1 in ( dom h) & y2 in ( dom h) and

         A17: (h . y1) = (h . y2);

        reconsider y1, y2 as Element of J by A16;

        y1 in ( Class RI);

        then

        consider a1 be object such that

         A18: a1 in the carrier of X and

         A19: y1 = ( Class (RI,a1)) by EQREL_1:def 3;

        y2 in ( Class RI);

        then

        consider b1 be object such that

         A20: b1 in the carrier of X and

         A21: y2 = ( Class (RI,b1)) by EQREL_1:def 3;

        reconsider a1, b1 as Element of X by A18, A20;

        

         A22: (h . y2) = (f . b1) by A8, A21;

        

         A23: (h . y1) = (f . a1) by A8, A19;

        then ((f . b1) \ (f . a1)) = ( 0. X9) by A17, A22, BCIALG_1:def 5;

        then (f . (b1 \ a1)) = ( 0. X9) by Def6;

        then

         A24: (b1 \ a1) in ( Ker f);

        ((f . a1) \ (f . b1)) = ( 0. X9) by A17, A23, A22, BCIALG_1:def 5;

        then (f . (a1 \ b1)) = ( 0. X9) by Def6;

        then (a1 \ b1) in ( Ker f);

        then [a1, b1] in RI by A1, A24, BCIALG_2:def 12;

        then b1 in ( Class (RI,a1)) by EQREL_1: 18;

        hence thesis by A19, A21, EQREL_1: 23;

      end;

      the carrier of H9 c= ( rng h)

      proof

        let y be object;

        

         A25: the carrier of J = ( dom h) by FUNCT_2:def 1;

        assume y in the carrier of H9;

        then

        consider x be object such that

         A26: x in ( dom f) and

         A27: y = (f . x) by A2, FUNCT_1:def 3;

        reconsider S = ( Class (RI,x)) as Element of J by A26, EQREL_1:def 3;

        (h . S) = (f . x) by A8, A26;

        hence thesis by A27, A25, FUNCT_1:def 3;

      end;

      then ( rng h) = the carrier of H9;

      then h is onto by FUNCT_2:def 3;

      hence thesis by A15;

    end;

    theorem :: BCIALG_6:54

    

     Th53: I = ( Ker f) & f is onto implies ((X ./. RI),X9) are_isomorphic

    proof

      assume that

       A1: I = ( Ker f) and

       A2: f is onto;

      consider h be BCI-homomorphism of (X ./. RI), X9 such that

       A3: f = (h * ( nat_hom RI)) and

       A4: h is one-to-one by A1, Th50;

      for y be object st y in the carrier of X9 holds ex z be object st z in the carrier of (X ./. RI) & (h . z) = y

      proof

        let y be object;

        assume y in the carrier of X9;

        then y in ( rng f) by A2, FUNCT_2:def 3;

        then

        consider x be object such that

         A5: x in ( dom f) and

         A6: y = (f . x) by FUNCT_1:def 3;

        take (( nat_hom RI) . x);

        

         A7: ( dom ( nat_hom RI)) = the carrier of X by FUNCT_2:def 1;

        then (( nat_hom RI) . x) in ( rng ( nat_hom RI)) by A5, FUNCT_1:def 3;

        hence thesis by A3, A5, A6, A7, FUNCT_1: 13;

      end;

      then ( rng h) = the carrier of X9 by FUNCT_2: 10;

      then h is onto by FUNCT_2:def 3;

      hence thesis by A4;

    end;

    begin

    definition

      let X, G, K, RK;

      :: BCIALG_6:def11

      func Union (G,RK) -> non empty Subset of X equals ( union { ( Class (RK,a)) where a be Element of G : ( Class (RK,a)) in the carrier of (X ./. RK) });

      correctness

      proof

        set Z2 = { ( Class (RK,a)) where a be Element of G : ( Class (RK,a)) in the carrier of (X ./. RK) };

        set Z1 = ( union { ( Class (RK,a)) where a be Element of G : ( Class (RK,a)) in the carrier of (X ./. RK) });

         A1:

        now

          let x be object;

          assume x in Z1;

          then

          consider g be set such that

           A2: x in g and

           A3: g in Z2 by TARSKI:def 4;

          ex a be Element of G st g = ( Class (RK,a)) & ( Class (RK,a)) in the carrier of (X ./. RK) by A3;

          hence x in the carrier of X by A2;

        end;

        ( 0. X) = ( 0. G) by BCIALG_1:def 10;

        then

         A4: ( Class (RK,( 0. X))) in Z2;

         [( 0. X), ( 0. X)] in RK by EQREL_1: 5;

        then ( 0. X) in ( Class (RK,( 0. X))) by EQREL_1: 18;

        hence thesis by A4, A1, TARSKI:def 3, TARSKI:def 4;

      end;

    end

    

     Lm5: for w be Element of ( Union (G,RK)) holds ex a be Element of G st w in ( Class (RK,a))

    proof

      set Z2 = { ( Class (RK,a)) where a be Element of G : ( Class (RK,a)) in the carrier of (X ./. RK) };

      let w be Element of ( Union (G,RK));

      consider g be set such that

       A1: w in g and

       A2: g in Z2 by TARSKI:def 4;

      consider a be Element of G such that

       A3: g = ( Class (RK,a)) and ( Class (RK,a)) in the carrier of (X ./. RK) by A2;

      take a;

      thus thesis by A1, A3;

    end;

    definition

      let X, G, K, RK;

      :: BCIALG_6:def12

      func HKOp (G,RK) -> BinOp of ( Union (G,RK)) means

      : Def12: for w1,w2 be Element of ( Union (G,RK)) holds for x,y be Element of X st w1 = x & w2 = y holds (it . (w1,w2)) = (x \ y);

      existence

      proof

        defpred P[ Element of ( Union (G,RK)), Element of ( Union (G,RK)), set] means for x, y st $1 = x & $2 = y holds $3 = (x \ y);

        

         A1: for w1,w2 be Element of ( Union (G,RK)) holds ex v be Element of ( Union (G,RK)) st P[w1, w2, v]

        proof

          let w1,w2 be Element of ( Union (G,RK));

          consider a be Element of G such that

           A2: w1 in ( Class (RK,a)) by Lm5;

          

           A3: [a, w1] in RK by A2, EQREL_1: 18;

          consider b be Element of G such that

           A4: w2 in ( Class (RK,b)) by Lm5;

          the carrier of G c= the carrier of X by BCIALG_1:def 10;

          then

          reconsider a1 = a, b1 = b as Element of X;

          ( Class (RK,(a1 \ b1))) in the carrier of (X ./. RK) by EQREL_1:def 3;

          then ( Class (RK,(a \ b))) in the carrier of (X ./. RK) by Th34;

          then

           A5: ( Class (RK,(a \ b))) in { ( Class (RK,c)) where c be Element of G : ( Class (RK,c)) in the carrier of (X ./. RK) };

          

           A6: [b, w2] in RK by A4, EQREL_1: 18;

          reconsider w1, w2 as Element of X;

           [(a1 \ b1), (w1 \ w2)] in RK by A3, A6, BCIALG_2:def 9;

          then (w1 \ w2) in ( Class (RK,(a1 \ b1))) by EQREL_1: 18;

          then (w1 \ w2) in ( Class (RK,(a \ b))) by Th34;

          then

          reconsider C = (w1 \ w2) as Element of ( Union (G,RK)) by A5, TARSKI:def 4;

          take C;

          thus thesis;

        end;

        thus ex B be BinOp of ( Union (G,RK)) st for w1,w2 be Element of ( Union (G,RK)) holds P[w1, w2, (B . (w1,w2))] from BINOP_1:sch 3( A1);

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( Union (G,RK));

        assume

         A7: for w1,w2 be Element of ( Union (G,RK)) holds for x,y be Element of X st w1 = x & w2 = y holds (o1 . (w1,w2)) = (x \ y);

        assume

         A8: for w1,w2 be Element of ( Union (G,RK)) holds for x,y be Element of X st w1 = x & w2 = y holds (o2 . (w1,w2)) = (x \ y);

        now

          let w1,w2 be Element of ( Union (G,RK));

          (o1 . (w1,w2)) = (w1 \ w2) by A7;

          hence (o1 . (w1,w2)) = (o2 . (w1,w2)) by A8;

        end;

        hence thesis;

      end;

    end

    definition

      let X, G, K, RK;

      :: BCIALG_6:def13

      func zeroHK (G,RK) -> Element of ( Union (G,RK)) equals ( 0. X);

      coherence

      proof

        

         A1: ( 0. G) = ( 0. X) by BCIALG_1:def 10;

        then ( 0. G) in ( Class (RK,( 0. G))) & ( Class (RK,( 0. G))) in { ( Class (RK,c)) where c be Element of G : ( Class (RK,c)) in the carrier of (X ./. RK) } by EQREL_1: 20;

        hence thesis by A1, TARSKI:def 4;

      end;

    end

    definition

      let X, G, K, RK;

      :: BCIALG_6:def14

      func HK (G,RK) -> BCIStr_0 equals BCIStr_0 (# ( Union (G,RK)), ( HKOp (G,RK)), ( zeroHK (G,RK)) #);

      coherence ;

    end

    registration

      let X, G, K, RK;

      cluster ( HK (G,RK)) -> non empty;

      coherence ;

    end

    definition

      let X, G, K, RK;

      let w1,w2 be Element of ( Union (G,RK));

      :: BCIALG_6:def15

      func w1 \ w2 -> Element of ( Union (G,RK)) equals (( HKOp (G,RK)) . (w1,w2));

      coherence ;

    end

    theorem :: BCIALG_6:55

    

     Th54: ( HK (G,RK)) is BCI-algebra

    proof

      reconsider IT = ( HK (G,RK)) as non empty BCIStr_0;

      

       A1: IT is being_BCI-4

      proof

        let x,y be Element of IT;

        reconsider x1 = x, y1 = y as Element of ( Union (G,RK));

        reconsider x2 = x1, y2 = y1 as Element of X;

        assume (x \ y) = ( 0. IT) & (y \ x) = ( 0. IT);

        then (x2 \ y2) = ( 0. X) & (y2 \ x2) = ( 0. X) by Def12;

        hence thesis by BCIALG_1:def 7;

      end;

       A2:

      now

        let x,y,z be Element of IT;

        reconsider x1 = x, y1 = y, z1 = z as Element of ( Union (G,RK));

        reconsider x2 = x1, y2 = y1, z2 = z1 as Element of X;

        (x2 \ y2) = (x1 \ y1) & (z2 \ y2) = (z1 \ y1) by Def12;

        then

         A3: ((x2 \ y2) \ (z2 \ y2)) = ((x1 \ y1) \ (z1 \ y1)) by Def12;

        (x2 \ z2) = (x1 \ z1) by Def12;

        then (((x2 \ y2) \ (z2 \ y2)) \ (x2 \ z2)) = (((x1 \ y1) \ (z1 \ y1)) \ (x1 \ z1)) by A3, Def12;

        hence (((x \ y) \ (z \ y)) \ (x \ z)) = ( 0. IT) by BCIALG_1:def 3;

      end;

      

       A4: IT is being_C

      proof

        let x,y,z be Element of IT;

        reconsider x1 = x, y1 = y, z1 = z as Element of ( Union (G,RK));

        reconsider x2 = x1, y2 = y1, z2 = z1 as Element of X;

        (x2 \ z2) = (x1 \ z1) by Def12;

        then

         A5: ((x2 \ z2) \ y2) = ((x1 \ z1) \ y1) by Def12;

        (x2 \ y2) = (x1 \ y1) by Def12;

        then ((x2 \ y2) \ z2) = ((x1 \ y1) \ z1) by Def12;

        then (((x2 \ y2) \ z2) \ ((x2 \ z2) \ y2)) = (((x1 \ y1) \ z1) \ ((x1 \ z1) \ y1)) by A5, Def12;

        hence thesis by BCIALG_1:def 4;

      end;

      IT is being_I

      proof

        let x be Element of IT;

        reconsider x1 = x as Element of ( Union (G,RK));

        reconsider x2 = x1 as Element of X;

        (x2 \ x2) = (x1 \ x1) by Def12;

        hence thesis by BCIALG_1:def 5;

      end;

      hence thesis by A2, A4, A1, BCIALG_1:def 3;

    end;

    registration

      let X, G, K, RK;

      cluster ( HK (G,RK)) -> strict being_B being_C being_I being_BCI-4;

      coherence by Th54;

    end

    theorem :: BCIALG_6:56

    

     Th55: ( HK (G,RK)) is SubAlgebra of X

    proof

      set IT = ( HK (G,RK));

      set V1 = the carrier of IT;

      reconsider D = V1 as non empty set;

      set A = (the InternalDiff of X || V1);

      set VV = the carrier of X;

      ( dom the InternalDiff of X) = [:VV, VV:] by FUNCT_2:def 1;

      then ( dom A) = ( [:VV, VV:] /\ [:V1, V1:]) by RELAT_1: 61;

      then

       A1: ( dom A) = [:D, D:] by XBOOLE_1: 28, ZFMISC_1: 96;

      for y be object holds y in D iff ex z be object st z in ( dom A) & y = (A . z)

      proof

        let y be object;

         A2:

        now

          given z be set such that

           A3: z in ( dom A) and

           A4: y = (A . z);

          consider x1,x2 be object such that

           A5: x1 in D & x2 in D and

           A6: z = [x1, x2] by A1, A3, ZFMISC_1:def 2;

          reconsider x1, x2 as Element of ( Union (G,RK)) by A5;

          reconsider v1 = x1, v2 = x2 as Element of VV;

          y = (v1 \ v2) by A3, A4, A6, FUNCT_1: 47;

          then y = (x1 \ x2) by Def12;

          hence y in D;

        end;

        y in D implies ex z be set st z in ( dom A) & y = (A . z)

        proof

          assume

           A7: y in D;

          then

          reconsider y1 = y, y2 = ( 0. IT) as Element of X;

          

           A8: [y, ( 0. IT)] in [:D, D:] by A7, ZFMISC_1: 87;

          

          then (A . [y, ( 0. IT)]) = (y1 \ y2) by FUNCT_1: 49

          .= y by BCIALG_1: 2;

          hence thesis by A1, A8;

        end;

        hence thesis by A2;

      end;

      then ( rng A) = D by FUNCT_1:def 3;

      then

      reconsider A as BinOp of V1 by A1, FUNCT_2:def 1, RELSET_1: 4;

      set B = the InternalDiff of IT;

      now

        let x,y be Element of V1;

        x in V1 & y in V1;

        then

        reconsider vx = x, vy = y as Element of VV;

         [x, y] in [:V1, V1:] by ZFMISC_1:def 2;

        then (A . (x,y)) = (vx \ vy) by FUNCT_1: 49;

        hence (A . (x,y)) = (B . (x,y)) by Def12;

      end;

      then ( 0. IT) = ( 0. X) & A = B;

      hence thesis by BCIALG_1:def 10;

    end;

    theorem :: BCIALG_6:57

    (the carrier of G /\ K) is closed Ideal of G

    proof

      set GK = (the carrier of G /\ K);

      

       A1: for x,y be Element of G st (x \ y) in GK & y in GK holds x in GK

      proof

        let x,y be Element of G;

        assume that

         A2: (x \ y) in GK and

         A3: y in GK;

        the carrier of G c= the carrier of X by BCIALG_1:def 10;

        then

        reconsider x1 = x, y1 = y as Element of X;

        (x \ y) in K by A2, XBOOLE_0:def 4;

        then

         A4: (x1 \ y1) in K by Th34;

        y1 in K by A3, XBOOLE_0:def 4;

        then x in K by A4, BCIALG_1:def 18;

        hence thesis by XBOOLE_0:def 4;

      end;

      

       A5: ( 0. G) = ( 0. X) by BCIALG_1:def 10;

      then

       A6: ( 0. G) in K by BCIALG_1:def 18;

      then

       A7: ( 0. G) in GK by XBOOLE_0:def 4;

      for x be object st x in GK holds x in the carrier of G by XBOOLE_0:def 4;

      then GK is non empty Subset of G by A6, TARSKI:def 3, XBOOLE_0:def 4;

      then

      reconsider GK as Ideal of G by A7, A1, BCIALG_1:def 18;

      for x be Element of GK holds (x ` ) in GK

      proof

        let x be Element of GK;

        

         A8: x in K by XBOOLE_0:def 4;

        then

        reconsider y = x as Element of X;

        (y ` ) in K by A8, BCIALG_1:def 19;

        then (x ` ) in K by A5, Th34;

        hence thesis by XBOOLE_0:def 4;

      end;

      hence thesis by BCIALG_1:def 19;

    end;

    theorem :: BCIALG_6:58

    for K1 be Ideal of ( HK (G,RK)), RK1 be I-congruence of ( HK (G,RK)), K1, I be Ideal of G, RI be I-congruence of G, I st RK1 = RK & I = (the carrier of G /\ K) holds ((G ./. RI),(( HK (G,RK)) ./. RK1)) are_isomorphic

    proof

      let K1 be Ideal of ( HK (G,RK)), RK1 be I-congruence of ( HK (G,RK)), K1, I be Ideal of G, RI be I-congruence of G, I;

      assume that

       A1: RK1 = RK and

       A2: I = (the carrier of G /\ K);

      defpred P[ Element of G, set] means $2 = ( Class (RK1,$1));

      

       A3: the carrier of G c= the carrier of ( HK (G,RK))

      proof

        let xx be object;

        assume xx in the carrier of G;

        then

        reconsider x = xx as Element of G;

        the carrier of G c= the carrier of X by BCIALG_1:def 10;

        then

         A4: x in the carrier of X;

        then ( Class (RK,x)) in the carrier of (X ./. RK) by EQREL_1:def 3;

        then

         A5: ( Class (RK,x)) in { ( Class (RK,a)) where a be Element of G : ( Class (RK,a)) in the carrier of (X ./. RK) };

         [x, x] in RK by A4, EQREL_1: 5;

        then x in ( Class (RK,x)) by EQREL_1: 18;

        hence thesis by A5, TARSKI:def 4;

      end;

      

       A6: for x be Element of G holds ex y be Element of (( HK (G,RK)) ./. RK1) st P[x, y]

      proof

        let x be Element of G;

        set y = ( Class (RK1,x));

        x in the carrier of G;

        then

        reconsider y as Element of (( HK (G,RK)) ./. RK1) by A3, EQREL_1:def 3;

        take y;

        thus thesis;

      end;

      consider f be Function of G, (( HK (G,RK)) ./. RK1) such that

       A7: for x be Element of G holds P[x, (f . x)] from FUNCT_2:sch 3( A6);

      now

        let a,b be Element of G;

        the carrier of G c= the carrier of X by BCIALG_1:def 10;

        then

        reconsider xa = a, xb = b as Element of X;

        a in the carrier of G & b in the carrier of G;

        then

        reconsider Wa = ( Class (RK1,a)), Wb = ( Class (RK1,b)) as Element of ( Class RK1) by A3, EQREL_1:def 3;

        reconsider a1 = a, b1 = b as Element of ( HK (G,RK)) by A3;

        Wa = (f . a) & Wb = (f . b) by A7;

        then

         A8: ((f . a) \ (f . b)) = ( Class (RK1,(a1 \ b1))) by BCIALG_2:def 17;

        ( HK (G,RK)) is SubAlgebra of X by Th55;

        then (xa \ xb) = (a1 \ b1) by Th34;

        then ((f . a) \ (f . b)) = ( Class (RK1,(a \ b))) by A8, Th34;

        hence (f . (a \ b)) = ((f . a) \ (f . b)) by A7;

      end;

      then

      reconsider f as BCI-homomorphism of G, (( HK (G,RK)) ./. RK1) by Def6;

      

       A9: ( Ker f) = I

      proof

        set X9 = (( HK (G,RK)) ./. RK1);

        thus ( Ker f) c= I

        proof

          let h be object;

          assume h in ( Ker f);

          then

          consider x be Element of G such that

           A10: h = x and

           A11: (f . x) = ( 0. X9);

          x in the carrier of G & the carrier of G c= the carrier of X by BCIALG_1:def 10;

          then

          reconsider x as Element of X;

          ( Class (RK,x)) = ( Class (RK,( 0. X))) by A1, A7, A11;

          then ( 0. X) in ( Class (RK,x)) by EQREL_1: 23;

          then [x, ( 0. X)] in RK by EQREL_1: 18;

          then

           A12: (x \ ( 0. X)) in K by BCIALG_2:def 12;

          x in K by A12, BCIALG_1:def 18;

          hence thesis by A2, A10, XBOOLE_0:def 4;

        end;

        let h be object;

        assume

         A13: h in I;

        then

        reconsider x = h as Element of X by A2;

        h in K by A2, A13, XBOOLE_0:def 4;

        then (x \ ( 0. X)) in K & (x ` ) in K by BCIALG_1: 2, BCIALG_1:def 19;

        then [x, ( 0. X)] in RK by BCIALG_2:def 12;

        then ( 0. X) in ( Class (RK,x)) by EQREL_1: 18;

        then ( Class (RK1,h)) = ( Class (RK1,( 0. X))) by A1, EQREL_1: 23;

        then (f . h) = ( 0. X9) by A7, A13;

        hence thesis by A13;

      end;

      now

        let y be object;

        y in the carrier of (( HK (G,RK)) ./. RK1) implies y in ( rng f)

        proof

          assume y in the carrier of (( HK (G,RK)) ./. RK1);

          then

          consider x be object such that

           A14: x in the carrier of ( HK (G,RK)) and

           A15: y = ( Class (RK1,x)) by EQREL_1:def 3;

          consider a be Element of G such that

           A16: x in ( Class (RK,a)) by A14, Lm5;

          a in the carrier of G & the carrier of G c= the carrier of X by BCIALG_1:def 10;

          then y = ( Class (RK1,a)) by A1, A15, A16, EQREL_1: 23;

          then

           A17: y = (f . a) by A7;

          ( dom f) = the carrier of G by FUNCT_2:def 1;

          hence thesis by A17, FUNCT_1:def 3;

        end;

        hence y in ( rng f) iff y in the carrier of (( HK (G,RK)) ./. RK1);

      end;

      then ( rng f) = the carrier of (( HK (G,RK)) ./. RK1) by TARSKI: 2;

      then f is onto by FUNCT_2:def 3;

      hence thesis by A9, Th53;

    end;