let X, X' be BCI-algebra; :: thesis: for I being Ideal of X
for f being BCI-homomorphism of X,X' st f is onto holds
f .: I is Ideal of X'
let I be Ideal of X; :: thesis: for f being BCI-homomorphism of X,X' st f is onto holds
f .: I is Ideal of X'
let f be BCI-homomorphism of X,X'; :: thesis: ( f is onto implies f .: I is Ideal of X' )
0. X in the carrier of X ;
then A1: 0. X in dom f by FUNCT_2:def 1;
( 0. X in I & f . (0. X) = 0. X' ) by Th35, BCIALG_1:def 18;
then reconsider imaf = f .: I as non empty Subset of by A1, FUNCT_1:def 12;
0. X in the carrier of X ;
then A2: 0. X in dom f by FUNCT_2:def 1;
assume A3: f is onto ; :: thesis: f .: I is Ideal of X'
A4: for x, y being Element of st x \ y in imaf & y in imaf holds
x in imaf

proof

let x, y be Element of ; :: thesis: ( x \ y in imaf & y in imaf implies x in imaf )
assume that
A5: x \ y in imaf and
A6: y in imaf ; :: thesis: x in imaf
consider y' being set such that
A7: y' in dom f and
A8: y' in I and
A9: y = f . y' by A6, FUNCT_1:def 12;
consider yy being Element of such that
A10: f . yy = x by A3, Th43;
consider z being set such that
A11: z in dom f and
A12: z in I and
A13: x \ y = f . z by A5, FUNCT_1:def 12;
reconsider y' = y', z = z as Element of by A7, A11;
set u = yy \ ((yy \ y') \ z);
((yy \ y') \ ((yy \ y') \ z)) \ z = 0. X by BCIALG_1:1;
then ((yy \ ((yy \ y') \ z)) \ y') \ z = 0. X by BCIALG_1:7;
then ((yy \ ((yy \ y') \ z)) \ y') \ z in I by BCIALG_1:def 18;
then (yy \ ((yy \ y') \ z)) \ y' in I by A12, BCIALG_1:def 18;
then A14: yy \ ((yy \ y') \ z) in I by A8, BCIALG_1:def 18;
yy \ ((yy \ y') \ z) in the carrier of X ;
then yy \ ((yy \ y') \ z) in dom f by FUNCT_2:def 1;
then [(yy \ ((yy \ y') \ z)),(f . (yy \ ((yy \ y') \ z)))] in f by FUNCT_1:8;
then f . (yy \ ((yy \ y') \ z)) in f .: I by A14, RELAT_1:def 13;
then (f . yy) \ (f . ((yy \ y') \ z)) in f .: I by Def6;
then (f . yy) \ ((f . (yy \ y')) \ (f . z)) in f .: I by Def6;
then (f . yy) \ ((x \ y) \ (x \ y)) in f .: I by A9, A13, A10, Def6;
then (f . yy) \ (0. X') in f .: I by BCIALG_1:def 5;
hence x in imaf by A10, BCIALG_1:2; :: thesis: verum

end;

( 0. X in I & f . (0. X) = 0. X' ) by Th35, BCIALG_1:def 18;
then 0. X' in imaf by A2, FUNCT_1:def 12;
hence f .: I is Ideal of X' by A4, BCIALG_1:def 18; :: thesis: verum