let X, X9 be BCI-algebra; :: 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:
set J = X ./. RI;
defpred S₁[ set , set ] means for a being 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 ; :: thesis:
A3: for x being Element of (X ./. RI) ex y being Element of X9 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;
reconsider t = f . y as Element of X9 ;
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 A2, 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 A2, 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),X9 such that
A8: for x being Element of (X ./. RI) holds S₁[x,h . x] from FUNCT_2:sch 3(A3);

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),X9 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 S = y1, T = y2 as Element of (X ./. RI) by A16;
S in Class RI ;
then consider a1 being 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 being object such that
A20: b1 in the carrier of X and
A21: T = Class (RI,b1) by EQREL_1:def 3;
reconsider a1 = a1, b1 = 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 y1 = y2 by A19, A21, EQREL_1:23; :: thesis:

end;

let x be object ; :: thesis:
thus ( x in dom f implies ( x in dom (nat_hom RI) & (nat_hom RI) . x in dom h ) ) :: thesis:

end;

end;

take h ; :: thesis:

let x be object ; :: thesis:
assume x in dom f ; :: thesis:
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; :: thesis:

end;