let X, X9 be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X9 holds
( f is one-to-one iff Ker f = {(0. X)} )
let f be BCI-homomorphism of X,X9; :: thesis: ( f is one-to-one iff Ker f = {(0. X)} )
thus ( f is one-to-one implies Ker f = {(0. X)} ) :: thesis: ( Ker f = {(0. X)} implies f is one-to-one )

proof

assume A1: f is one-to-one ; :: thesis: Ker f = {(0. X)}
thus Ker f c= {(0. X)} :: according to XBOOLE_0:def 10 :: thesis: {(0. X)} c= Ker f

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Ker f or a in {(0. X)} )
assume a in Ker f ; :: thesis: a in {(0. X)}
then A2: ex x being Element of X st
( a = x & f . x = 0. X9 ) ;
then reconsider a = a as Element of X ;
f . a = f . (0. X) by A2, Th35;
then a = 0. X by A1, FUNCT_2:19;
hence a in {(0. X)} by TARSKI:def 1; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {(0. X)} or a in Ker f )
assume A3: a in {(0. X)} ; :: thesis: a in Ker f
then reconsider a = a as Element of X by TARSKI:def 1;
a = 0. X by A3, TARSKI:def 1;
then f . a = 0. X9 by Th35;
hence a in Ker f ; :: thesis: verum

end;

assume A4: Ker f = {(0. X)} ; :: thesis: f is one-to-one

now :: thesis: for a, b being Element of X st a <> b holds
not f . a = f . b

let a, b be Element of X; :: thesis: ( a <> b implies not f . a = f . b )
assume that
A5: a <> b and
A6: f . a = f . b ; :: thesis: contradiction
(f . b) \ (f . a) = 0. X9 by A6, BCIALG_1:def 5;
then f . (b \ a) = 0. X9 by Def6;
then b \ a in Ker f ;
then A7: b \ a = 0. X by A4, TARSKI:def 1;
(f . a) \ (f . b) = 0. X9 by A6, BCIALG_1:def 5;
then f . (a \ b) = 0. X9 by Def6;
then a \ b in Ker f ;
then a \ b = 0. X by A4, TARSKI:def 1;
hence contradiction by A5, A7, BCIALG_1:def 7; :: thesis: verum

end;

then for a, b being Element of X st f . a = f . b holds
a = b ;
hence f is one-to-one by GROUP_6:1; :: thesis: verum