let G1, G2 be Group; :: thesis: for f being Homomorphism of G1,G2 holds (FuncLatt f) . ((1). G1) = (1). G2
let f be Homomorphism of G1,G2; :: thesis: (FuncLatt f) . ((1). G1) = (1). G2
consider A being Subset of G2 such that
A1: A = f .: the carrier of ((1). G1) ;
A2: A = f .: {(1_ G1)} by A1, GROUP_2:def 7;
A3: ( 1_ G1 in {(1_ G1)} & 1_ G2 = f . (1_ G1) ) by GROUP_6:31, TARSKI:def 1;
for x being object holds
( x in A iff x = 1_ G2 )

proof

let x be object ; :: thesis: ( x in A iff x = 1_ G2 )
thus ( x in A implies x = 1_ G2 ) :: thesis: ( x = 1_ G2 implies x in A )

proof

assume A4: x in A ; :: thesis: x = 1_ G2
then reconsider x = x as Element of G2 ;
consider y being Element of G1 such that
A5: y in {(1_ G1)} and
A6: x = f . y by A2, A4, FUNCT_2:65;
y = 1_ G1 by A5, TARSKI:def 1;
hence x = 1_ G2 by A6, GROUP_6:31; :: thesis: verum

end;

thus ( x = 1_ G2 implies x in A ) by A2, A3, FUNCT_2:35; :: thesis: verum

end;

then A = {(1_ G2)} by TARSKI:def 1;
then gr A = (1). G2 by Th12;
hence (FuncLatt f) . ((1). G1) = (1). G2 by A1, Def3; :: thesis: verum