let X, X9 be BCI-algebra; :: thesis: for I being Ideal of X
for f being BCI-homomorphism of X,X9 st f is onto holds
f .: I is Ideal of X9
let I be Ideal of X; :: thesis: for f being BCI-homomorphism of X,X9 st f is onto holds
f .: I is Ideal of X9
let f be BCI-homomorphism of X,X9; :: thesis: ( f is onto implies f .: I is Ideal of X9 )
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. X9 ) by Th35, BCIALG_1:def 18;
then reconsider imaf = f .: I as non empty Subset of X9 by A1, FUNCT_1:def 6;
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 X9
A4: for x, y being Element of X9 st x \ y in imaf & y in imaf holds
x in imaf

proof

let x, y be Element of X9; :: 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 y9 being object such that
A7: y9 in dom f and
A8: y9 in I and
A9: y = f . y9 by A6, FUNCT_1:def 6;
consider yy being Element of X such that
A10: f . yy = x by A3, Th42;
consider z being object such that
A11: z in dom f and
A12: z in I and
A13: x \ y = f . z by A5, FUNCT_1:def 6;
reconsider y9 = y9, z = z as Element of X by A7, A11;
set u = yy \ ((yy \ y9) \ z);
((yy \ y9) \ ((yy \ y9) \ z)) \ z = 0. X by BCIALG_1:1;
then ((yy \ ((yy \ y9) \ z)) \ y9) \ z = 0. X by BCIALG_1:7;
then ((yy \ ((yy \ y9) \ z)) \ y9) \ z in I by BCIALG_1:def 18;
then (yy \ ((yy \ y9) \ z)) \ y9 in I by A12, BCIALG_1:def 18;
then A14: yy \ ((yy \ y9) \ z) in I by A8, BCIALG_1:def 18;
yy \ ((yy \ y9) \ z) in the carrier of X ;
then yy \ ((yy \ y9) \ z) in dom f by FUNCT_2:def 1;
then [(yy \ ((yy \ y9) \ z)),(f . (yy \ ((yy \ y9) \ z)))] in f by FUNCT_1:1;
then f . (yy \ ((yy \ y9) \ z)) in f .: I by A14, RELAT_1:def 13;
then (f . yy) \ (f . ((yy \ y9) \ z)) in f .: I by Def6;
then (f . yy) \ ((f . (yy \ y9)) \ (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. X9) 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. X9 ) by Th35, BCIALG_1:def 18;
then 0. X9 in imaf by A2, FUNCT_1:def 6;
hence f .: I is Ideal of X9 by A4, BCIALG_1:def 18; :: thesis: verum