for X, X9 being BCI-algebra
for f being BCI-homomorphism of X,X9 st f is onto holds
for c being Element of X9 ex x being Element of X st c = f . x