let X, X9 be BCI-algebra; :: thesis: for A9 being non empty Subset of X9
for f being BCI-homomorphism of X,X9 st A9 is Ideal of X9 holds
f " A9 is Ideal of X
let A9 be non empty Subset of X9; :: thesis: for f being BCI-homomorphism of X,X9 st A9 is Ideal of X9 holds
f " A9 is Ideal of X
let f be BCI-homomorphism of X,X9; :: thesis: ( A9 is Ideal of X9 implies f " A9 is Ideal of X )
assume A1: A9 is Ideal of X9 ; :: thesis: f " A9 is Ideal of X

A2: now :: thesis: for x, y being Element of X st x \ y in f " A9 & y in f " A9 holds
x in f " A9

let x, y be Element of X; :: thesis: ( x \ y in f " A9 & y in f " A9 implies x in f " A9 )
assume that
A3: x \ y in f " A9 and
A4: y in f " A9 ; :: thesis: x in f " A9
f . (x \ y) in A9 by A3, FUNCT_2:38;
then A5: (f . x) \ (f . y) in A9 by Def6;
f . y in A9 by A4, FUNCT_2:38;
then f . x in A9 by A1, A5, BCIALG_1:def 18;
hence x in f " A9 by FUNCT_2:38; :: thesis: verum

end;

0. X9 in A9 by A1, BCIALG_1:def 18;
then f . (0. X) in A9 by Th35;
then 0. X in f " A9 by FUNCT_2:38;
hence f " A9 is Ideal of X by A2, BCIALG_1:def 18; :: thesis: verum