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 consider x' being Element of X such that
B1: ( x = x' & f . x' = 0. X' ) ;
thus x in the carrier of X by B1; :: thesis: verum

end;

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

proof

f . (0. X) = 0. X' by PR1621;
then B1: 0. X in Ker f ;

now

let x, y be Element of X; :: thesis: ( x \ y in Ker f & y in Ker f implies x in Ker f )
assume B3: ( x \ y in Ker f & y in Ker f ) ; :: thesis: x in Ker f
then consider y' being Element of X such that
B5: ( y = y' & f . y' = 0. X' ) ;
consider x' being Element of X such that
B7: ( x \ y = x' & f . x' = 0. X' ) by B3;
(f . x) \ (0. X') = 0. X' by B5, B7, Def0;
then f . x = 0. X' by BCIALG_1:2;
hence x in Ker f ; :: thesis: verum

end;

hence Ker f is Ideal of X by A1, B1, BCIALG_1:def 18; :: thesis: verum

end;

then reconsider Kf = Ker f as Ideal of X ;
Kf is closed

proof

let x be Element of Kf; :: according to BCIALG_1:def 19 :: thesis: x ` in Kf
x in Kf ;
then consider x' being Element of X such that
B1: ( x = x' & f . x' = 0. X' ) ;
f . (x ` ) = (f . (0. X)) \ (f . x) by Def0;
then f . (x ` ) = (0. X') ` by PR1621, B1;
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