let T be TopaddGroup; :: thesis: ( T is BinContinuous implies T is homogeneous )
assume T is BinContinuous ; :: thesis: T is homogeneous
then reconsider G = T as BinContinuous TopaddGroup ;
G is homogeneous

proof

let p, q be Point of G; :: according to TOPGRP_1:def 6 :: thesis: ex b₁ being Homeomorphism of G st b₁ . p = q
take + ((- p) + q) ; :: thesis: (+ ((- p) + q)) . p = q
thus (+ ((- p) + q)) . p = p + ((- p) + q) by Def2
.= (p + (- p)) + q by RLVECT_1:def 3
.= (0_ G) + q by Def5
.= q by Def4 ; :: thesis: verum

end;

hence T is homogeneous ; :: thesis: verum