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

now

let a, b be Element of ; :: 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,H' by Def6; :: thesis: verum