let X, X9 be BCI-algebra; :: thesis: 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 & f is onto holds
X ./. RI,X9 are_isomorphic
let I be Ideal of X; :: thesis: for RI being I-congruence of X,I
for f being BCI-homomorphism of X,X9 st I = Ker f & f is onto holds
X ./. RI,X9 are_isomorphic
let RI be I-congruence of X,I; :: thesis: for f being BCI-homomorphism of X,X9 st I = Ker f & f is onto holds
X ./. RI,X9 are_isomorphic
let f be BCI-homomorphism of X,X9; :: thesis: ( I = Ker f & f is onto implies X ./. RI,X9 are_isomorphic )
assume that
A1: I = Ker f and
A2: f is onto ; :: thesis: X ./. RI,X9 are_isomorphic
consider h being BCI-homomorphism of (X ./. RI),X9 such that
A3: f = h * (nat_hom RI) and
A4: h is one-to-one by A1, Th50;
for y being object st y in the carrier of X9 holds
ex z being object st
( z in the carrier of (X ./. RI) & h . z = y )

proof

let y be object ; :: thesis: ( y in the carrier of X9 implies ex z being object st
( z in the carrier of (X ./. RI) & h . z = y ) )
assume y in the carrier of X9 ; :: thesis: ex z being object st
( z in the carrier of (X ./. RI) & h . z = y )
then y in rng f by A2, FUNCT_2:def 3;
then consider x being object such that
A5: x in dom f and
A6: y = f . x by FUNCT_1:def 3;
take (nat_hom RI) . x ; :: thesis: ( (nat_hom RI) . x in the carrier of (X ./. RI) & h . ((nat_hom RI) . x) = y )
A7: dom (nat_hom RI) = the carrier of X by FUNCT_2:def 1;
then (nat_hom RI) . x in rng (nat_hom RI) by A5, FUNCT_1:def 3;
hence ( (nat_hom RI) . x in the carrier of (X ./. RI) & h . ((nat_hom RI) . x) = y ) by A3, A5, A6, A7, FUNCT_1:13; :: thesis: verum

end;

then rng h = the carrier of X9 by FUNCT_2:10;
then h is onto by FUNCT_2:def 3;
hence X ./. RI,X9 are_isomorphic by A4; :: thesis: verum