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 that
A1: I = Ker f and
A2: f is onto ; :: thesis: X ./. RI,X' are_isomorphic
consider h being BCI-homomorphism of (X ./. RI),X' such that
A3: f = h * (nat_hom RI) and
A4: h is one-to-one by A1, Th51;
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 A2, FUNCT_2:def 3;
then consider x being set such that
A5: x in dom f and
A6: 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 )
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 5;
hence ( z in the carrier of (X ./. RI) & h . z = y ) by A3, A5, A6, A7, 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 A4, Def9; :: thesis: verum