let X, X9 be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X9 holds f . (0. X) = 0. X9
let f be BCI-homomorphism of X,X9; :: thesis: f . (0. X) = 0. X9
f . (0. X) = f . ((0. X) `) by BCIALG_1:2
.= (f . (0. X)) \ (f . (0. X)) by Def6 ;
hence f . (0. X) = 0. X9 by BCIALG_1:def 5; :: thesis: verum