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 Th36;
FuncLatt f is sup-Semilattice-Homomorphism of lattice G1, lattice G2 by Th37;
hence FuncLatt f is Homomorphism of lattice G1, lattice G2 by A1, VECTSP_8:11; :: thesis: verum