:: {BCI}-Homomorphisms
:: by Yuzhong Ding , Fuguo Ge and Chenglong Wu
::
:: Received August 26, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

definition
let D be set ;
let f be Function of NAT,D;
let n be Nat;
:: original:.
redefine funcf . n ->  Element of D;
coherence
 f . n is Element of D
proofend;
end;

definition
let G be non empty BCIStr_0 ;
func BCI-power G ->  Function of [: the carrier of G,NAT:], the carrier of G means :Def1: :: BCIALG_6:def 1
 for x being Element of G holds
( it . (x,0) = 0. G & ( for n being Element of NAT holds it . (x,(n + 1)) = x \ ((it . (x,n)) `) ) );
existence
 ex b1 being Function of [: the carrier of G,NAT:], the carrier of G st
for x being Element of G holds
( b1 . (x,0) = 0. G & ( for n being Element of NAT holds b1 . (x,(n + 1)) = x \ ((b1 . (x,n)) `) ) )
proofend;
uniqueness
 for b1, b2 being Function of [: the carrier of G,NAT:], the carrier of G st ( for x being Element of G holds
( b1 . (x,0) = 0. G & ( for n being Element of NAT holds b1 . (x,(n + 1)) = x \ ((b1 . (x,n)) `) ) ) ) & ( for x being Element of G holds
( b2 . (x,0) = 0. G & ( for n being Element of NAT holds b2 . (x,(n + 1)) = x \ ((b2 . (x,n)) `) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines BCI-power BCIALG_6:def_1_:_
 for G being non empty BCIStr_0
for b2 being Function of [: the carrier of G,NAT:], the carrier of G holds
( b2 = BCI-power G iff for x being Element of G holds
( b2 . (x,0) = 0. G & ( for n being Element of NAT holds b2 . (x,(n + 1)) = x \ ((b2 . (x,n)) `) ) ) );

definition
let X be BCI-algebra;
let i be Integer;
let x be Element of X;
funcx |^ i ->  Element of X equals :Def2: :: BCIALG_6:def 2
(BCI-power X) . (x,(abs i)) if  0 <= i
otherwise (BCI-power X) . ((x `),(abs i));
correctness
coherence
( ( 0 <= i implies (BCI-power X) . (x,(abs i)) is Element of X ) &amp; ( not 0 <= i implies (BCI-power X) . ((x `),(abs i)) is Element of X ) );
consistency
for b1 being Element of X holds verum;
;
end;

:: deftheorem Def2 defines |^ BCIALG_6:def_2_:_
 for X being BCI-algebra
for i being Integer
for x being Element of X holds
( ( 0 <= i implies x |^ i = (BCI-power X) . (x,(abs i)) ) &amp; ( not 0 <= i implies x |^ i = (BCI-power X) . ((x `),(abs i)) ) );

definition
let X be BCI-algebra;
let n be Nat;
let x be Element of X;
redefine func x |^ n equals :: BCIALG_6:def 3
(BCI-power X) . (x,n);
compatibility
 for b1 being Element of X holds
( b1 = x |^ n iff b1 = (BCI-power X) . (x,n) )
proofend;
end;

:: deftheorem  defines |^ BCIALG_6:def_3_:_
 for X being BCI-algebra
for n being Nat
for x being Element of X holds x |^ n = (BCI-power X) . (x,n);

theorem Th1: :: BCIALG_6:1
for X being BCI-algebra
for x being Element of X
for a, b being Element of AtomSet X holds a \ (x \ b) = b \ (x \ a)
proofend;

theorem Th2: :: BCIALG_6:2
for X being BCI-algebra
for x being Element of X
for n being Nat holds x |^ (n + 1) = x \ ((x |^ n) `)
proofend;

theorem Th3: :: BCIALG_6:3
for X being BCI-algebra
for x being Element of X holds x |^ 0 = 0. X by Def1;

theorem Th4: :: BCIALG_6:4
for X being BCI-algebra
for x being Element of X holds x |^ 1 = x
proofend;

theorem Th5: :: BCIALG_6:5
for X being BCI-algebra
for x being Element of X holds x |^ (- 1) = x `
proofend;

theorem :: BCIALG_6:6
for X being BCI-algebra
for x being Element of X holds x |^ 2 = x \ (x `)
proofend;

theorem Th7: :: BCIALG_6:7
for X being BCI-algebra
for n being Nat holds (0. X) |^ n = 0. X
proofend;

::P18-theorem 1.4.2(1-4)
theorem :: BCIALG_6:8
for X being BCI-algebra
for a being Element of AtomSet X holds (a |^ (- 1)) |^ (- 1) = a
proofend;

theorem :: BCIALG_6:9
for X being BCI-algebra
for x being Element of X
for n being Nat holds x |^ (- n) = ((x `) `) |^ (- n)
proofend;

theorem Th10: :: BCIALG_6:10
for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat holds (a `) |^ n = a |^ (- n)
proofend;

theorem :: BCIALG_6:11
for X being BCI-algebra
for x being Element of X
for n being Nat st x in BCK-part X &amp; n >= 1 holds
x |^ n = x
proofend;

theorem :: BCIALG_6:12
for X being BCI-algebra
for x being Element of X
for n being Nat st x in BCK-part X holds
x |^ (- n) = 0. X
proofend;

::P19 theorem 1.4.3
theorem Th13: :: BCIALG_6:13
for X being BCI-algebra
for a being Element of AtomSet X
for i being Integer holds a |^ i in AtomSet X
proofend;

theorem Th14: :: BCIALG_6:14
for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat holds (a |^ (n + 1)) ` = ((a |^ n) `) \ a
proofend;

Lm1:  for X being BCI-algebra
for a being Element of AtomSet X
for n, m being Nat holds a |^ (n + m) = (a |^ m) \ ((a |^ n) `)
proofend;

Lm2:  for X being BCI-algebra
for a being Element of AtomSet X
for m, n being Nat holds (a |^ m) |^ n = a |^ (m * n)
proofend;

theorem Th15: :: BCIALG_6:15
for X being BCI-algebra
for a, b being Element of AtomSet X
for n being Nat holds (a \ b) |^ n = (a |^ n) \ (b |^ n)
proofend;

theorem :: BCIALG_6:16
for X being BCI-algebra
for a, b being Element of AtomSet X
for n being Nat holds (a \ b) |^ (- n) = (a |^ (- n)) \ (b |^ (- n))
proofend;

theorem Th17: :: BCIALG_6:17
for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat holds (a `) |^ n = (a |^ n) `
proofend;

theorem Th18: :: BCIALG_6:18
for X being BCI-algebra
for x being Element of X
for n being Nat holds (x `) |^ n = (x |^ n) `
proofend;

theorem :: BCIALG_6:19
for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat holds (a `) |^ (- n) = (a |^ (- n)) `
proofend;

theorem Th20: :: BCIALG_6:20
for X being BCI-algebra
for x being Element of X
for a being Element of AtomSet X
for n being Nat st a = ((x `) `) |^ n holds
x |^ n in BranchV a
proofend;

theorem Th21: :: BCIALG_6:21
for X being BCI-algebra
for x being Element of X
for n being Nat holds (x |^ n) ` = (((x `) `) |^ n) `
proofend;

Lm3:  for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer st i > 0 &amp; j > 0 holds
(a |^ i) \ (a |^ j) = a |^ (i - j)
proofend;

theorem Th22: :: BCIALG_6:22
for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer holds (a |^ i) \ (a |^ j) = a |^ (i - j)
proofend;

::1.4.11
theorem Th23: :: BCIALG_6:23
for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer holds (a |^ i) |^ j = a |^ (i * j)
proofend;

theorem Th24: :: BCIALG_6:24
for X being BCI-algebra
for a being Element of AtomSet X
for i, j being Integer holds a |^ (i + j) = (a |^ i) \ ((a |^ j) `)
proofend;

definition
let X be BCI-algebra;
let x be Element of X;
attrx is finite-period  means :Def4: :: BCIALG_6:def 4
 ex n being Element of NAT st
( n <> 0 &amp; x |^ n in BCK-part X );
end;

:: deftheorem Def4 defines finite-period BCIALG_6:def_4_:_
 for X being BCI-algebra
for x being Element of X holds
( x is finite-period iff ex n being Element of NAT st
( n <> 0 &amp; x |^ n in BCK-part X ) );

theorem Th25: :: BCIALG_6:25
for X being BCI-algebra
for x being Element of X st x is finite-period holds
(x `) ` is finite-period
proofend;

definition
let X be BCI-algebra;
let x be Element of X;
assume A1: x is finite-period ;
func ord x ->  Element of NAT  means :Def5: :: BCIALG_6:def 5
( x |^ it in BCK-part X &amp; it <> 0 &amp; ( for m being Element of NAT st x |^ m in BCK-part X &amp; m <> 0 holds
it <= m ) );
existence
 ex b1 being Element of NAT st
( x |^ b1 in BCK-part X &amp; b1 <> 0 &amp; ( for m being Element of NAT st x |^ m in BCK-part X &amp; m <> 0 holds
b1 <= m ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st x |^ b1 in BCK-part X &amp; b1 <> 0 &amp; ( for m being Element of NAT st x |^ m in BCK-part X &amp; m <> 0 holds
b1 <= m ) &amp; x |^ b2 in BCK-part X &amp; b2 <> 0 &amp; ( for m being Element of NAT st x |^ m in BCK-part X &amp; m <> 0 holds
b2 <= m ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines ord BCIALG_6:def_5_:_
 for X being BCI-algebra
for x being Element of X st x is finite-period holds
for b3 being Element of NAT holds
( b3 = ord x iff ( x |^ b3 in BCK-part X &amp; b3 <> 0 &amp; ( for m being Element of NAT st x |^ m in BCK-part X &amp; m <> 0 holds
b3 <= m ) ) );

theorem Th26: :: BCIALG_6:26
for X being BCI-algebra
for a being Element of AtomSet X
for n being Nat st a is finite-period &amp; ord a = n holds
a |^ n = 0. X
proofend;

theorem :: BCIALG_6:27
for X being BCI-algebra holds
( X is BCK-algebra iff for x being Element of X holds
( x is finite-period &amp; ord x = 1 ) )
proofend;

theorem Th28: :: BCIALG_6:28
for X being BCI-algebra
for x being Element of X
for a being Element of AtomSet X st x is finite-period &amp; a is finite-period &amp; x in BranchV a holds
ord x = ord a
proofend;

theorem Th29: :: BCIALG_6:29
for X being BCI-algebra
for x being Element of X
for n, m being Nat st x is finite-period &amp; ord x = n holds
( x |^ m in BCK-part X iff n divides m )
proofend;

theorem :: BCIALG_6:30
for X being BCI-algebra
for x being Element of X
for m, n being Nat st x is finite-period &amp; x |^ m is finite-period &amp; ord x = n &amp; m > 0 holds
ord (x |^ m) = n div (m gcd n)
proofend;

theorem :: BCIALG_6:31
for X being BCI-algebra
for x being Element of X st x is finite-period &amp; x ` is finite-period holds
ord x = ord (x `)
proofend;

theorem :: BCIALG_6:32
for X being BCI-algebra
for x, y being Element of X
for a being Element of AtomSet X st x \ y is finite-period &amp; x in BranchV a &amp; y in BranchV a holds
ord (x \ y) = 1
proofend;

theorem :: BCIALG_6:33
for X being BCI-algebra
for x, y being Element of X
for a, b being Element of AtomSet X st a \ b is finite-period &amp; x is finite-period &amp; y is finite-period &amp; a is finite-period &amp; b is finite-period &amp; x in BranchV a &amp; y in BranchV b holds
ord (a \ b) divides (ord x) lcm (ord y)
proofend;

begin

theorem Th34: :: BCIALG_6:34
for X being BCI-algebra
for Y being SubAlgebra of X
for x, y being Element of X
for x9, y9 being Element of Y st x = x9 &amp; y = y9 holds
x \ y = x9 \ y9
proofend;

definition
let X, X9 be non empty BCIStr_0 ;
let f be Function of X,X9;
attrf is multiplicative  means :Def6: :: BCIALG_6:def 6
 for a, b being Element of X holds f . (a \ b) = (f . a) \ (f . b);
end;

:: deftheorem Def6 defines multiplicative BCIALG_6:def_6_:_
 for X, X9 being non empty BCIStr_0
for f being Function of X,X9 holds
( f is multiplicative iff for a, b being Element of X holds f . (a \ b) = (f . a) \ (f . b) );

registration
let X, X9 be BCI-algebra;
cluster Relation-like the carrier of X -defined the carrier of X9 -valued Function-like non empty V14( the carrier of X) quasi_total multiplicative for Element of bool [: the carrier of X, the carrier of X9:];
existence
 ex b1 being Function of X,X9 st b1 is multiplicative
proofend;
end;

definition
let X, X9 be BCI-algebra;
mode BCI-homomorphism of X,X9 is multiplicative Function of X,X9;
end;

definition
let X, X9 be BCI-algebra;
let f be BCI-homomorphism of X,X9;
attrf is isotonic  means :: BCIALG_6:def 7
 for x, y being Element of X st x <= y holds
f . x <= f . y;
end;

:: deftheorem  defines isotonic BCIALG_6:def_7_:_
 for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9 holds
( f is isotonic iff for x, y being Element of X st x <= y holds
f . x <= f . y );

definition
let X be BCI-algebra;
mode Endomorphism of X is BCI-homomorphism of X,X;
end;

definition
let X, X9 be BCI-algebra;
let f be BCI-homomorphism of X,X9;
func Ker f ->  set  equals :: BCIALG_6:def 8
 {  x where x is Element of X : f . x = 0. X9  }  ;
coherence
  {  x where x is Element of X : f . x = 0. X9  }  is set ;
end;

:: deftheorem  defines Ker BCIALG_6:def_8_:_
 for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9 holds Ker f =  {  x where x is Element of X : f . x = 0. X9  }  ;

theorem Th35: :: BCIALG_6:35
for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9 holds f . (0. X) = 0. X9
proofend;

registration
let X, X9 be BCI-algebra;
let f be BCI-homomorphism of X,X9;
cluster Ker f ->  non empty ;
coherence
 not Ker f is empty
proofend;
end;

theorem :: BCIALG_6:36
for X, X9 being BCI-algebra
for x, y being Element of X
for f being BCI-homomorphism of X,X9 st x <= y holds
f . x <= f . y
proofend;

theorem :: BCIALG_6:37
for X9, X being BCI-algebra
for f being BCI-homomorphism of X,X9 holds
( f is one-to-one iff Ker f = {(0. X)} )
proofend;

theorem :: BCIALG_6:38
for X9, X being BCI-algebra
for f being BCI-homomorphism of X,X9
for g being BCI-homomorphism of X9,X st f is bijective &amp; g = f " holds
g is bijective
proofend;

theorem :: BCIALG_6:39
for X9, X, Y being BCI-algebra
for f being BCI-homomorphism of X,X9
for h being BCI-homomorphism of X9,Y holds h * f is BCI-homomorphism of X,Y
proofend;

theorem :: BCIALG_6:40
for X9, X being BCI-algebra
for f being BCI-homomorphism of X,X9
for Z being SubAlgebra of X9 st the carrier of Z = rng f holds
f is BCI-homomorphism of X,Z
proofend;

theorem Th41: :: BCIALG_6:41
for X9, X being BCI-algebra
for f being BCI-homomorphism of X,X9 holds Ker f is closed Ideal of X
proofend;

registration
let X, X9 be BCI-algebra;
let f be BCI-homomorphism of X,X9;
cluster Ker f ->  closed for Ideal of X;
coherence
 for b1 being Ideal of X st b1 = Ker f holds
b1 is closed by Th41;
end;

theorem Th42: :: BCIALG_6:42
for X9, X being BCI-algebra
for f being BCI-homomorphism of X,X9 st f is onto holds
for c being Element of X9 ex x being Element of X st c = f . x
proofend;

::P75
theorem :: BCIALG_6:43
for X9, X being BCI-algebra
for f being BCI-homomorphism of X,X9
for a being Element of X st a is minimal holds
f . a is minimal
proofend;

theorem :: BCIALG_6:44
for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9
for a being Element of AtomSet X
for b being Element of AtomSet X9 st b = f . a holds
f .: (BranchV a) c= BranchV b
proofend;

::P76
theorem Th45: :: BCIALG_6:45
for X9, X being BCI-algebra
for A9 being non empty Subset of X9
for f being BCI-homomorphism of X,X9 st A9 is Ideal of X9 holds
f " A9 is Ideal of X
proofend;

theorem :: BCIALG_6:46
for X9, X being BCI-algebra
for A9 being non empty Subset of X9
for f being BCI-homomorphism of X,X9 st A9 is closed Ideal of X9 holds
f " A9 is closed Ideal of X
proofend;

theorem Th47: :: BCIALG_6:47
for X, X9 being BCI-algebra
for I being Ideal of X
for f being BCI-homomorphism of X,X9 st f is onto holds
f .: I is Ideal of X9
proofend;

theorem :: BCIALG_6:48
for X, X9 being BCI-algebra
for CI being closed Ideal of X
for f being BCI-homomorphism of X,X9 st f is onto holds
f .: CI is closed Ideal of X9
proofend;

definition
let X, X9 be BCI-algebra;
predX,X9 are_isomorphic  means :Def9: :: BCIALG_6:def 9
 ex f being BCI-homomorphism of X,X9 st f is bijective ;
end;

:: deftheorem Def9 defines are_isomorphic BCIALG_6:def_9_:_
 for X, X9 being BCI-algebra holds
( X,X9 are_isomorphic iff ex f being BCI-homomorphism of X,X9 st f is bijective );

registration
let X be BCI-algebra;
let I be Ideal of X;
let RI be I-congruence of X,I;
clusterX ./. RI ->  strict being_B being_C being_I being_BCI-4 ;
coherence
 ( X ./. RI is strict &amp; X ./. RI is being_B &amp; X ./. RI is being_C &amp; X ./. RI is being_I &amp; X ./. RI is being_BCI-4 ) ;
end;

definition
let X be BCI-algebra;
let I be Ideal of X;
let RI be I-congruence of X,I;
func nat_hom RI ->  BCI-homomorphism of X,(X ./. RI) means :Def10: :: BCIALG_6:def 10
 for x being Element of X holds it . x = Class (RI,x);
existence
 ex b1 being BCI-homomorphism of X,(X ./. RI) st
for x being Element of X holds b1 . x = Class (RI,x)
proofend;
uniqueness
 for b1, b2 being BCI-homomorphism of X,(X ./. RI) st ( for x being Element of X holds b1 . x = Class (RI,x) ) &amp; ( for x being Element of X holds b2 . x = Class (RI,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines nat_hom BCIALG_6:def_10_:_
 for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for b4 being BCI-homomorphism of X,(X ./. RI) holds
( b4 = nat_hom RI iff for x being Element of X holds b4 . x = Class (RI,x) );

begin

:: f
:: X--------->X'
:: | /
:: g| / h
:: | /
:: | /
:: | /
:: V /
:: X/Ker(f)
theorem :: BCIALG_6:49
for X being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I holds nat_hom RI is onto
proofend;

theorem Th50: :: BCIALG_6:50
for X, X9 being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for f being BCI-homomorphism of X,X9 st I = Ker f holds
ex h being BCI-homomorphism of (X ./. RI),X9 st
( f = h * (nat_hom RI) &amp; h is one-to-one )
proofend;

theorem :: BCIALG_6:51
for X, X9 being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for f being BCI-homomorphism of X,X9 st I = Ker f holds
ex h being BCI-homomorphism of (X ./. RI),X9 st
( f = h * (nat_hom RI) &amp; h is one-to-one ) by Th50;

theorem :: BCIALG_6:52
for X being BCI-algebra
for K being closed Ideal of X
for RK being I-congruence of X,K holds Ker (nat_hom RK) = K
proofend;

Lm4:  for X9, X being BCI-algebra
for H9 being SubAlgebra of X9
for f being BCI-homomorphism of X,X9 st the carrier of H9 = rng f holds
f is BCI-homomorphism of X,H9
proofend;

begin

theorem :: BCIALG_6:53
for X9, X being BCI-algebra
for H9 being SubAlgebra of X9
for I being Ideal of X
for RI being I-congruence of X,I
for f being BCI-homomorphism of X,X9 st I = Ker f &amp; the carrier of H9 = rng f holds
X ./. RI,H9 are_isomorphic
proofend;

theorem Th54: :: BCIALG_6:54
for X, X9 being BCI-algebra
for I being Ideal of X
for RI being I-congruence of X,I
for f being BCI-homomorphism of X,X9 st I = Ker f &amp; f is onto holds
X ./. RI,X9 are_isomorphic
proofend;

begin

definition
let X be BCI-algebra;
let G be SubAlgebra of X;
let K be closed Ideal of X;
let RK be I-congruence of X,K;
func Union (G,RK) ->  non empty Subset of X equals :: BCIALG_6:def 11
 union  {  (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK)  }  ;
correctness
coherence
union  {  (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK)  }  is non empty Subset of X;
proofend;
end;

:: deftheorem  defines Union BCIALG_6:def_11_:_
 for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K holds Union (G,RK) = union  {  (Class (RK,a)) where a is Element of G : Class (RK,a) in the carrier of (X ./. RK)  }  ;

Lm5:  for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K
for w being Element of Union (G,RK) ex a being Element of G st w in Class (RK,a)
proofend;

definition
let X be BCI-algebra;
let G be SubAlgebra of X;
let K be closed Ideal of X;
let RK be I-congruence of X,K;
func HKOp (G,RK) ->  BinOp of (Union (G,RK)) means :Def12: :: BCIALG_6:def 12
 for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x &amp; w2 = y holds
it . (w1,w2) = x \ y;
existence
 ex b1 being BinOp of (Union (G,RK)) st
for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x &amp; w2 = y holds
b1 . (w1,w2) = x \ y
proofend;
uniqueness
 for b1, b2 being BinOp of (Union (G,RK)) st ( for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x &amp; w2 = y holds
b1 . (w1,w2) = x \ y ) &amp; ( for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x &amp; w2 = y holds
b2 . (w1,w2) = x \ y ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines HKOp BCIALG_6:def_12_:_
 for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K
for b5 being BinOp of (Union (G,RK)) holds
( b5 = HKOp (G,RK) iff for w1, w2 being Element of Union (G,RK)
for x, y being Element of X st w1 = x &amp; w2 = y holds
b5 . (w1,w2) = x \ y );

definition
let X be BCI-algebra;
let G be SubAlgebra of X;
let K be closed Ideal of X;
let RK be I-congruence of X,K;
func zeroHK (G,RK) ->  Element of Union (G,RK) equals :: BCIALG_6:def 13
 0. X;
coherence
 0. X is Element of Union (G,RK)
proofend;
end;

:: deftheorem  defines zeroHK BCIALG_6:def_13_:_
 for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K holds zeroHK (G,RK) = 0. X;

definition
let X be BCI-algebra;
let G be SubAlgebra of X;
let K be closed Ideal of X;
let RK be I-congruence of X,K;
func HK (G,RK) ->  BCIStr_0  equals :: BCIALG_6:def 14
 BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #);
coherence
 BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #) is BCIStr_0 ;
end;

:: deftheorem  defines HK BCIALG_6:def_14_:_
 for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K holds HK (G,RK) = BCIStr_0(# (Union (G,RK)),(HKOp (G,RK)),(zeroHK (G,RK)) #);

registration
let X be BCI-algebra;
let G be SubAlgebra of X;
let K be closed Ideal of X;
let RK be I-congruence of X,K;
cluster HK (G,RK) ->  non empty ;
coherence
 not HK (G,RK) is empty ;
end;

definition
let X be BCI-algebra;
let G be SubAlgebra of X;
let K be closed Ideal of X;
let RK be I-congruence of X,K;
let w1, w2 be Element of Union (G,RK);
funcw1 \ w2 ->  Element of Union (G,RK) equals :: BCIALG_6:def 15
(HKOp (G,RK)) . (w1,w2);
coherence
 (HKOp (G,RK)) . (w1,w2) is Element of Union (G,RK) ;
end;

:: deftheorem  defines \ BCIALG_6:def_15_:_
 for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K
for w1, w2 being Element of Union (G,RK) holds w1 \ w2 = (HKOp (G,RK)) . (w1,w2);

theorem Th55: :: BCIALG_6:55
for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K holds HK (G,RK) is BCI-algebra
proofend;

registration
let X be BCI-algebra;
let G be SubAlgebra of X;
let K be closed Ideal of X;
let RK be I-congruence of X,K;
cluster HK (G,RK) ->  strict being_B being_C being_I being_BCI-4 ;
coherence
 ( HK (G,RK) is strict &amp; HK (G,RK) is being_B &amp; HK (G,RK) is being_C &amp; HK (G,RK) is being_I &amp; HK (G,RK) is being_BCI-4 ) by Th55;
end;

theorem Th56: :: BCIALG_6:56
for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K holds HK (G,RK) is SubAlgebra of X
proofend;

theorem :: BCIALG_6:57
for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X holds the carrier of G /\ K is closed Ideal of G
proofend;

theorem :: BCIALG_6:58
for X being BCI-algebra
for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K
for K1 being Ideal of HK (G,RK)
for RK1 being I-congruence of HK (G,RK),K1
for I being Ideal of G
for RI being I-congruence of G,I st RK1 = RK &amp; I = the carrier of G /\ K holds
G ./. RI,(HK (G,RK)) ./. RK1 are_isomorphic
proofend;