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

now

let x' be Element of Kf; :: thesis: x' ` in Kf
consider x being set such that
x in dom f and
A1: x in CI and
A2: x' = f . x by FUNCT_1:def 12;
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:8;
then f . (x ` ) in f .: CI by RELAT_1:def 13;
then (f . (0. X)) \ (f . x) in f .: CI by Def6;
hence x' ` in Kf by A2, Th35; :: thesis: verum

end;

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