let X', X be BCI-algebra; :: thesis: for A' being non empty Subset of
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 ; :: 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

A2: now

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

end;

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