for G1, G2 being Group
for f being Homomorphism of G1,G2 holds (FuncLatt f) . ((1). G1) = (1). G2