let X, X9 be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X9
for Z being SubAlgebra of X9 st the carrier of Z = rng f holds
f is BCI-homomorphism of X,Z
let f be BCI-homomorphism of X,X9; :: thesis: for Z being SubAlgebra of X9 st the carrier of Z = rng f holds
f is BCI-homomorphism of X,Z
let Z be SubAlgebra of X9; :: 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 f9 = f as Function of X,Z by A1, RELSET_1:4;

now :: thesis: for a, b being Element of X holds (f9 . a) \ (f9 . b) = f9 . (a \ b)

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

end;

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