let G be Group; :: thesis: FuncLatt (id the carrier of G) = id the carrier of (lattice G)
set f = id the carrier of G;
A1: for x being object st x in the carrier of (lattice G) holds
(FuncLatt (id the carrier of G)) . x = x

proof

let x be object ; :: thesis: ( x in the carrier of (lattice G) implies (FuncLatt (id the carrier of G)) . x = x )
assume x in the carrier of (lattice G) ; :: thesis: (FuncLatt (id the carrier of G)) . x = x
then reconsider x = x as strict Subgroup of G by GROUP_3:def 1;
A2: the carrier of x c= (id the carrier of G) .: the carrier of x

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of x or z in (id the carrier of G) .: the carrier of x )
assume A3: z in the carrier of x ; :: thesis: z in (id the carrier of G) .: the carrier of x
the carrier of x c= the carrier of G by GROUP_2:def 5;
then reconsider z = z as Element of G by A3;
(id the carrier of G) . z = z ;
hence z in (id the carrier of G) .: the carrier of x by A3, FUNCT_2:35; :: thesis: verum

end;

A4: (id the carrier of G) .: the carrier of x c= the carrier of x

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (id the carrier of G) .: the carrier of x or z in the carrier of x )
assume A5: z in (id the carrier of G) .: the carrier of x ; :: thesis: z in the carrier of x
then reconsider z = z as Element of G ;
ex Z being Element of G st
( Z in the carrier of x & z = (id the carrier of G) . Z ) by A5, FUNCT_2:65;
hence z in the carrier of x ; :: thesis: verum

end;

then reconsider X = the carrier of x as Subset of G by A2, XBOOLE_0:def 10;
(id the carrier of G) .: the carrier of x = the carrier of x by A4, A2;
then (FuncLatt (id the carrier of G)) . x = gr X by Def3;
hence (FuncLatt (id the carrier of G)) . x = x by Th3; :: thesis: verum

end;

dom (FuncLatt (id the carrier of G)) = the carrier of (lattice G) by FUNCT_2:def 1;
hence FuncLatt (id the carrier of G) = id the carrier of (lattice G) by A1, FUNCT_1:17; :: thesis: verum