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

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

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

end;

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