for X, X9 being 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 holds
ex h being BCI-homomorphism of (X ./. RI),X9 st
( f = h * (nat_hom RI) & h is one-to-one )