let X', X be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X' st f is onto holds
for c being Element of X' ex x being Element of X st c = f . x
let f be BCI-homomorphism of X,X'; :: thesis: ( f is onto implies for c being Element of X' ex x being Element of X st c = f . x )
assume f is onto ; :: thesis: for c being Element of X' ex x being Element of X st c = f . x
then A3: rng f = the carrier of X' by FUNCT_2:def 3;
for c being set holds
( c in rng f iff ex x being Element of X st c = f . x )

proof

let c be set ; :: thesis: ( c in rng f iff ex x being Element of X st c = f . x )
thus ( c in rng f implies ex x being Element of X st c = f . x ) :: thesis: ( ex x being Element of X st c = f . x implies c in rng f )

proof

assume c in rng f ; :: thesis: ex x being Element of X st c = f . x
then consider y being set such that
A1: ( y in dom f & f . y = c ) by FUNCT_1:def 5;
reconsider y = y as Element of X by A1;
take y ; :: thesis: c = f . y
thus c = f . y by A1; :: thesis: verum

end;

given x being Element of X such that A3: c = f . x ; :: thesis: c in rng f
( x in the carrier of X & the carrier of X = dom f ) by FUNCT_2:def 1;
hence c in rng f by A3, FUNCT_1:def 5; :: thesis: verum

end;

hence for c being Element of X' ex x being Element of X st c = f . x by A3; :: thesis: verum