let X, X9 be BCI-algebra; :: thesis:
let H9 be SubAlgebra of X9; :: thesis:
let I be Ideal of X; :: thesis:
let RI be I-congruence of X,I; :: thesis:
let f be BCI-homomorphism of X,X9; :: thesis:
assume that
A1: I = Ker f and
A2: the carrier of H9 = rng f ; :: thesis:
defpred S₁[ set , set ] means for a being Element of X st $1 = Class (RI,a) holds
$2 = f . a;
set J = X ./. RI;
A3: for x being Element of (X ./. RI) ex y being Element of H9 st S₁[x,y]

let x be Element of (X ./. RI); :: thesis:
x in Class RI ;
then consider y being object such that
A4: y in the carrier of X and
A5: x = Class (RI,y) by EQREL_1:def 3;
reconsider y = 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 ; :: thesis:
let a be Element of X; :: thesis:
assume x = Class (RI,a) ; :: thesis:
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 being 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 being Element of X st
( a \ y = x1 & f . x1 = 0. X9 ) ;
then (f . a) \ (f . y) = 0. X9 by Def6;
hence t = f . a by A7, BCIALG_1:def 7; :: thesis:

end;

consider h being Function of (X ./. RI),H9 such that
A8: for x being Element of (X ./. RI) holds S₁[x,h . x] from FUNCT_2:sch 3(A3);

reconsider f = f as BCI-homomorphism of X,H9 by A2, Lm4;
let a, b be Element of (X ./. RI); :: thesis:
a in Class RI ;
then consider a1 being 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 being object such that
A11: b1 in the carrier of X and
A12: b = Class (RI,b1) by EQREL_1:def 3;
reconsider a1 = a1, b1 = 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; :: thesis:

end;

then reconsider h = h as BCI-homomorphism of (X ./. RI),H9 by Def6;
A15: h is one-to-one

let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A16: ( y1 in dom h & y2 in dom h ) and
A17: h . y1 = h . y2 ; :: thesis:
reconsider y1 = y1, y2 = y2 as Element of (X ./. RI) by A16;
y1 in Class RI ;
then consider a1 being 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 being object such that
A20: b1 in the carrier of X and
A21: y2 = Class (RI,b1) by EQREL_1:def 3;
reconsider a1 = a1, b1 = 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 y1 = y2 by A19, A21, EQREL_1:23; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
A25: the carrier of (X ./. RI) = dom h by FUNCT_2:def 1;
assume y in the carrier of H9 ; :: thesis:
then consider x being 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 (X ./. RI) by A26, EQREL_1:def 3;
h . S = f . x by A8, A26;
hence y in rng h by A27, A25, FUNCT_1:def 3; :: thesis:

end;