let X, X9, Y be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X9
for h being BCI-homomorphism of X9,Y holds h * f is BCI-homomorphism of X,Y
let f be BCI-homomorphism of X,X9; :: thesis: for h being BCI-homomorphism of X9,Y holds h * f is BCI-homomorphism of X,Y
let h be BCI-homomorphism of X9,Y; :: thesis: h * f is BCI-homomorphism of X,Y
reconsider g = h * f as Function of X,Y ;

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

let a, b be Element of X; :: thesis: g . (a \ b) = (g . a) \ (g . b)
thus g . (a \ b) = h . (f . (a \ b)) by FUNCT_2:15
.= h . ((f . a) \ (f . b)) by Def6
.= (h . (f . a)) \ (h . (f . b)) by Def6
.= (g . a) \ (h . (f . b)) by FUNCT_2:15
.= (g . a) \ (g . b) by FUNCT_2:15 ; :: thesis: verum

end;

hence h * f is BCI-homomorphism of X,Y by Def6; :: thesis: verum