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

now

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:21
.= h . ((f . a) \ (f . b)) by Def0
.= (h . (f . a)) \ (h . (f . b)) by Def0
.= (g . a) \ (h . (f . b)) by FUNCT_2:21
.= (g . a) \ (g . b) by FUNCT_2:21 ; :: thesis: verum

end;

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