for G1, G2 being Group
for f being Homomorphism of G1,G2 st f is one-to-one holds
FuncLatt f is one-to-one