let X', X be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X' holds Ker f is closed Ideal of X
let f be BCI-homomorphism of X,X'; :: thesis: Ker f is closed Ideal of X

now

let x be set ; :: thesis: ( x in Ker f implies x in the carrier of X )
assume x in Ker f ; :: thesis: x in the carrier of X
then ex x' being Element of X st
( x = x' & f . x' = 0. X' ) ;
hence x in the carrier of X ; :: thesis: verum

end;

then A1: Ker f is non empty Subset of X by TARSKI:def 3;

A2: now

let x, y be Element of X; :: thesis: ( x \ y in Ker f & y in Ker f implies x in Ker f )
assume ( x \ y in Ker f & y in Ker f ) ; :: thesis: x in Ker f
then ( ex y' being Element of X st
( y = y' & f . y' = 0. X' ) & ex x' being Element of X st
( x \ y = x' & f . x' = 0. X' ) ) ;
then (f . x) \ (0. X') = 0. X' by Def6;
then f . x = 0. X' by BCIALG_1:2;
hence x in Ker f ; :: thesis: verum

end;

f . (0. X) = 0. X' by Th35;
then 0. X in Ker f ;
then reconsider Kf = Ker f as Ideal of X by A1, A2, BCIALG_1:def 18;
Kf is closed

proof

let x be Element of Kf; :: according to BCIALG_1:def 19 :: thesis: x ` in Kf
x in Kf ;
then A3: ex x' being Element of X st
( x = x' & f . x' = 0. X' ) ;
f . (x ` ) = (f . (0. X)) \ (f . x) by Def6;
then f . (x ` ) = (0. X') ` by A3, Th35;
then f . (x ` ) = 0. X' by BCIALG_1:def 5;
hence x ` in Kf ; :: thesis: verum

end;

hence Ker f is closed Ideal of X ; :: thesis: verum