let X', X be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X'
for Z being SubAlgebra of X' st the carrier of Z = rng f holds
f is BCI-homomorphism of X,Z
let f be BCI-homomorphism of X,X'; :: thesis: for Z being SubAlgebra of X' st the carrier of Z = rng f holds
f is BCI-homomorphism of X,Z
let Z be SubAlgebra of X'; :: thesis: ( the carrier of Z = rng f implies f is BCI-homomorphism of X,Z )
A1: dom f = the carrier of X by FUNCT_2:def 1;
assume the carrier of Z = rng f ; :: thesis: f is BCI-homomorphism of X,Z
then reconsider f' = f as Function of X,Z by A1, RELSET_1:11;

now

let a, b be Element of X; :: thesis: (f' . a) \ (f' . b) = f' . (a \ b)
thus (f' . a) \ (f' . b) = (f . a) \ (f . b) by Th34
.= f' . (a \ b) by Def6 ; :: thesis: verum

end;

hence f is BCI-homomorphism of X,Z by Def6; :: thesis: verum