assume A4: g in (a -con_map) " {x} ; :: thesis: g in Cad
then (a -con_map) . g in {x} by FUNCT_1:def 7;
then A5: (a -con_map) . g = x by TARSKI:def 1;
reconsider y = g as Element of G by A4;
A6: (a -con_map) . g = a |^ y by Def2;
A7: y * (((d ") * a) * d) = (y * ((d ") * a)) * d by GROUP_1:def 3
.= ((y * (d ")) * a) * d by GROUP_1:def 3 ;
y * (((y ") * a) * y) = (y * ((y ") * a)) * y by GROUP_1:def 3
.= a * y by GROUP_3:1 ;
then (((y * (d ")) * a) * d) * (d ") = a * (y * (d ")) by A1, A5, A6, A7, GROUP_1:def 3;
then (y * (d ")) * a = a * (y * (d ")) by GROUP_3:1;
then y * (d ") is Element of (Centralizer a) by Th8;
then consider z being Element of G such that
A8: z in the carrier of (Centralizer a) and
A9: y * (d ") = z ;
A10: z in Centralizer a by A8;
reconsider z = z as Element of G ;
y = z * d by A9, GROUP_3:1;
hence g in Cad by A10, GROUP_2:104; :: thesis: verum

assume g in Cad ; :: thesis: g in (a -con_map) " {x}
then consider z being Element of G such that
A11: g = z * d and
A12: z in Centralizer a by GROUP_2:104;
reconsider y = g as Element of G by A11;
y * (d ") = z by A11, GROUP_3:1;
then y * (d ") in carr (Centralizer a) by A12;
then (y * (d ")) * a = a * (y * (d ")) by Th8;
then ((y * (d ")) * a) * d = a * ((y * (d ")) * d) by GROUP_1:def 3;
then ((y * (d ")) * a) * d = a * y by GROUP_3:1;
then (y * (d ")) * (a * d) = a * y by GROUP_1:def 3;
then (y ") * ((y * (d ")) * (a * d)) = ((y ") * a) * y by GROUP_1:def 3;
then ((y ") * (y * (d "))) * (a * d) = ((y ") * a) * y by GROUP_1:def 3;
then (d ") * (a * d) = ((y ") * a) * y by GROUP_3:1;
then x = a |^ y by A1, GROUP_1:def 3;
then (a -con_map) . y = x by Def2;
then A13: (a -con_map) . y in {x} by TARSKI:def 1;
dom (a -con_map) = the carrier of G by FUNCT_2:def 1;
hence g in (a -con_map) " {x} by A13, FUNCT_1:def 7; :: thesis: verum