let X be BCI-algebra; :: thesis:
let G be SubAlgebra of X; :: thesis:
let K be closed Ideal of X; :: thesis:
let RK be I-congruence of X,K; :: thesis:
let K1 be Ideal of HK (G,RK); :: thesis:
let RK1 be I-congruence of HK (G,RK),K1; :: thesis:
let I be Ideal of G; :: thesis:
let RI be I-congruence of G,I; :: thesis:
assume that
A1: RK1 = RK and
A2: I = the carrier of G /\ K ; :: thesis:
defpred S₁[ Element of G, set ] means $2 = Class (RK1,$1);
A3: the carrier of G c= the carrier of (HK (G,RK))

let xx be object ; :: according to TARSKI:def 3 :: thesis:
assume xx in the carrier of G ; :: thesis:
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 is 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 xx in the carrier of (HK (G,RK)) by A5, TARSKI:def 4; :: thesis:

end;

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

let x be Element of G; :: thesis:
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 3;
take y ; :: thesis:
thus S₁[x,y] ; :: thesis:

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);

let a, b be Element of G; :: thesis:
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; :: thesis:

end;

then reconsider f = f as BCI-homomorphism of G,((HK (G,RK)) ./. RK1) by Def6;
A9: Ker f = I

set X9 = (HK (G,RK)) ./. RK1;
thus Ker f c= I :: according to XBOOLE_0:def 10 :: thesis:

let h be object ; :: according to TARSKI:def 3 :: thesis:
assume h in Ker f ; :: thesis:
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: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 h in I by A2, A10, XBOOLE_0:def 4; :: thesis:

end;

let h be object ; :: according to TARSKI:def 3 :: thesis:
assume A13: h in I ; :: thesis:
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. ((HK (G,RK)) ./. RK1) by A7, A13;
hence h in Ker f by A13; :: thesis:

end;

let y be object ; :: thesis:
( y in the carrier of ((HK (G,RK)) ./. RK1) implies y in rng f )

assume y in the carrier of ((HK (G,RK)) ./. RK1) ; :: thesis:
then consider x being 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 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:23;
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 3; :: thesis:

end;

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

end;