let G1, G2 be Group; :: thesis: for f being Homomorphism of G1,G2 st f is one-to-one holds
FuncLatt f is Homomorphism of (lattice G1),(lattice G2)
let f be Homomorphism of G1,G2; :: thesis: ( f is one-to-one implies FuncLatt f is Homomorphism of (lattice G1),(lattice G2) )
assume f is one-to-one ; :: thesis: FuncLatt f is Homomorphism of (lattice G1),(lattice G2)
then A1: FuncLatt f is Semilattice-Homomorphism of (lattice G1),(lattice G2) by Th31;
FuncLatt f is sup-Semilattice-Homomorphism of (lattice G1),(lattice G2) by Th32;
hence FuncLatt f is Homomorphism of (lattice G1),(lattice G2) by A1; :: thesis: verum