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 = w + a by Def2;
then consider W being open a_neighborhood of w, B being open a_neighborhood of a such that
A3: W + B 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 W + a by Th16;
then A4: ex h being Element of G st
( k = h + a & h in W ) by Th28;
a in B by CONNSP_2:4;
then k in W + B by A4;
hence k in A by A3; :: thesis: verum

end;

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