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

now :: thesis: for x being object st x in Ker f holds
x in the carrier of X

let x be object ; :: 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 x9 being Element of X st
( x = x9 & f . x9 = 0. X9 ) ;
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 :: thesis: for x, y being Element of X st x \ y in Ker f & y in Ker f holds
x in Ker f

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 y9 being Element of X st
( y = y9 & f . y9 = 0. X9 ) & ex x9 being Element of X st
( x \ y = x9 & f . x9 = 0. X9 ) ) ;
then (f . x) \ (0. X9) = 0. X9 by Def6;
then f . x = 0. X9 by BCIALG_1:2;
hence x in Ker f ; :: thesis: verum

end;

f . (0. X) = 0. X9 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 x9 being Element of X st
( x = x9 & f . x9 = 0. X9 ) ;
f . (x `) = (f . (0. X)) \ (f . x) by Def6;
then f . (x `) = (0. X9) ` by A3, Th35;
then f . (x `) = 0. X9 by BCIALG_1:def 5;
hence x ` in Kf ; :: thesis: verum

end;

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