for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9
for g being BCI-homomorphism of X9,X st f is bijective & g = f " holds
g is bijective