let X, X9 be BCI-algebra; 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; 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; 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; ( I = Ker f & f is onto implies X ./. RI,X9 are_isomorphic )
assume that
A1:
I = Ker f
and
A2:
f is onto
; 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 )
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; verum