let X, X9 be BCI-algebra; :: thesis: for f being BCI-homomorphism of X,X9
for g being BCI-homomorphism of X9,X st f is bijective & g = f " holds
g is bijective
let f be BCI-homomorphism of X,X9; :: thesis: for g being BCI-homomorphism of X9,X st f is bijective & g = f " holds
g is bijective
let g be BCI-homomorphism of X9,X; :: thesis: ( f is bijective & g = f " implies g is bijective )
assume A1: ( f is bijective & g = f " ) ; :: thesis: g is bijective
dom f = the carrier of X by FUNCT_2:def 1;
then rng g = the carrier of X by A1, FUNCT_1:33;
then A2: g is onto by FUNCT_2:def 3;
g is one-to-one by A1, FUNCT_1:40;
hence g is bijective by A2; :: thesis: verum