let X, X9 be BCI-algebra; :: thesis: for CI being closed Ideal of X
for f being BCI-homomorphism of X,X9 st f is onto holds
f .: CI is closed Ideal of X9
let CI be closed Ideal of X; :: thesis: for f being BCI-homomorphism of X,X9 st f is onto holds
f .: CI is closed Ideal of X9
let f be BCI-homomorphism of X,X9; :: thesis: ( f is onto implies f .: CI is closed Ideal of X9 )
assume f is onto ; :: thesis: f .: CI is closed Ideal of X9
then reconsider Kf = f .: CI as Ideal of X9 by Th47;

now :: thesis: for x9 being Element of Kf holds x9 ` in Kf

let x9 be Element of Kf; :: thesis: x9 ` in Kf
consider x being object such that
x in dom f and
A1: x in CI and
A2: x9 = f . x by FUNCT_1:def 6;
reconsider x = x as Element of CI by A1;
x ` in the carrier of X ;
then x ` in dom f by FUNCT_2:def 1;
then ( x ` in CI & [(x `),(f . (x `))] in f ) by BCIALG_1:def 19, FUNCT_1:1;
then f . (x `) in f .: CI by RELAT_1:def 13;
then (f . (0. X)) \ (f . x) in f .: CI by Def6;
hence x9 ` in Kf by A2, Th35; :: thesis: verum

end;

hence f .: CI is closed Ideal of X9 by BCIALG_1:def 19; :: thesis: verum