let X be BCI-algebra; :: thesis: 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 & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let G be SubAlgebra of X; :: thesis: 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 & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let K be closed Ideal of X; :: thesis: 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 & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let RK be I-congruence of X,K; :: thesis: 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 & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let K1 be Ideal of HK G,RK; :: thesis: 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 & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let RK1 be I-congruence of HK G,RK,K1; :: thesis: for I being Ideal of G
for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let I be Ideal of G; :: thesis: for RI being I-congruence of G,I st RK1 = RK & I = the carrier of G /\ K holds
G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
let RI be I-congruence of G,I; :: thesis: ( RK1 = RK & I = the carrier of G /\ K implies G ./. RI,(HK G,RK) ./. RK1 are_isomorphic )
assume that
A1: RK1 = RK and
A2: I = the carrier of G /\ K ; :: thesis: G ./. RI,(HK G,RK) ./. RK1 are_isomorphic
defpred S₁[ 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 set ; :: according to TARSKI:def 3 :: thesis: ( not xx in the carrier of G or xx in the carrier of (HK G,RK) )
assume xx in the carrier of G ; :: thesis: xx in the carrier of (HK G,RK)
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 by TARSKI:def 3;
then Class RK,x in the carrier of (X ./. RK) by EQREL_1:def 5;
then A5: Class RK,x in { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ;
[x,x] in RK by A4, EQREL_1:11;
then x in Class RK,x by EQREL_1:26;
hence xx in the carrier of (HK G,RK) by A5, TARSKI:def 4; :: thesis: verum

end;

A6: for x being Element of G ex y being Element of ((HK G,RK) ./. RK1) st S₁[x,y]

proof

let x be Element of G; :: thesis: ex y being Element of ((HK G,RK) ./. RK1) st S₁[x,y]
set y = Class RK1,x;
x in the carrier of G ;
then reconsider y = Class RK1,x as Element of ((HK G,RK) ./. RK1) by A3, EQREL_1:def 5;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] ; :: thesis: verum

end;

consider f being Function of G,((HK G,RK) ./. RK1) such that
A7: for x being Element of G holds S₁[x,f . x] from FUNCT_2:sch 3(A6);

now

let a, b be Element of G; :: thesis: f . (a \ b) = (f . a) \ (f . b)
the carrier of G c= the carrier of X by BCIALG_1:def 10;
then reconsider xa = a, xb = b as Element of X by TARSKI:def 3;
( 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 5;
( a in the carrier of G & b in the carrier of G ) ;
then 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 Th57;
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; :: thesis: verum

end;

then reconsider f = 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 :: according to XBOOLE_0:def 10 :: thesis: I c= Ker f

proof

let h be set ; :: according to TARSKI:def 3 :: thesis: ( not h in Ker f or h in I )
assume h in Ker f ; :: thesis: h in I
then consider x being Element of G such that
A10: h = x and
A11: f . x = 0. ((HK G,RK) ./. RK1) ;
( x in the carrier of G & the carrier of G c= the carrier of X ) by BCIALG_1:def 10;
then reconsider x = 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:31;
then [x,(0. X)] in RK by EQREL_1:26;
then A12: x \ (0. X) in K by BCIALG_2:def 12;
0. X in K by BCIALG_1:def 18;
then x in K by A12, BCIALG_1:def 18;
hence h in I by A2, A10, XBOOLE_0:def 4; :: thesis: verum

end;

let h be set ; :: according to TARSKI:def 3 :: thesis: ( not h in I or h in Ker f )
assume A13: h in I ; :: thesis: h in Ker f
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:26;
then Class RK1,h = Class RK1,(0. X) by A1, EQREL_1:31;
then f . h = 0. ((HK G,RK) ./. RK1) by A7, A13;
hence h in Ker f by A13; :: thesis: verum

end;

now

let y be set ; :: thesis: ( y in rng f iff y in the carrier of ((HK G,RK) ./. RK1) )
( 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) ; :: thesis: y in rng f
then consider x being set such that
A14: x in the carrier of (HK G,RK) and
A15: y = Class RK1,x by EQREL_1:def 5;
consider a being 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:31;
then A17: y = f . a by A7;
dom f = the carrier of G by FUNCT_2:def 1;
hence y in rng f by A17, FUNCT_1:def 5; :: thesis: verum

end;

hence ( y in rng f iff y in the carrier of ((HK G,RK) ./. RK1) ) ; :: thesis: verum

end;

then rng f = the carrier of ((HK G,RK) ./. RK1) by TARSKI:2;
then f is onto by FUNCT_2:def 3;
hence G ./. RI,(HK G,RK) ./. RK1 are_isomorphic by A9, Th55; :: thesis: verum