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

proof

let y be set ; :: thesis: ( y in the carrier of X' implies ex z being set st
( z in the carrier of (X ./. RI) & h . z = y ) )
assume y in the carrier of X' ; :: thesis: ex z being set st
( z in the carrier of (X ./. RI) & h . z = y )
then y in rng f by A1, FUNCT_2:def 3;
then consider x being set such that
B3: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
take z = (nat_hom RI) . x; :: thesis: ( z in the carrier of (X ./. RI) & h . z = y )
( dom (nat_hom RI) = the carrier of X & dom f = the carrier of X ) by FUNCT_2:def 1;
then ( dom (nat_hom RI) = the carrier of X & dom f = the carrier of X & (nat_hom RI) . x in rng (nat_hom RI) & dom h = the carrier of (X ./. RI) & dom f = the carrier of X ) by B3, FUNCT_1:def 5, FUNCT_2:def 1;
hence ( z in the carrier of (X ./. RI) & h . z = y ) by B3, A3, FUNCT_1:23; :: thesis: verum

end;

then rng h = the carrier of X' by FUNCT_2:16;
then h is onto by FUNCT_2:def 3;
hence X ./. RI,X' are_isomorphic by Def4, A3; :: thesis: verum