theorem :: BCIALG_6:37

for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9 holds
( f is one-to-one iff Ker f = {(0. X)} )