set f = a * ;
for w being Point of G
for A being a_neighborhood of (a *) . w ex W being a_neighborhood of w st (a *) .: W c= A

proof

let w be Point of G; :: thesis: for A being a_neighborhood of (a *) . w ex W being a_neighborhood of w st (a *) .: W c= A
let A be a_neighborhood of (a *) . w; :: thesis: ex W being a_neighborhood of w st (a *) .: W c= A
(a *) . w = a * w by Def1;
then consider B being open a_neighborhood of a, W being open a_neighborhood of w such that
A1: B * W c= A by Th36;
take W ; :: thesis: (a *) .: W c= A
let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in (a *) .: W or k in A )
assume k in (a *) .: W ; :: thesis: k in A
then k in a * W by Th15;
then A2: ex h being Element of G st
( k = a * h & h in W ) by GROUP_2:27;
a in B by CONNSP_2:4;
then k in B * W by A2;
hence k in A by A1; :: thesis: verum

end;

hence a * is continuous by BORSUK_1:def 1; :: thesis: verum