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' )
assume AA: f is onto ; :: thesis: f .: I is Ideal of X'
f .: I is non empty Subset of X'

proof

AB: 0. X in I by BCIALG_1:def 18;
0. X in the carrier of X ;
then ( 0. X in dom f & f . (0. X) = 0. X' ) by PR1621, FUNCT_2:def 1;
hence f .: I is non empty Subset of X' by AB, FUNCT_1:def 12; :: thesis: verum

end;

then reconsider imaf = f .: I as non empty Subset of X' ;
BC: 0. X' in imaf

proof

AB: 0. X in I by BCIALG_1:def 18;
BB: f . (0. X) = 0. X' by PR1621;
0. X in the carrier of X ;
then 0. X in dom f by FUNCT_2:def 1;
hence 0. X' in imaf by AB, BB, FUNCT_1:def 12; :: thesis: verum

end;

for x, y being Element of X' st x \ y in imaf & y in imaf holds
x in imaf

proof

let x, y be Element of X'; :: thesis: ( x \ y in imaf & y in imaf implies x in imaf )
assume B3: ( x \ y in imaf & y in imaf ) ; :: thesis: x in imaf
then consider y' being set such that
B5: ( y' in dom f & y' in I & y = f . y' ) by FUNCT_1:def 12;
consider z being set such that
B7: ( z in dom f & z in I & x \ y = f . z ) by B3, FUNCT_1:def 12;
reconsider y' = y', z = z as Element of X by B5, B7;
consider yy being Element of X such that
B10: f . yy = x by Lm1653, AA;
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 B7, BCIALG_1:def 18;
then B13: ( yy \ ((yy \ y') \ z) in I & yy \ ((yy \ y') \ z) in the carrier of X ) by B5, BCIALG_1:def 18;
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 B13, RELAT_1:def 13;
then (f . yy) \ (f . ((yy \ y') \ z)) in f .: I by Def0;
then (f . yy) \ ((f . (yy \ y')) \ (f . z)) in f .: I by Def0;
then (f . yy) \ ((x \ y) \ (x \ y)) in f .: I by B5, B7, B10, Def0;
then (f . yy) \ (0. X') in f .: I by BCIALG_1:def 5;
hence x in imaf by B10, BCIALG_1:2; :: thesis: verum

end;

hence f .: I is Ideal of X' by BC, BCIALG_1:def 18; :: thesis: verum