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 )
assume A1: the carrier of Z = rng f ; :: thesis: f is BCI-homomorphism of X,Z
f is Function of X,Z

proof

dom f = the carrier of X by FUNCT_2:def 1;
hence f is Function of X,Z by A1, RELSET_1:11; :: thesis: verum

end;

then reconsider f' = f as Function of X,Z ;

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 Lmth14
.= f' . (a \ b) by Def0 ; :: thesis: verum

end;

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