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