let X, X9 be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X9 st f is onto holds
for c being Element of X9 ex x being Element of X st c = f . x
let f be BCI-homomorphism of X,X9; :: thesis: ( f is onto implies for c being Element of X9 ex x being Element of X st c = f . x )
A1: 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 object such that
A2: y in dom f and
A3: f . y = c by FUNCT_1:def 3;
reconsider y = y as Element of X by A2;
take y ; :: thesis: c = f . y
thus c = f . y by A3; :: thesis: verum

end;

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

end;

assume f is onto ; :: thesis: for c being Element of X9 ex x being Element of X st c = f . x
then rng f = the carrier of X9 by FUNCT_2:def 3;
hence for c being Element of X9 ex x being Element of X st c = f . x by A1; :: thesis: verum