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: dom (FuncLatt (id the carrier of G)) = the carrier of (lattice G) by FUNCT_2:def 1;
for x being set st x in the carrier of (lattice G) holds
(FuncLatt (id the carrier of G)) . x = x

proof

let x be set ; :: 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: (id the carrier of G) .: the carrier of x = the carrier of x

proof

thus (id the carrier of G) .: the carrier of x c= the carrier of x :: according to XBOOLE_0:def 10 :: thesis: the carrier of x c= (id the carrier of G) .: the carrier of x

proof

let z be set ; :: 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 A3: 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 ;
consider Z being Element of G such that
A4: ( Z in the carrier of x & z = (id the carrier of G) . Z ) by A3, FUNCT_2:116;
thus z in the carrier of x by A4, FUNCT_1:34; :: thesis: verum

end;

thus the carrier of x c= (id the carrier of G) .: the carrier of x :: thesis: verum

proof

let z be set ; :: 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 A5: 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 A5;
(id the carrier of G) . z = z by FUNCT_1:34;
hence z in (id the carrier of G) .: the carrier of x by A5, FUNCT_2:43; :: thesis: verum

end;

end;

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

end;

hence FuncLatt (id the carrier of G) = id the carrier of (lattice G) by A1, FUNCT_1:34; :: thesis: verum