let X be BCI-algebra; :: thesis: for I being Ideal of X
for RI being I-congruence of X,I holds nat_hom RI is onto
let I be Ideal of X; :: thesis: for RI being I-congruence of X,I holds nat_hom RI is onto
let RI be I-congruence of X,I; :: thesis: nat_hom RI is onto
set f = nat_hom RI;
set Y = X ./. RI;
reconsider Y = X ./. RI as BCI-algebra ;
reconsider f = nat_hom RI as BCI-homomorphism of X,Y ;
for y being object st y in the carrier of Y holds
ex x being object st
( x in the carrier of X & y = f . x )

proof

let y be object ; :: thesis: ( y in the carrier of Y implies ex x being object st
( x in the carrier of X & y = f . x ) )
assume A1: y in the carrier of Y ; :: thesis: ex x being object st
( x in the carrier of X & y = f . x )
then reconsider y = y as Element of Y ;
consider x being object such that
A2: x in the carrier of X and
A3: y = Class (RI,x) by A1, EQREL_1:def 3;
take x ; :: thesis: ( x in the carrier of X & y = f . x )
thus ( x in the carrier of X & y = f . x ) by A2, A3, Def10; :: thesis: verum

end;

then rng f = the carrier of Y by FUNCT_2:10;
hence nat_hom RI is onto by FUNCT_2:def 3; :: thesis: verum