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