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