let X', X be BCI-algebra; :: thesis: for A' being non empty Subset of X'
for f being BCI-homomorphism of X,X' st A' is Ideal of X' holds
f " A' is Ideal of X
let A' be non empty Subset of X'; :: thesis: for f being BCI-homomorphism of X,X' st A' is Ideal of X' holds
f " A' is Ideal of X
let f be BCI-homomorphism of X,X'; :: thesis: ( A' is Ideal of X' implies f " A' is Ideal of X )
assume A1: A' is Ideal of X' ; :: thesis: f " A' is Ideal of X
0. X' in A' by A1, BCIALG_1:def 18;
then f . (0. X) in A' by PR1621;
then C3: 0. X in f " A' by FUNCT_2:46;

now

let x, y be Element of X; :: thesis: ( x \ y in f " A' & y in f " A' implies x in f " A' )
assume B1: ( x \ y in f " A' & y in f " A' ) ; :: thesis: x in f " A'
then E1: f . (x \ y) in A' by FUNCT_2:46;
E3: f . y in A' by B1, FUNCT_2:46;
(f . x) \ (f . y) in A' by Def0, E1;
then f . x in A' by A1, E3, BCIALG_1:def 18;
hence x in f " A' by FUNCT_2:46; :: thesis: verum

end;

hence f " A' is Ideal of X by C3, BCIALG_1:def 18; :: thesis: verum